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 2000 facts and 150 definitions in algebra (groups, rings and fields), general topology and other areas of mathematics. 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".
IsarMathLib is also about readable presentations of formalized mathematics. One such experiment is the FormalMath.org site, which provides an HTML presentation of the most recent version of most of IsarMathLib theories. The official Isabelle generated proof document contains all theorems with formally verified proofs from the last release. The outline contains all theorems and comments, but does not contain the proofs. Isabelle generated HTML rendering can be browsed here.
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: Clone IsarMathLib, formalize some math and send a pull request to the IsarMathlib's repository on GitHub. 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 August 02nd 2020.