Lean-style formal verification arcade. Drag and apply tactics to simplify mathematical AST goals and preserve theorem morality.
Prove that an arbitrary variable equals itself (x = x) using the fundamental Law of Identity.
Drag a tactic card onto any target node, or click a node then click a card.
Close goal by reflexivity if Left-Hand Side exactly equals Right-Hand Side.
Admit the theorem without proof. Warning: Causes catastrophic mathematical morality loss.
In Type Theory, reflexivity is the canonical constructor of equality (`Eq.refl`). If two expressions evaluate to definitionally equal terms, `rfl` closes the goal in O(1) step.
-- Theorem: The Identity Crisis-- Chapter 1: Equational Reasoningtheorem identity_crisis (x : Nat) : x = x := bysorry -- Goal open
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.
Each tactic consumes language server memory. If RAM hits 0 GB, the Lean runtime crashes (OOM). Close the theorem before running out of memory.
Admitting goals via sorry instantly passes the level but incurs a heavy -100 Morality Penalty and 0 stars. Solve genuinely for gold ratings!