Algebraic computations in Lean

This is a tutorial on doing proofs with a computational flavour using the Mathlib library for the Lean proof assistant.

The phrase “computational flavour” might need some explanation. These are not heavy computations that require two hours running Mathematica, but simply the kind of mildly-painful calculation that might take a couple of paragraphs on paper.

The tutorial focuses on the Gröbner basis tactic polyrith and on the division-cancelling tactic field_simp. There are several other powerful tactics which are commonly needed for “computational” proofs, notably norm_num, norm_cast (and variants), (n)linarith and gcongr. These other tactics are discussed in context as the need arises.

This is an intermediate-level tutorial, requiring familiarity with the syntax of Lean as covered in approximately the first two chapters of Mathematics in Lean. But the focus of the exercises and presentation is on the computations, so don’t worry about understanding every detail of the syntax if you can pick up the general idea.

This tutorial was originally written in Lean 3 in July 2022 when polyrith first appeared. A video of a talk at ICERM following that version of the tutorial is available in ICERM’s video database. The update to Lean 4 was posted in May 2024.

Feedback is very welcome. Email me (Heather Macbeth), or come to the Lean chat room on Zulip and say hello!

• 1. Basics of polyrith
  • 1.1. Housekeeping
  • 1.2. Basics of the linear_combination tactic
  • 1.3. linear_combination for nonlinear equations
  • 1.4. Basics of the polyrith tactic
• 2. Using polyrith
  • 2.1. Chebyshev polynomials
  • 2.2. Isometries of the complex plane
  • 2.3. Double cover of SO(3, ℝ)
• 3. Nonsingularity of algebraic curves
  • 3.1. Powers and cancellation
  • 3.2. Klein quartic
  • 3.3. Weierstrass-form elliptic curve
• 4. Combining tactics
  • 4.1. Basics of the field_simp tactic
  • 4.2. Stereographic projection
  • 4.3. A binomial coefficient identity

Acknowledgements: I have raided the Mathlib contributions of a number of people for examples in this tutorial. Thank you to Johan Commelin, Julian Külshammer and François Sunatori! And particular thanks to Jeremy Avigad, for sharing the Sphinx template for the tutorial; Marc Masdeu and Patrick Massot, for work on the bump to Lean 4; and Rob Lewis, for many conversations about automation in Lean.