Formal Verification / Lean 4 Simulator
Quasi-Perfect Puzzler
Apply tactics to a proof tree and work your way to a complete proof. You can skip a goal with “sorry,” but the score will notice.
Cabinet Standby
FDR PORTFOLIO ARCADE v2.6Quasi-Perfect Puzzler
Small Proofs, Limited Memory
Apply tactics to a proof tree and work your way to a complete proof. You can skip a goal with “sorry,” but the score will notice.
Click / DragApply Tactic
Ctrl/⌘ + Z / YUndo / Redo
R / MReset Level / Switch Mode
Quasi-Perfect Puzzler needs a bigger screen
It's built for a keyboard and a desktop-sized screen, and on a phone it's cramped. Save the link and play it on your laptop.
Meanwhile, on your phone
Tactics & AST Nodes
Drag tactic cards from your hand onto AST nodes, or tap a tactic card and then tap a target node to execute the proof step.
Lean Server RAM Limits
Each tactic, including a failed one, consumes simulated memory. Story Mode starts with twice the Hacker Mode budget. In either mode, if RAM hits 0 GB the simulated tactic session stops and the level must be reset. Close the theorem before running out of memory.
Theorem Morality & Sorry
Admitting goals via sorry instantly passes the level but incurs a heavy -100 Morality Penalty and 0 stars. Solve genuinely for gold ratings!