In formalized mathematics definitions and proofs ar e 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 1400 facts and definitions in algebra (groups, rings and fields) and general topology. In addition, about 1200 facts and 600 proofs have been translated 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. The Tiddly Formal Math site provides an alternative presentation of some IsarMathLib theories. Sometimes I write about IsarMathLib on my blog.
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?
A: 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?
A: Please send your contributions to the 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.
This page was last modified March 11th 2008.