Game da Theorem.chat
Theorem.chat na da wani zargin kimiyyar lissafi kuma yana kokarin daidaita shi. Kuna bayyana zargin, da kuma ma'aunin da ya kamata ya cika. Wani panel na AI models - kamar yadda kuke so, daga duk waɗanda kuke so - suna harin shi, da wani mai bincike na siffa. Sa'an nan an sanya hujjar a cikin Lean 4 a kan Mathlib, kuma Lean kernel na yanke shawarar ko an tabbatar da shi. Wannan mataki na ƙarshe shine samfurin.
Me yasa wani kernel, ba wani nau'i ba
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.
Abin da fanel ke iya yi a gaskiya
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.
@ action
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.
Ka saita bar
@ action: button
Don yin bayani game da shi: wannan ba injin ba ne wanda ke magance matsaloli masu budewa. Wannan injin ne wanda ke ki yarda da wani hujjar da ta wuce kamar yadda aka yanke hukunci idan ba haka ba, kuma wannan yana gaya maka daidai abin da mataki ya kuskure.
QODBCResult
@ action: button
QSoftKeyManager
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.
@ action
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.