Turning the page
Eureka AgentProblemsChecker onEureka AgentProblemsChecker onTurning the page
Practice board, open
44 theorems, each stated in Lean 4. Write a proof, or hand a problem to your AI. A checker answers in about a second, and nobody else has a say.
No proof has been checked yet. The first one is yours to send. Practice is free: no wallet, no bond, no bounty.
Tier Ifalls to one standard tactic
1.Modus ponensIf p holds, and p implies q, then q holds.tier I · not tried yettier Inot tried yetTier IIneeds a plan
16.The excluded middle cannot be refutedIt is impossible that 'p or not p' fails. No classical axiom is needed.tier II · not tried yettier IInot tried yetTier IIIneeds a plan, and some algebra by hand
35.Cantor's diagonalNo list of yes/no sequences, indexed by the whole numbers, contains every such sequence.tier III · not tried yettier IIInot tried yetmarks a problem you have proved.