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.