Dagstuhl experiments in formalisation
These pages report on a working group at
Schloss Dagstuhl Seminar 18341
on Formalization of Mathematics in Type Theory. The aim was to
investigate what happens when a working mathematician with limited
knowledge of proof assistants attempts to set up one of the more
popular systems and use it to perform some fairly basic tasks.
Tasks
The discussion on these pages will be based on the following list of
tasks, which is different in some details from the list used at the
conference.
| Prove that $1+1=2$ |
Details |
| Prove the infinitude of primes |
Details |
| Set up the unit group of a commutative ring. Prove that $\mathbb{Z}^\times=\{1,-1\}$. |
Details |
| Set up the ideal of nilpotents in a commutative ring, and the corresponding quotient ring.
Prove that $\text{Nil}(\mathbb{Z}/4)=\{0,2\}$ and $\text{Nil}(R/\text{Nil}(R))=0$. |
Details |
| Given a finite set $A$, construct the poset of partitions of $A$. Prove that if $|A|=3$ then $|\text{Part}(A)|=5$. |
Details |
Proof assistant systems
These pages will focus on the following three systems:
| Lean with the mathlib library |
Details |
| Coq/ssreflect with the mathematical components library |
Details |
| Isabelle HOL with the HOL-Algebra library |
Details |
Formalisations
| $1+1=2$ |
Lean |
| primes |
Lean |
| units |
|
| nilpotents |
Lean |
| partitions |
Lean |