A library of formalized mathematics for Isabelle/Isar proof assistant

In formalized mathematics definitions and proofs are written in a computer language so that they can be formally verified by a machine. This project uses the Isabelle/Isar theorem prover as the language and proof checker.
Isabelle is a generic theorem prover that supports several logical frameworks. IsarMathLib uses the ZF logic which implements Zermelo-Fraenkel (untyped) set theory.

The current release contains over 1300 facts and definitions in algebra (groups, rings and fields) and general topology. In addition, about 670 facts and 300 proofs have been imported from Metamath.
Release 1.0.0 finished formal verification of a construction of real numbers from the group of integers described for example in R. D. Arthan: "The Eudoxus Real Numbers", N. A'Campo: "A natural construction for the real numbers" and R. Street et al.: "The Efficient Real Numbers".

The latest release of IsarMathlib can be browsed here. The outline contains all theorems and comments, but does not contain the proofs. This is the recommended starting point for a casual reader. The proof document contains all theorems with formally verified proofs.

Questions and Answers

Q1: Why would anyone want to do formalized mathematics?

A: Because it is fun and a good exercise for your brain. Some people also believe that formalized mathematics can be useful.

Q2: Why Isabelle/Isar and not any of the other provers of the world?

A: The first reason is that the Isar syntax allows to write proofs that can be read and followed by anyone familiar with standard mathematical notation. The second reason is that Isabelle/Isar is free software, distributed under the modified BSD license. It can also be downloaded free of charge.

Q3: Why ZF logic?

Almost all mathematics I know about is based on the first order logic and
Zermelo-Fraenkel set theory. This is what I was taught in high school and feels natural to me. I am sure other logical frameworks, like HOL, are interesting and useful, but someone would have to pay me money to make me twist my brain around HOL and its typed set theory.

Q4: How can I contribute?

Please send your contributions to isarmathlib-devel mailing list. The Style Guide provides information about the suggested writing style. If you submit a theory file the copyright of that theory file will be assigned to you.  Single theorems will be attributed in the proof document. I may edit your submission  and move the theorems to different theory files.

Health Warning: Proving theorems may be addictive!

See here and here. It's true.

This page was last modified November 30th 2006.

Valid HTML 4.01 Transitional