Lean #

Lean is a theorem prover and programming language that can be used to formalise mathematics and use computers to prove theorems.

Links and resources #

• A course on formalising mathematics using Lean.
• Wikipedia.
• A book teaching functional programming using Lean.
• An interview with Terry Tao about automatic theorem proving with Lean and the future of mathematics post-AI.
  • A really great talk by Tao about the history of machine-assisted proofs in mathematics.