Mathematics in Isabelle
Caveat emptor: this web page is outdated, and is not being maintained.
This is a small-scale project, directed by Jeremy
Avigad, based in the Department of Philosophy at Carnegie Mellon University.
The project's goal is to formalize, and develop tools to assist in the formalization
of, portions of mathematics in Isabelle's
higher-order logic. We are currently focusing on number theory in particular.
The following people have worked on this project in the past.
- Kevin Donnelly, now a Ph.D student
in computer science at Boston University
- David Gray, Ph.D. student
in philosophy (studying ethics) at Carnegie Mellon
- Adam Kramer, now a Ph.D. student in experimental psychology at Oregon
- Paul Raff, now a Ph.D. student in mathematics at Rutgers
On September 6, 2004, we verified a proof of the prime number theorem.
- the Isabelle 2004 source files (downloadable as
a tar file)
- an index to the browser versions the
theory files
- an annotated index
- the theory files as a session document: pdf
(687 pages, 1.4 MB)
- a paper on the formalization: arXiv
- a talk based on that paper: pdf
- informal notes and initial thoughts on the formalization: pdf
(letter), pdf (a4)
- a paper by Avigad and Donnelly describing the library for big O calculations:
pdf (letter), pdf
(a4)
- an associated talk by Kevin Donnelly: pdf
The project is in mentioned in an article
on formal verification in Science (Vol 307, Issue 5714, 1402-1403, March
4, 2005). Isabelle also makes an appearance in a more philosophical paper of
mine, "Mathematical method and proof": pdf
(letter), pdf (a4)
The formalization has not been adapated to Isabelle 2005. Note that almost
everything in the files RingLib, FiniteLib, EvenOdd2, SetsAndFunctions, RealLib,
BigO, and Ln is included in or superceded by libraries that will be part of
the Isabelle 2005 release. Soon I hope to clean up and revise the elementary
number theory libraries as well.
Here are some of our contributions to the Isabelle 2004 release:
- a library for dealing with parity (HOL/Parity)
- properties of finite sums and products, and cardinalities of intervals (in
HOL/Finite_Set, HOL/Set_Interval)
- Gauss's law of quadratic reciprocity (in the HOL/NumberTheory session)
Here are some of our contributions to the Isabelle 2005 release:
- theorems supporting calculations in ordered rings, etc. (in HOL/OrderedGroup,
HOL/Ring_and_Field)
- theorems supporting casting between natural numbers, integers, and reals
(in HOL-Complex/RealDef, HOL-Complex/RComplete)
- properties of natural logarithm (HOL-Complex/Ln)
- libraries to support "big O" calculations (Library/SetsAndFunctions,
Library/BigO)
The prime number theorem theory files also include:
- basic facts about natural numbers and integers, involving divisibility,
primes, etc.
- unique factorization for the integers, and properties of the multiplicity
function
- properties of binomial coefficients (the "choose" function)
- elementary number-theoretic facts involving Euler's phi function, square-free
numbers, the mu function, and Moebius inversion
- asymptotic identities involving natural logarithm
- Chebyshev's theorems
- various forms of the Selberg symmetry formula
- a proof of the prime number theorem.
I currently intend to:
- work to develop better support for calculations with reals, casting, combinatorial
reasoning, etc.
- develop a good elementary number theory library
- write readable, expository, fully verified texts in elementary number theory
- start contributing to Tom Hales's Flyspeck
project
- experiment with the use of locales to prove theorems in algebra (perhaps
by formalizing Galois theory)
I am also interested in using such work to develop a better logical and philosophical
understanding of mathematical practice.
Comments and suggestions are welcome, and may be sent to avigad@cmu.edu.