Peano numbers in Lean2024-01-10·2122 wordsMath Lean ProgrammingIn this post, I will define the natural numbers using the Peano axioms and prove that the set of natural numbers $\N$ equipped with ordinary addition and multiplication is a commutative semiring.