State the claim.
The kernel decides whether it's proved.

A panel of models attacks your problem with the literature, Sage, PARI and an SMT solver — then formalises the result in Lean 4 against Mathlib. Lean's kernel either accepts the proof or it does not, and no amount of confident prose changes that. When it fails you get the exact goal that remains, which is usually where the informal argument was hand-waving.

The goal
Be specific about what "done" means. "Decide whether X is true, and prove it" beats "tell me about X".
The bar it has to clear
The referee holds this bar literally. Ask for a prize-level proof and it will tell you plainly when the panel falls short, rather than declaring victory.
The panel
Up to 6 debating seats. More seats means more angles — and more cost per round.
Referee
Rules on the criteria and re-checks every piece of evidence. Worth your strongest model.
Rounds
Spending limit
Hitting it pauses the match. Nothing is lost.
Sign up to start a match New accounts get starting credit — enough for a real match.
A checker that cannot be persuaded

Lean 4 with Mathlib type-checks the final statement, and a proof that leans on sorry or a fresh axiom is rejected rather than counted. Alongside it: SageMath, PARI/GP, Z3 and the OEIS, so a construction can be computed and identified before anyone tries to prove anything about it.

A failed proof is a finding

When formalisation fails, the goal Lean could not close is handed to whichever seat is best placed to attack it — just that goal, not the whole history. A rejected proof names the gap precisely, which is more than most informal arguments ever do.

Nothing is proved twice

Every lemma the panel establishes goes in a shared ledger with its proof, so it is never re-derived and dead ends are never retried. Long problems pause and resume without losing work — close the tab and come back tomorrow.