natural_number_game

Tech stack & purpose

The Natural Number Game is an educational project that teaches formal mathematical proof through an interactive game built with Lean 3 (now end-of-life). The game introduces players to mathematical induction and formal proof techniques by having them prove fundamental properties of natural numbers—such as commutativity of addition and the distributive property—that are typically considered self-evident. Created by Kevin Buzzard with computational contributions from Mohammad Pedramfar, the project demonstrates how to express mathematics in a way that computers can verify and understand, addressing the challenge of teaching formal mathematics to machines.

Community & reference links

• here
• here
• Lean game maker
• the Zulip Lean chat
• this blog post
• Play here.

Languages

Contributors

• 
  Kevin Buzzard355 commits · 946 followers
• Mohammad3 commits
• Donald Sebastian Leung3 commits
• 
  Andrew Helwer2 commits · 238 followers
• 
  Mohammad Pedramfar2 commits · 11 followers
• postmasters2 commits
• Agro Rachmatullah1 commits
• Christopher Sumnicht1 commits
• 
  zx9w1 commits · 4 followers
• Alexandre Rademaker1 commits
• Matthias Hutzler1 commits
• 
  Sebastien Gouezel1 commits · 24 followers
• Predrag Gruevski1 commits
• 
  Bryan Gin-ge Chen1 commits · 49 followers
• 
  Patrick Massot1 commits · 219 followers
• Ben Dyer1 commits
• 
  crunsk1 commits · 1 followers
• Ilia Kriukov1 commits
• MatthiasHu1 commits