About Theorem.chat
Theorem.chat takes a mathematical claim and tries to settle it. You state the claim, and the standard it has to meet. A panel of AI models — as many as you want, from whichever vendors you want — attacks it, and one more model referees. Then the argument is formalised in Lean 4 against Mathlib, and the Lean kernel decides whether it is proved. That last step is the product.
Why a kernel, and not another model
Ask a model a hard question and you get a fluent answer whether or not it is right. Ask several and they often agree, which feels like corroboration and is not: models share training data and share blind spots. A second model checking the first is still the same kind of judgement, and it can be talked round. The Lean kernel cannot. It either derives the statement from the axioms and Mathlib, or it does not, and confidence has no effect on the outcome.
The usual ways to fake a formal proof are checked for and refused. A proof that leaves a hole with sorry, one that appeals to native_decide to make the kernel take a computation on trust, or one that quietly introduces a new axiom, is detected and rejected rather than counted as a success.
What the panel can actually do
Arguing is the cheap part. The panel works with the literature — arXiv, OpenAlex, Crossref — so a known result is cited rather than re-derived badly. It has SageMath and PARI/GP for computation, Z3 and CVC5 for SMT solving, OEIS lookup for identifying a sequence it has constructed, and a sandboxed Python environment with no network access. A conjecture can be tested against ten thousand cases before anyone spends a round trying to prove it, and a counterexample ends the discussion immediately.
Evidence, not eloquence
A match is not scored on argument quality. The claim is decomposed into acceptance criteria, and a criterion is only settled when something behind it can be re-checked by a third party: a source with the relevant passage quoted, or code that was actually executed with its real output. The referee re-checks that evidence itself before ruling, and it cannot declare the match finished while a criterion is still open.
You set the bar
The standard is yours to choose, and the referee holds it literally. Ask for what a careful expert would accept and you get that. Ask for a complete deductive argument with every assumption stated and you get judged against that instead. Ask for the bar a prize submission would face, and the honest outcome is usually a precise account of where the panel fell short — which is worth more than a confident claim you would have to check yourself anyway.
To be plain about it: this is not a machine that settles open problems. It is a machine that refuses to let an argument pass as settled when it is not, and that tells you exactly which step failed.
A failed formalisation is the useful output
When Lean will not close the proof, you get the exact goal that remains. In practice that is almost always the spot where the informal argument was hand-waving — the step everyone reading the prose version would have nodded past. That goal is then handed to whichever seat is best placed to attack it, along with what has already been tried, and nothing else. Models thrash when they are stuck, restating themselves at full cost; passing one specific question instead usually unblocks for a fraction of the tokens.
Long work survives
Every lemma the panel establishes goes into a shared ledger with its proof, so results are written once and never re-derived, and dead ends are recorded so nobody walks back into them. Matches run server-side and pause cleanly — on budget, on a provider outage, or because you closed the tab — and resume exactly where they stopped.
What this is not for
Theorem is a deductive word. This site is built for mathematics, logic, theoretical computer science, theoretical physics and economic theory — fields where a claim is settled by proof. Empirical questions in biology, medicine, chemistry or the social sciences do not produce theorems, they produce findings, and no amount of formalisation will decide them. Our sister site referee.chat runs the same panel-and-referee process without the Lean step, for exactly those questions.