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.

On September 6, 2004, we verified a proof of the prime number theorem.

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:

Here are some of our contributions to the Isabelle 2005 release:

The prime number theorem theory files also include:

I currently intend to:

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