petergpt/lean-3d-game-axiom

Axiom: First Light is a playable first person voxel game, built almost entirely in Lean 4, a programming language normally used for proving mathematical theorems rather than making games. The project shows that the same language used for formal proofs can also run a real time game loop, complete with graphics, physics, sound, and saved progress. In the game you explore a small island made of blocks, about 96 by 96 by 48 units in size, with beaches, forest, caves, ocean, clouds, stars, and a day and night cycle. You can walk, sprint, jump, or switch to a creative flying mode, and you can mine and place blocks using nine different materials. There is a hidden cave and a marble sun gate somewhere on the island to find. The game deliberately stays small: there is no crafting, no combat, no multiplayer, and no endlessly generated terrain, since it is meant to be a compact, complete experience rather than an ever expanding one. Nearly everything that makes the game work, including world generation, block storage, rendering meshes, physics, aiming, editing, sound effects, saving, and the menus, is written in Lean. A separate library called Raylib handles the lower level platform work: opening the window, reading keyboard and mouse input, playing audio, and sending the graphics Lean produces to the graphics card. The game currently only runs on Apple Silicon Macs. You can download a prebuilt release and open the app directly, though you may need to right click and choose Open the first time since it is not notarized by Apple. To build it from source, you need macOS 26 on Apple Silicon, a Lean toolchain manager called elan installed through Homebrew, and Apple's clang compiler, after which a few setup scripts compile the game and launch it. The project is released under the MIT license and includes no third party art or audio.