Explanation¶

These pages discuss why Lean behaves as it does. They are not needed to finish the tutorial, and they are best read once something in Lean has already surprised us.

• Lean and Mathlib: what each piece of the toolchain is, and what it is not.
• The origins of Lean: from Microsoft Research in 2013 to Lean 4 and the Mathlib port.
• Computation and the real numbers: why decide fails on the reals and norm_num succeeds.
• Definitions and proofs: why formalising a definition is harder than formalising a proof, using two equivalent definitions of an ESS.
• Nash's existence theorem: what a formal proof would require, and why these notes stop short of it.