Proofs as programs in Lean

This is the website for a discussion group on using Lean, held at NCTS in May-June 2025.

Lean is a programming language designed for writing mathematical proofs. It allows the computer to help verify that your proof is correct. In particular, writing a proof using Lean should “make it harder to prove things that are not true.” (borrowing words from Leslie Lamport.)

For this discussion group, we will use code in this github repository.

Project topics

For details, see the About section.

1. Newton’s theorem on real roots

2. Cauchy interlacing theorem

3. Puiseux’s theorem

4. Descartes’s rule of signs

5. Sturm’s theorem for polynomial roots

6. Newton’s theorem for valued fields

Lean resources

Official documentation: https://leanprover-community.github.io/mathlib4_docs/

Tactics reference

Quick search

• Human-language search: Zulip chat

• LLM-assisted human-language search: Leansearch

• Source code search (type signatures, etc.): Loogle

Textbooks

• Hitchhiker’s Guide to Logical Verification, by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, and Jannis Limperg

Philosophical commentary

• Is mathematics obsolete?, Jeremy Avigad

---

Website built using Just the Class, a template that extends the popular Just the Docs theme, which provides a robust and thoroughly-tested foundation for your website.