Madwar Theorem.chat
Theorem.chat jieħu pretensjoni matematika u tipprova biex jiffissaw dan. Inti jiddikjara l-pretensjoni, u l-istandard li għandu jilħaq. Panil ta AI mudelli — kif ħafna kif inti tixtieq, minn kwalunkwe bejjiegħa inti tixtieq — attakki lilu, u wieħed aktar mudell referees. Imbagħad l-argument huwa formalizzat fil Lean 4 kontra Mathlib, u l-kernel Lean tiddeċiedi jekk huwa ppruvat. Dak l-aħħar pass huwa l-prodott.
Għaliex kernel, u mhux mudell ieħor
Staqsi mudell mistoqsija iebsa u inti tikseb tweġiba fluent jekk jew le huwa dritt. Staqsi diversi u huma spiss jaqblu, li jħoss bħall-korroborazzjoni u mhux: mudelli jaqsmu data taħriġ u jaqsmu blind spots. A mudell tieni iċċekkjar l-ewwel għadu l-istess tip ta ’ġudizzju, u jista’ jitkellem madwar. Il-kernel Lean ma tistax. Hija jew tidderiva l-istqarrija mill-assiomi u Mathlib, jew ma, u l-kunfidenza m’għandha l-ebda effett fuq ir-riżultat.
Il-modi normali biex tiġi ffalsifikata prova formali huma ċċekkjati u rrifjutati.Prova li tħalli toqba ma' sorry, waħda li tappella għal native_decide biex il-kernel jieħu komputazzjoni fuq fiduċja, jew waħda li bil-kwiet tintroduċi assioma ġdida, hija skoperta u rrifjutata minflok ma tingħadd bħala suċċess.
X’jista’ jagħmel il-bord fil-fatt
Il-panel jaħdem bil-letteratura — arXiv, OpenAlex, Crossref — sabiex riżultat magħruf huwa kkwotat minflok ri-derivat ħażin. Hija għandha SageMath u PARI/GP għall-komputazzjoni, Z3 u CVC5 għas-soluzzjoni SMT, OEIS tfittxija għall-identifikazzjoni sekwenza li hija mibnija, u sandboxed Python ambjent mingħajr aċċess netwerk. Konjezzjoni jistgħu jiġu ttestjati kontra għaxar eluf każijiet qabel xi ħadd jqattgħu round jippruvaw jippruvaw dan, u counterexample jintemm id-diskussjoni immedjatament.
Evidenza, mhux eloquence
Match ma jiġix ikkalkulat fuq il-kwalità tal-argumenti, l-argument jiġi maqsum f'kriterji ta' aċċettazzjoni, u kriterju jiġi solvut biss meta xi ħaġa warajh tista' tiġi ċċekkjata mill-ġdid minn parti terza: sors bil-passaġġ rilevanti kkwotat, jew kodiċi li fil-fatt ġie eżegwit bl-output reali tiegħu. Ir-referee jiċċekkja mill-ġdid dik l-evidenza nnifisha qabel ma jiddeċiedi, u ma jistax jiddikjara l-match lest waqt li kriterju jkun għadu miftuħ.
Inti stabbilit bar
L-istandard huwa tiegħek li jagħżlu, u l-referee żżomm litteralment. Staqsi għal dak li espert bir-reqqa se jaċċetta u inti tikseb dak. Staqsi għal argument deduttiv sħiħ ma kull suppożizzjoni ddikjarat u inti tikseb ġudikati kontra dak minflok. Staqsi għall-bar sottomissjoni premju se jiffaċċjaw, u r-riżultat onest huwa normalment kont preċiż ta fejn il-panel waqa qasir — li jiswa aktar minn talba kunfidenti inti jkollok biex tiċċekkja lilek innifsek xorta waħda.
Biex inkun ċar: din mhijiex magna li ssolvi problemi miftuħa, hija magna li tirrifjuta li tħalli argument jgħaddi bħala solvut meta ma jkunx, u li tgħidlek eżattament liema pass falla.
Formalizzazzjoni li ma rnexxietx hija l-output utli
Meta Lean mhux se tagħlaq il-prova, inti tikseb l-għan eżatt li jibqa. Fil-prattika li huwa kważi dejjem il-post fejn l-argument informali kien hand-waving — il-pass kulħadd qari l-verżjoni prosa kien ikollhom nodded passat. Dak l-għan huwa mbagħad mogħtija li kwalunkwe sedil huwa l-aħjar imqiegħda biex jattakkaw dan, flimkien ma dak li diġà ġie ppruvata, u xejn ieħor. Mudelli thrash meta dawn huma mwaħħla, restating ruħhom bi spiża sħiħa; jgħaddu kwistjoni speċifika waħda minflok normalment unblocks għal frazzjoni tal-token.
Xogħol twil jgħix
Kull lemma l-panel tistabbilixxi tmur f'reġistru kondiviż mal-prova tagħha, sabiex ir-riżultati huma miktuba darba u qatt mill-ġdid derivati, u dead ends huma rreġistrati sabiex ħadd jimxi lura fihom. Match run server-ġenb u pawża nadif - fuq il-baġit, fuq waqfien fornitur, jew minħabba li inti magħluqa l-tab - u jerġgħu jibdew eżattament fejn waqfu.
X’inhu dan mhux għal
Teorema hija kelma deduttiva. Dan is-sit huwa mibni għall-matematika, loġika, xjenza teoretika tal-kompjuter, fiżika teoretika u teoria ekonomika — oqsma fejn talba hija solvuta permezz prova. Mistoqsijiet empiriċi fil-bijoloġija, mediċina, kimika jew xjenzi soċjali ma jipproduċux teorema, huma jipproduċu sejbiet, u l-ebda ammont ta formalizzazzjoni se jiddeċiedi minnhom. Is-sit sister tagħna referee.chat tmexxi l-istess panel-and-referee proċess mingħajr il-pass Lean, għal eżattament dawk il-mistoqsijiet.
referee.chat — l-istess idea, għal dikjarazzjonijiet empiriċi