Lean 64

A barebones, windowed 3D first-person game implemented in Lean 4. Apparently lean is turing complete :)

Watch the 5-second 1080p60 gameplay clip with audio

Run it

Install elan, then:

lake build
lake exe lean64

For the deterministic five-second 60 FPS highlight loop with synchronized audio:

lake build lean64demo
lake exe lean64demo

Controls:

• Enter: deploy from the title screen or continue to Map 2
• 1 / 2 / 3 on the title screen: Easy, Hard, or Nightmare
• W / S: move forward and backward
• A / D: strafe
• mouse or arrow keys: yaw and pitch the camera
• Shift: sprint
• Space: fire
• E: use doors and switches
• 1 / 2: select the double-barrel shotgun or collected chaingun
• Tab or M: toggle the automap
• P: pause or resume
• R: restart after victory or death
• Esc or Q: quit

What is implemented

• a Win32/OpenGL presentation path with a retained software renderer for tests and screenshots
• 3D vectors, camera-space transforms, and perspective projection in Lean
• triangle mesh construction, camera state, and render submission authored in Lean
• GPU depth testing, distance fog, and procedural repeating material textures for the live game
• a barycentric software rasterizer and per-pixel depth buffer retained as a reference backend
• distance-aware muzzle illumination that briefly warms nearby world geometry and monsters
• procedural brick, riveted-metal, dirty-floor, ceiling, and emissive materials
• a two-map mini-campaign with distinct red-brick and teal-metal arenas
• campaign transitions that carry health, weapons, ammunition, difficulty, and score forward
• alternating Map 2 bulkheads that create a zig-zag combat gauntlet into a stronger Warden finale
• two staged encounter rooms joined by an interactive rising bulkhead
• classic red-key progression with a collectible 3D access card and locked bulkhead
• multi-part monster meshes with bodies, heads, limbs, glowing eyes, pain flashes, and timed collapse deaths
• dormant/alert monster awareness, pursuit, obstacle collision, melee attacks, and player damage
• ranged monster fireballs with travel, collision, and impact damage
• telegraphed ranged attacks with interruptible charge-up effects
• a heavy final-arena warden with a unique horned mesh, eight health, boss bar, purple reactor attacks, and bonus score
• shootable explosive barrels with splash damage, player damage, debris, and chain reactions
• world-space blood sprays, metal sparks, explosion debris, persistent blood pools, and capped wall-impact marks
• first-person movement, collision, yaw, pitch, sprinting, and unobstructed hitscan shooting
• movement-driven view bob, weapon sway, faster sprint cadence, and a decaying shotgun recoil kick
• captured relative mouse-look with automatic cursor restoration
• a two-shell super shotgun with held-fire cadence, hard recoil, muzzle smoke, opening breech, visible shell insertion, wood furniture, and shaped muzzle flash
• five-pellet horizontal shotgun spread with close-range stacking, multi-monster blasts, classic vertical auto-aim, and individual wall sparks and impact marks
• a collectible multi-barrel chaingun with rotary animation and rapid held-fire cadence
• separate shell and bullet ammunition pools with weapon-aware HUD display
• persistent corpses, health vials, shell boxes, and hit confirmation
• synthesized asynchronous shotgun and chaingun reports
• original synthesized wake, pain, death, fireball, impact, door, secret, pickup, barrel, keycard, and Warden cues
• event-prioritized audio dispatch authored in Lean, with the native shim limited to asynchronous WAV playback
• health, ammo, damage vignette, crosshair, score state, victory, death, and restart
• distinct full-screen red damage and warm pickup palette pulses
• a procedural title screen, reusable pixel font, pause overlay, numeric HUD, and readable state messages
• timed map-name cards for The Foundry and Black Circuit
• selectable Easy/Hard/Nightmare modes scaling enemy health, aggression, ammunition, damage, and score
• a full-screen intermission tracking real elapsed time, kills, secrets, shots, hits, accuracy, and score
• a live automap showing geometry, doors, supplies, alerted enemies, corpses, and the exit
• dynamic red/amber/green lock feedback in-world, on the HUD, and on the automap
• a hidden wall-rune secret with health, ammunition, score rewards, and a pixel-art discovery banner
• a second hidden, roofed maintenance chamber with a moving facade, trapped monster, supplies, and optional combat
• clear-gated glowing exit pads, per-map intermissions, and a campaign-complete state
• a real-time state/update/render loop with frame pacing

The game state, AI, combat, camera, meshes, material IDs, lighting changes, and HUD composition live in Lean. The native shim owns the Win32/OpenGL context, uploads Lean's triangle stream and HUD texture, and handles input and audio.

The next large milestone toward source-port territory would be a legally supplied WAD reader, BSP traversal, texture atlases, sprite animation, and a larger authored campaign. Lean 64 deliberately ships only original procedural art and synthesized audio.