Algebraic computations in Lean

This is a tutorial on doing proofs with a computational flavour using the mathlib library for the Lean 3 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.

Currently the tutorial focuses on the brand new tactic polyrith and on field_simp. There are several other powerful tactics which are commonly needed for “computational” proofs, notably norm_num, norm_cast (and variants), and (n)linarith. These other tactics are discussed in context as the need arises, but this tutorial might eventually be extended to cover them too.

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 is new (July 2022) and feedback is very welcome. If you try this tutorial, 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 case splits
  • 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, and Rob Lewis, for many conversations about automation in Lean.