Omkring Theorem.chat
Theorem.chat tager en matematisk påstand og forsøger at afvikle det. Du angiver kravet, og standarden det skal opfylde. Et panel af AI modeller ~ så mange som du ønsker, fra hvilke leverandører du ønsker • angriber det, og en anden model dommere. Så argumentet formaliseres i Lean 4 mod Mathlib, og Lean kernel beslutter, om det er bevist. Det sidste skridt er produktet.
Hvorfor en kerne, og ikke en anden model
Spørg en model et svært spørgsmål, og du får et flydende svar, om det er rigtigt. Spørg flere, og de er ofte enige, hvilket føles som bekræftelse og er ikke: modeller deler træningsdata og deler blinde pletter. En anden model, der kontrollerer den første, er stadig den samme slags dom, og det kan tales rundt. Lean kernel ikke. Det enten stammer udsagnet fra aksiomer og Mathlib, eller det gør ikke, og tillid har ingen effekt på resultatet.
De sædvanlige måder at forfalske en formel bevis kontrolleres for og nægtes. Et bevis, der efterlader et hul med sorry, en, der appellerer til native_decide at gøre kernen tage en beregning på tillid, eller en, der roligt indfører et nyt aksiom, opdages og afvises snarere end regnes som en succes.
Hvad panelet kan gøre
Arguing er den billige del. Panelet arbejder med litteraturen ~ arXiv, OpenAlex, Crossref ~ så et kendt resultat er citeret snarere end re-afledt dårligt. Det har SageMath og PARI/GP til beregning, Z3 og CVC5 til SMT løsning, OEIS opslag til at identificere en sekvens, det har konstrueret, og en sandkasse Python miljø uden netværksadgang. En formodning kan testes mod ti tusind tilfælde, før nogen bruger en runde forsøger at bevise det, og et modeksempel slutter diskussionen straks.
Beviser, ikke veltalenhed
En match scores ikke på argumentkvalitet. Påstanden er nedbrudt i acceptkriterier, og et kriterium afgøres først, når noget bag det kan kontrolleres igen af en tredjepart: en kilde med den relevante tekst citeret, eller kode, der faktisk blev udført med sin reelle output. Dommeren re-tjekker, at beviser selv, før de træffer afgørelse, og det kan ikke erklære matchen færdig, mens et kriterium stadig er åbent.
Du sætter baren
Standarden er din at vælge, og dommeren holder det bogstaveligt. Spørg efter, hvad en omhyggelig ekspert ville acceptere, og du får det. Bed om en komplet deduktiv argument med enhver antagelse angivet, og du får bedømt mod det i stedet. Bed om baren en præmie indsendelse ville stå, og det ærlige resultat er normalt en præcis konto, hvor panelet faldt kort! som er mere værd end en sikker påstand, du ville have til at kontrollere dig selv alligevel.
For at være helt klar: Det er ikke en maskine, der løser åbne problemer. Det er en maskine, der nægter at lade et argument passere som afgjort, når det ikke er, og det fortæller dig præcis, hvilket skridt mislykkedes.
En fejlslagen formalisering er den nyttige output
Når Lean ikke vil lukke beviset, får du det nøjagtige mål, der forbliver. I praksis er det næsten altid stedet, hvor det uformelle argument var hånd-bølgende! trin alle læser prosa version ville have nikket forbi. Dette mål er derefter afleveres til hvilken plads er bedst placeret til at angribe det, sammen med hvad der allerede er blevet prøvet, og intet andet. Modeller thrash, når de sidder fast, hvile sig på fuld pris; passerer et specifikt spørgsmål i stedet normalt unblocks for en brøkdel af tokens.
Langt arbejde overlever
Hver lemma panelet etablerer går ind i en delt hovedbog med sin bevis, så resultaterne er skrevet en gang og aldrig re-afledt, og blindgyder registreres, så ingen går tilbage i dem. Matcher køre server-side og pause rent budget, på en udbyder udfald, eller fordi du lukkede fanebladet! og genoptage præcis hvor de stoppede.
Hvad det ikke er til for
Teorem er et deduktivt ord. Dette site er bygget til matematik, logik, teoretisk computer videnskab, teoretisk fysik og økonomisk teori ~ områder, hvor en påstand er afgjort ved bevis. Empiriske spørgsmål i biologi, medicin, kemi eller socialvidenskab ikke producerer teoremer, de producerer resultater, og ingen mængde formalisering vil afgøre dem. Vores søster site referee.chat kører den samme panel-og-referere proces uden Lean trin, for præcis disse spørgsmål.