Ca. Theorem.chat
Theorem.chat tar et matematisk krav og forsøker å gjøre opp det. Du oppgir kravet, og standarden det må møte. Et panel av AI- modeller – så mange du vil, fra hvilke leverandører du vil – angriper det, og en til modelldommer. Så formaliseres argumentet Lean 4 mot Mathlib, og Lean- kjernen bestemmer om det er bevist. Det siste trinnet er produktet.
Hvorfor en kjerne, og ikke en annen modell
Spør en modell et vanskelig spørsmål og du får et flytende svar om det er riktig eller ikke. Spør flere og de er ofte enige, som føles som bekreftelse og ikke er: modeller deler treningsdata og deler blinde flekker. En annen modell som sjekker den første er fremdeles den samme typen skjønn, og den kan snakkes rundt. Det kan ikke være slik at Lean- kjernen enten får utsagnet fra aksiomene og Mathlib, eller det gjør det ikke, og tilliten har ingen innvirkning på utfallet.
Den vanlige måten å fuske et formelt bevis på blir sjekket og nektet. Et bevis som etterlater et hull med sorry, et bevis som appellerer til native_decide for å få kjernen til å ta en beregning på tillit, eller et bevis som stille innfører et nytt aksiom, blir oppdaget og forkastet i stedet for å telle som en suksess.
Hva panelet kan gjøre
Arguing er den billige delen. Panelet arbeider med litteraturen – arXiv, OpenAlex, Crossref – så det siteres et kjent resultat i stedet for å hente feil. Det har SageMath og PARI/GP for beregning, Z3 og CVC5 for SMT- løsning, OEIS oppslag for å identifisere en sekvens den har laget, og et Python- miljø i sandkasse uten nettverkstilgang. En formodning kan testes mot ti tusen tilfeller før noen forsøker å bevise det, og et moteksempl avslutter diskusjonen umiddelbart.
Bevis, ikke verdifastsettelse
En scoret scoret ikke på argumentkvalitet. Kravet blir degradert til godkjenningskriterier, og et kriterium gjøres bare opp når noe bak det kan kontrolleres på nytt av en tredjemann: en kilde med den oppgitte teksten, eller en kode som faktisk ble utført med dens virkelige utdata. Referent kontrollerer på nytt det beviset selv før han traff, og kan ikke erklære funnet ferdig mens et kriterium fremdeles er åpent.
Du setter linja
Standarden er din å velge, og referansen holder det bokstavelig. Spør etter hva en forsiktig sakkyndig ville godta og du får det. Spør etter et fullstendig deduktivt argument med hver antakelse som er oppgitt og du blir dømt mot det i stedet. Spør etter baren en premie innsending ville stå overfor, og det ærlige resultatet er vanligvis en nøyaktig redegjørelse for hvor panelet ble kort — som er mer verdt enn et sikkert krav du måtte sjekke deg selv likevel.
For å være klar over det: dette er ikke en maskin som gjør opp åpne problemer. Det er en maskin som nekter å la et argument gå over når den ikke er avgjort, og det forteller deg nøyaktig hvilket steg som mislyktes.
En feilet formalisering er den nyttige utdataen
Når Lean ikke vil lukke beviset får du det nøyaktige målet som gjenstår. I praksis er det nesten alltid stedet der det uformelle argumentet var for hånd- våkning – det steget alle leser prosa- versjonen ville ha nikket fortiden. Det målet blir da levert til det stedet som er best egnet til å angripe det, sammen med det som allerede er prøvd, og ikke noe annet. Modeller tråkker ut når de sitter fast, og gjenopptar seg selv til full kostnad. Det passerer et bestemt spørsmål i stedet for å fjerne blokker for en brøk av symbolene.
Langt arbeid overlever
Hver lemma panelet etablerer går inn i en delt leder med sine beviser, så resultatene skrives en gang og aldri re-deriveres, og døde ender registreres så ingen går tilbake inn i dem. Passer kjører tjenersiden og pauser rent – på budsjett, på en leverandør utgang, eller fordi du lukket fanen – og gjenopptar nøyaktig hvor de stoppet.
Hva dette ikke er til
Teorem er et deduktiv ord. Dette nettstedet er bygget for matematikk, logikk, teoretisk datavitenskap, teoretisk fysikk og økonomisk teori – felt der påstander avklares med bevis. Empiriske spørsmål i biologi, medisin, kjemi eller samfunnsvitenskap produserer ikke teoremer, de produserer funn, og ingen formalisering vil avgjøre dem. Vår søsters nettsted referee.chat driver samme panel- og- refere- prosess uten Lean- trinnet, for akkurat disse spørsmålene.