The short version
An interactive Lean course that builds natural-number proofs from the Peano axioms.
From the HackerLinks archive
Natural Number Game
An interactive Lean course that builds natural-number proofs from the Peano axioms.
At a glance:
First seen:2026-07-23
Last seen:2026-07-23
Times seen:1
Website:adam.math.hhu.de
Why it caught our attention
It is a notably approachable on-ramp to Lean rather than another passive reference.
Where it surfaced on Hacker News
2026-07-23
Editorial paraphrase
Multiple commenters called it ‘amazing’ and ‘the best intro to Lean,’ strongly recommending it to beginners.
Original threadIntroduction to Formal Verification with Lean Part 1