Show HN: Lean64 – doom64 style FPS on Lean 4

Category: other

Tags: game-engine, lean, fps

Score: 7.5/10 (Innovation: 8, Technical: 9, Documentation: 8, Utility: 5)

Lean64 is a first-person shooter game engine and demo campaign written entirely in Lean 4, implementing a Doom 64-style experience with original procedural art and audio. It is interesting because it demonstrates the use of a theorem prover language (Lean) for game development, including complex real-time systems like 3D rendering, AI, physics, and audio synthesis in a pure functional setting.

Target audience: game developers, language enthusiasts, experimental developers

Repository: https://github.com/aouxwoux/lean64 · Lean · MIT

View on Hacker News