Formalised mathematics
Here are some preliminary documents recording what I have learnt about formalising proofs in
Agda.
- Some notes entitled "Agda for the working mathematician".
- A brief survey outlining some but not all of the contents of the Agda standard library.
- A heavily annotated proof in Agda that there are infinitely many primes. The .lagda files mix Agda and LaTeX code; they can be interpreted by Agda, or processed by LaTeX to generate the pdf files below. The framework is partially explained here. Some of the code is only available in unannotated .agda files, but it should be possible to understand those if you read the annotated ones first.