Theorem.chat
Theorem.chat prenas matematikan aserton kaj provas solvi ĝin. Vi diras la aserton, kaj la normon kiun ĝi devas plenumi. Panelo de AI- modeloj - tiom kiom vi volas, de iu ajn vendisto vi volas - atakas ĝin, kaj unu plia modelo juĝas ĝin. Poste la argumento estas formaligita en Lean 4 kontraŭ Mathlib, kaj la Lean- kerno decidas ĉu ĝi estas pruvita. Tiu lasta paŝo estas la produkto.
Kial kerno, kaj ne alia modelo
Demandu al modelo malfacilan demandon kaj vi ricevas fluan respondon ĉu ĝi estas ĝusta aŭ ne. Demandu al pluraj kaj ili ofte konsentas, kio ŝajnas kiel konfirmo kaj ne estas: modeloj kunhavas trejnadon kaj blindajn punktojn. Dua modelo kontrolas la unuan estas ankoraŭ la sama speco de juĝo, kaj ĝi povas esti diskutita. La Lean kerno ne povas. Ĝi aŭ derivas la deklaron el la aksiomoj kaj Mathlib, aŭ ĝi ne faras, kaj konfido ne havas efikon sur la rezulto.
La kutimaj manieroj por falsigi formalan pruvon estas kontrolitaj kaj malakceptitaj. Pruvo kiu lasas truon kun sorry, unu kiu apelaciis al native_decide por fari ke la kerno prenu kalkulon pri fido, aŭ unu kiu silente enkondukas novan aksiomon, estas detektita kaj malakceptita anstataŭ kalkulita kiel sukceso.
Kion la panelo povas fari
Argumentado estas la malmultekosta parto. La panelo laboras kun la literaturo - arXiv, OpenAlex, Crossref - tiel konata rezulto estas citita prefere ol malbone re- derivita. Ĝi havas SageMath kaj PARI/GP por komputado, Z3 kaj CVC5 por SMT solvo, OEIS serĉo por identigi sekvencon kiun ĝi konstruis, kaj sabloŝranka Pitona medio sen retaj aliroj. Konjekto povas esti testita kontraŭ dek mil kazoj antaŭ ol iu ajn pasigas rondiron provante pruvi ĝin, kaj kontraŭekzemplo tuj finas la diskuton.
Evidenco, ne elokventeco
Konkordo ne estas poentata laŭ argumenta kvalito. La aserto estas disigita en akcepto- kriteriojn, kaj kriterio estas solvita nur kiam io malantaŭ ĝi povas esti re- kontrolita de tria partio: fonto kun la koncerna citita paĝo, aŭ kodo kiu estis efektive plenumita kun ĝia reala eligo. La juĝisto re- kontrolas tiun pruvon mem antaŭ juĝado, kaj ĝi ne povas deklari la kongruon finita dum kriterio estas ankoraŭ malfermita.
Vi starigis la baron
La normo estas via por elekti, kaj la juĝisto tenas ĝin laŭvorte. Demandu pri kion zorgema eksperto akceptus kaj vi ricevas tion. Demandu pri kompleta dedukta argumento kun ĉiu supozata deklaro kaj vi estas juĝita kontraŭ tio anstataŭe. Demandu pri la baroj kiujn premio- submeto renkontus, kaj la honesta rezulto estas kutime preciza raporto pri kie la panelo malsukcesis - kio valoras pli ol konfida aserto kiun vi devus kontroli mem ĉiuokaze.
Por esti klara pri tio: tio ne estas maŝino kiu solvas malfermajn problemojn. Ĝi estas maŝino kiu rifuzas lasi argumenton pasi kiel solvita kiam ĝi ne estas, kaj kiu diras al vi precize kiu paŝo malsukcesis.
Malsukcesa formaligo estas la utila eligo
Kiam Lean ne fermas la pruvon, vi ricevas la ĝustan celon kiu restas. Praktike tio estas preskaŭ ĉiam la loko kie la neformala argumento estis man- svingado - la paŝo ĉiu leganta la prozan version estus kliniĝinta antaŭen. Tiu celo estas tiam transdonita al kiu ajn sidloko estas plej bone poziciigita por ataki ĝin, kune kun kio jam estis provita, kaj nenio alia. Modeloj kraŝas kiam ili estas blokitaj, re- esprimante sin je plena kosto; pasigado de specifa demando anstataŭe kutime malblokas por frakcio de la signoj.
Longa laboro supervivas
Ĉiu lemo kiun la panelo starigis iras al komuna libro kun sia pruvo, do rezultoj estas skribitaj unufoje kaj neniam re- derivitaj, kaj senfinaĵoj estas registritaj tiel ke neniu revenas al ili. Konkordoj ruliĝas servile kaj paŭzas pura - je buĝeto, je provizanto- interrompo, aŭ ĉar vi fermis la folion - kaj daŭrigas precize kie ili ĉesis.
Kio tio ne estas por
Teoremo estas dedukta vorto. Tiu retejo estas konstruita por matematiko, logiko, teoria komputiko, teoria fiziko kaj ekonomia teorio - kampoj kie asertoj estas solvita per pruvo. Empiriaj demandoj en biologio, medicino, kemio aŭ sociaj sciencoj ne produktas teoremoj, ili produktas trovojn, kaj neniu kvanto de formaligo decidos ilin. Nia frata retejo referee.chat funkciigas la saman panel- kaj juĝisto- procezon sen la Lean- paŝo, por precize tiuj demandoj.