Karibu 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.
Kwa nini kuna mbegu, na si kiolezo kingine
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.
Njia za kawaida za kughushi ushahidi rasmi hukaguliwa na kukataliwa. Uthibitisho unaoacha shimo na sorry, ambalo huvutia native_decide kufanya zonti hiyo ihesabu juu ya amana, au ile inayoanzisha axiom mpya, hutambuliwa na kukataliwa badala ya kuhesabiwa kuwa mafanikio.
Kile ambacho jopo hilo laweza kufanya
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.
Uthibitisho, si Usemaji
A match hairidhishwi na hali ya kugombana. Dai hilo linavunjwa kuwa masharti ya kukubaliwa, na kanuni ya msingi inaamuliwa tu wakati kitu kilicho nyuma yacho kinaweza kuzuiliwa tena na chama cha tatu: chanzo chenye kifungu cha maana kilichonukuliwa, au msimbo ambao kwa kweli ulitekelezwa kwa matokeo yake halisi. Mrejezeo huo unabaki tena wakati ushahidi wenyewe kabla ya kutawala, na hauwezi kutangaza match imemalizika wakati kanuni hiyo bado iko wazi.
Nyinyi mnajenga msikiti
Omba maoni kamili kuhusu kila wazo lililoelezwa na badala yake uhukumiwe dhidi ya hilo. Omba zawadi ambayo mtaalamu mwenye uangalifu angekubali na upate.
Kusema wazi: Hii si mashine inayosuluhisha matatizo waziwazi.
Kusihihika kusikofaulu ni matokeo yenye mafaa
Wakati Lean hatafunga ithibati, unapata lengo hususa linalobaki. Kwa kawaida, hapo ndipo nafasi ambayo karibu kila mtu angepewa nafasi ya kushambulia, pamoja na kile ambacho tayari kimejaribiwa, na hakuna kitu kingine. Migendo huangushwa wakati imekwama, ikijituliza kabisa; na kupitisha swali moja hususa kwa ajili ya kisehemu.
Kazi ndefu yabaki
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.
Hayawafai kitu
Kituo hiki kimeundwa kwa ajili ya hisabati, mantiki, sayansi ya kinadharia, fizikia ya kinadharia na nadharia ya uchumi mahali ambapo madai yanatatuliwa kwa uthibitisho. Dada yetu referee.chat anaendesha jopo lilelile la jopo-nanchi bila ya Lean kujibu maswali hayo.
referee.chat bustanini wazo lilo hilo, kwa madai ya kibayolojia