Lean, formal proofs, and verifiable reasoning
ยท 22 min read
Lean is a programming language in which mathematical proofs can be checked by a computer. This post gives an introduction to Lean, from its origins and recent history to its applications to model reasoning and verifiable reinforcement learning.
