I wanted to see how lean does outside of theorems.(currently studying ME, professor introduced us to lean4)Lean handles the game loop, geometry, collision detection, enemy AI, weapons, particles, and HUD. The native side is a roughly 570-line C shim that handles Win32 input and audio, and submits Lean-generated triangles to OpenGL.The game currently has two maps, a shotgun, and a few secrets.