Lean4

Updated: 30 August 2025

Background reading

  1. https://mathigon.org/world/Axioms_and_Proof
  2. https://www.uv.es/coslloen/Lean4/Leancap1.html
  3. Let’s code math | Lean4 | Theorem prover

A result or observation that we think is true is called a Hypothesis or Conjecture. Once we have proven it, we call it a Theorem. Once we have proven a theorem, we can use it to prove other, more complicated results – thus building up a growing network of mathematical theorems.

Leave a comment