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/

Textbooks

Philosophical commentary


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.