Oko Theorem.chat.
Theorem.chat uzima matematičku tvrdnju i pokušava je riješiti. Vi navodite tvrdnju i standard koji ona mora zadovoljiti. Panel modela AI - koliko god želite, od bilo kojeg prodavca koji želite - napada ga, i još jedan model sudi. Onda se argument formalizira u Lean 4 protiv Mathlib, i Lean kernel odlučuje da li je dokazan. Taj zadnji korak je proizvod.
Zašto jezgro, a ne neki drugi model
Pitajte model teško pitanje i dobit ćete tečni odgovor da li je točno ili ne. Pitajte nekoliko i oni se često slažu, što se osjeća kao potvrda a nije: modeli dijele podatke o obuci i dijele slijepe tačke. Drugi model koji provjerava prvi je još uvijek ista vrsta prosudbe, i može se pričati oko toga. Lean kernel ne može. On ili izvodi izjavu iz aksioma i Mathlib, ili ne, i povjerenje nema efekta na ishod.
Uobičajeni načini za lažno formalno dokazivanje su provjereni i odbijeni.Dokaz koji ostavlja rupu sa sorry, jedan koji apelira na native_decide da navede kernel da izvrši računanje na povjerenje, ili jedan koji tiho uvodi novi aksiom, je otkriven i odbijen umjesto da se računa kao uspjeh.
Šta panel zapravo može da uradi
Rasprava je jeftiniji dio. Panel radi sa literaturom - arXiv, OpenAlex, Crossref - tako da se poznati rezultat citira umjesto da se loše ponovno izvodi. Ima SageMath i PARI/GP za računanje, Z3 i CVC5 za SMT rješavanje, OEIS pretraživanje za identifikaciju sekvence koju je konstruirao, i Python okruženje u sandboxu bez mrežnog pristupa. Pretpostavka se može testirati protiv deset hiljada slučajeva prije nego što neko potroši krug pokušavajući je dokazati, a protivprimjer odmah završava raspravu.
Dokazi, a ne govorništvo.
Podudarnost se ne ocjenjuje po kvaliteti argumenta. Tvrdnja se rastavlja na kriterije prihvaćanja, a kriterij se rješava samo kada nešto iza njega može biti ponovno provjereno od strane treće strane: izvor s relevantnim citatom, ili kod koji je stvarno izvršen sa svojim stvarnim izlazom. Sudija ponovno provjerava dokaze prije odlučivanja, i ne može proglasiti podudarnost završenom dok je kriterij još uvijek otvoren.
Ti si postavio standard
Standard je na vama da odaberete, a sudac ga drži doslovno. Pitajte za ono što bi pažljivi stručnjak prihvatio i vi to dobijete. Pitajte za potpuni deduktivni argument sa svakom pretpostavkom koja je navedena i vi ćete biti suđeni protiv toga umjesto toga. Pitajte za bar nagrade bi se suočio, i pošteni ishod je obično precizan račun gdje panel nije bio dobar - što vrijedi više od samouvjerene tvrdnje koju biste ionako morali sami provjeriti.
Da budemo jasni: ovo nije mašina koja rješava otvorene probleme. To je mašina koja odbija da argument prođe kao riješen kada nije, i koja vam tačno kaže koji korak nije uspio.
Neuspjela formalizacija je korisni rezultat
Kada Lean ne zatvori dokaz, dobijete tačan cilj koji ostaje. U praksi to je skoro uvijek mjesto gdje je neformalni argument bio mazanje rukom - korak koji bi svi koji čitaju proznu verziju prošli kimom. Taj cilj se onda predaje na bilo koje sjedalo koje je najbolje pozicionirano da ga napada, zajedno sa onim što je već pokušano, i ništa drugo. Modeli se tresu kada su zaglavljeni, ponavljajući se po punoj cijeni; prolazeći jedno specifično pitanje umjesto toga obično otključava za djelić žetona.
Dugi rad preživljava
Svaka lema koju panel ustanovi ide u zajedničku knjigu sa svojim dokazom, tako da su rezultati napisani jednom i nikad se ne izvode ponovo, a mrtvi krajevi se bilježe tako da se niko ne vraća u njih. Podudarnosti se izvode na serveru i pauziraju čisto - na budžetu, na prekidu pružatelja ili zato što ste zatvorili karticu - i nastavljaju se tačno tamo gdje su stali.
Za šta ovo nije?
Teorem je deduktivna riječ. Ova stranica je napravljena za matematiku, logiku, teorijsku računarsku nauku, teorijsku fiziku i ekonomsku teoriju - polja gdje se tvrdnja rješava dokazom. Empirijska pitanja u biologiji, medicini, hemiji ili društvenim naukama ne proizvode teoreme, oni proizvode otkrića, i nikakva količina formalizacije neće ih odlučiti. Naša sestrinska stranica referee.chat pokreće isti proces panela i ocjenjivača bez Lean koraka, za upravo ta pitanja.