7/30/2025
•
EN
The Math Is Haunted
An introduction to Lean, a programming language for formalizing mathematics, using a simple proof of 2=2 as an example.