NNG4

Tech stack & purpose

NNG4 is the Lean 4 version of the Natural Number Game, an interactive educational game built with the Lean4 Game Engine that teaches formal mathematics and proof techniques. The project is an adaptation of the original Lean 3 Natural Number Game from Imperial College London and runs live at adam.math.hhu.de. It is developed as a standard Lean project using the Lake build system and welcomes community contributions including translations into multiple languages.

Community & reference links

• See lean3 version
• lean4game repo
• Creating a Game
• Running Games Locally
• Lean Community Map

Languages

Contributors (top 30 of 45)

• 
  Kevin Buzzard278 commits · 946 followers
• 
  Jon Eugster174 commits · 36 followers
• 
  Jon Eugster33 commits · 36 followers
• 
  Alexander Bentkamp28 commits · 24 followers
• 
  Jiecheng Z21 commits · 8 followers
• 
  Pietro Monticone11 commits · 1,160 followers
• Yannick Seurin7 commits
• Jiecheng Z6 commits
• TentativeConvert3 commits
• 
  Madjosz2 commits · 4 followers
• Steven Clontz2 commits
• Balazs Endresz2 commits
• Federico2 commits
• Andrii Kurdiumov2 commits
• Marco Colombo2 commits
• dalps2 commits
• Yu-Ting Hsiung2 commits
• 
  Kitamado1 commits · 114 followers
• 
  Arnaud Bodin1 commits · 71 followers
• Hans Christian Schmitz1 commits
• 
  Chris Lloyd1 commits · 4 followers
• Marly Gotti1 commits
• 
  Bryan Gin-ge Chen1 commits · 49 followers
• Helder Geovane Gomes de Lima1 commits
• 
  Federico Dal Pio Luogo1 commits · 21 followers
• 
  Jan Hrcek1 commits · 80 followers
• 
  Thomas Moulin1 commits · 2 followers
• 
  abram!1 commits · 1 followers
• James Salvatore1 commits
• 
  Peiran Wu1 commits · 7 followers