## 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.