IsarMathLib
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?
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 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.
