Àkóónú Theorem.chat

Theorem.chat gbayọ̀kà mathematiki àti àwọn ìyànpàrà láti fi hàn. Ò sọ́rọ̀ àwọn ayọ̀kà, àti àwọn ìpèwọ̀n tí o tì ní. Pánẹ́ẹ̀lì àwọn módè́lì AI - bí o tí fẹ́, láti inú gbogbo àwọn oníjádè tí o fẹ́ - tí wọ́ inú o, àti módè́lì kan tí o tí jẹ́ ayọ̀kà. Lẹ́ẹ̀ nínú Lean 4 ní àwọn àkọ́lé àwọn ayọ̀kà tí a tí kọ́ ní àwọn Mathlib, àtì Lean kernel tí o bá yaǹdárà láti mọ́ pé a tí fi hàn. Àwọn àkókò tí o tí n bọ́ ní ayọ̀kà.

Kini idi ti kernel, ati pe kò jẹ́ módè́ẹ̀lì mìíràn

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.

Àwọn ìṣàmúlò-ètò ìṣàfarawé ìpéwọ̀n tí a tíwàn fún ìṣàfihàn ìpéwọ̀n tí a tíwàn fún àwọn ìṣàfihàn. Àwọn ìṣàfihàn tí wọ́n fi ààyè pamọ́ láti sorry, ọkan tí a fi native_decide pamọ́ láti mú kànẹ́lì náà gba àwọn ìṣàmúlò-ètò láti ìdára, tabi ọkan tí a fi àwọn

Àwọn àtòjọ-ẹ̀yàn pánẹ́ẹ̀lì

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.

Àwọn ààyè-iṣẹ́

match kò ní àwọn ààyè nípa ìdáràn àwọn àṣẹ. Àwọn àṣẹ ní pàtó nínú àwọn ìpéwọ̀n ìyànfẹ́, àti àwọn ìpéwọ̀n ní pàtó nígbà tí ohunkohun tí wa nínú rẹ̀ lè fi àwọn ààyè pamọ́ sípàtà kẹtà: àwọn ìṣàfilọ́lẹ̀ nípa àwọn àkọ́lé tí a fi kọ́, tàbí àwọn ìṣàfilọ́lẹ̀ tí a tí ṣe nípa àwọn ààyè tí a tì fi pamọ́. Àwọn ìpéwọ̀n náà fi àwọn ààyè pamọ́ sípàtà kẹtà lọ́wọ́lọ́wọ́ lọ́wọ́lọ́wọ́, àti àwọn ìpéwọ̀n náà kò lè sọ pe match tí pari nígbà tí àwọn ìpéwọ̀n náà tí wa ní pàtó.

Ò fi àwọn ààyè-iṣẹ́ hàn

Ó ní ẹ̀yàn rẹ̀ láti yan, àti àwọn agbẹ̀jọro náà ní ayẹ̀wò. Fẹ̀wọ́lẹ̀ fun ohun tí olórí-ìmọ̀ tí o ní ìbárá tí o fẹ́ gbà, àtí ò gbá. Fẹ̀wọ́lẹ̀ fun àwọn àkọ́lé tí a tí ìṣàfilọ́lẹ̀ nípa gbogbo àwọn à

Lati jẹ́ ayọ̀rọ̀ nípa rẹ̀: yió kò jẹ́ ẹrọ tí o ǹpá ìròyìn àwọn à

Àwọn ìṣàmúlò-ètò tí a kò lè fi pamọ́ nínú àwọn àtòjọ-ẹ̀yàn

Tí Lean kò bá fi àwọn ìṣàfihàn pa, ò gbá àwọn àwọn ààyè tí o tì wa ní. Nínú ìṣàfihàn, ò jẹ́ pé ní gbogbo àkóónú níbi tí àwọn ààyè tí kò ní ìdáràyé jẹ́ - àwọn ààyè tí gbogbo eniyan bá kọ̀ nípa ìṣàfihàn àwọn àkọsílẹ̀ tí a tí sọ̀rọ̀. Àwọn ààyè náà ní a fi pamọ́ sínú àwọn ààyè tí a tí fi pamọ́ láti sàyé, nípa àwọn ààyè tí a tí ṣé, àti àwọn àwọn ààyè tí a kò tì ṣe. Àwọn módè́lì tí wọ́n tí wọ́n tí wọ́n tí wọ́n pamọ́, tí wọn bá sọ́rẹ̀ nípa àwọn

Àwọn iṣẹ́ tí o tí ìgbà

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.

Ohun tí kò bá jẹ́ fun

Téẹ̀mù ní ọrọ̀ deductive. Ààyè yìí tí a kọ̀ fún mathematiki, lògìtì, ìmọ̀ kọ̀ǹpútà tí a ǹṣe, ìṣàfarawé ìṣàfilọ́lẹ̀ tí a ǹṣe, àti àwọn ààyè ékóó - àwọn ààyè tí a tí sọ̀rọ̀ nípa ìṣàfilọ́lẹ̀. Àwọn ààyè àwọn ẹ̀yàn nínú ẹ̀yàn, ilé-ìwosan, kémíràlì tabi àwọn ìmọ̀ awujo kò ṣẹ̀dà téẹ̀mù, wọn ṣẹ̀dá àwọn àwọn ààyè, àti kò si àwọn. Ààyè agbẹ̀gbẹ̀ wa referee.chat ǹlàrà ìṣàmúlò-ètò pánẹ́ẹ̀lì-àti-àjọ-ìsẹ́ kan nípa àkókò Lean, fún àwọn ààyè náà.

referee.chat — àwọn àwòrán tí a tí kọ́, fún àwọn ìṣàfarawé àwọn àṣẹ

Theorem.chat ni a nṣe ni Muddy Holdings LLC. Fi Ìṣàmúlò-ètò pamọ́.