Noin Theorem.chat
Theorem.chat ottaa matemaattisen väitteen ja yrittää ratkaista sen. Väitös ja vaatimus, joka sen on täytettävä. Valiollinen tekoälymalleja – niin monta kuin haluat, kummalta myyjältä haluat – hyökkää sitä vastaan, ja yksi mallituomari. Sitten väite virallistetaan Lean 4:ssa Mathlib:aa vastaan, ja Lean-ydin päättää, onko se todistettu. Tuo viimeinen askel on tuote.
Miksi ydin, eikä toinen malli
Kysy mallia vaikealla kysymyksellä ja saat sujuvan vastauksen, onko se oikea. Kysy useita, ja he ovat usein samaa mieltä, mikä tuntuu vahvistukselta, eikä ole: mallit jakavat harjoitustietojakavat sokeita pisteitä. Toinen malli, joka tarkistaa ensimmäisen, on edelleen samanlainen arviointi, ja se voidaan puhua ympäri. Lean-ytimen voi joko saada aksioomat ja Mathlib, tai sitten se ei, eikä itseluottamuksella ole vaikutusta lopputulokseen.
Tavanomaiset keinot muodollisen todisteen esittämiseen tarkistetaan ja hylätään. Todiste, joka jättää sorry-kuoppaan, joka vetoaa native_decide:een, jotta ydin saisi laskelmia luottamuksesta tai joka hiljaa tuo uuden aksiooman, havaitaan ja torjutaan sen sijaan, että se katsottaisiin menestykseksi.
Mitä paneeli voi tehdä
Paneeli toimii kirjallisuuden parissa – arXiv, OpenAlex, Crossref – joten tunnettu tulos mainitaan sen sijaan, että se johtaisi uudelleen huonosti. Siinä on SageMath ja PARI/GP laskentaa varten, Z3 ja CVC5 SMT:n ratkaisemista varten, OEIS etsimistä rakentamansa sekvenssin tunnistamiseksi ja hiekkalaatikkoon laitettua Python-ympäristöä, jossa ei ole verkkoyhteyttä. Arveluja voidaan testata kymmenentuhatta tapausta vastaan, ennen kuin kuka tahansa yrittää todistaa sitä, ja vastaesimerkki päättää keskustelun välittömästi.
Todisteita, ei kaunopuheisuutta
Ottelu ei perustu argumentin laatuun, vaan väite hajoaa hyväksymiskriteereihin, ja kriteeri ratkaistaan vasta, kun jokin sen takana oleva asia voidaan tarkistaa uudelleen kolmannen osapuolen toimesta: lähde, jossa on mainittu kohta, tai koodi, joka on todellisuudessa toteutettu sen todellisella tuotoksella. Tuomari tarkistaa uudelleen, että todisteet ovat itse asiassa olemassa ennen tuomion antamista, eikä se voi julistaa ottelua päättyneeksi, kun kriteeri on vielä auki.
Sinä asetit riman
Standardi on sinun, ja erotuomari pitää sitä kirjaimellisesti. Kysy, mitä huolellinen asiantuntija hyväksyisi ja saat sen. Pyydä täydellistä päättelyperustelua, jossa on kaikki esitetyt oletukset, ja saat tuomion sen sijaan. Pyydä baaria, jossa palkintopyyntö kohtaa, ja rehellinen lopputulos on yleensä tarkka selvitys siitä, missä paneelissa oli puutteita – mikä on arvokkaampaa kuin itsevarma väite, jonka sinun pitäisi joka tapauksessa tarkistaa itsesi.
Se on kone, joka ei anna kiistan mennä niin kuin se ei ole, ja se kertoo tarkalleen, mikä askel epäonnistui.
Epäonnistunut virallistaminen on hyödyllinen tulos
Kun Lean ei sulje todisteita, saat tarkan maalin, joka jää jäljelle. Käytännössä se on lähes aina paikka, jossa epävirallinen väittely oli käsien heiluttelua – askel, jonka jokainen proosaversion lukeva olisi nyökytellyt ohi. Tämä tavoite annetaan sille, jolla on parhaat mahdollisuudet hyökätä sitä vastaan, sekä se, mitä on jo kokeiltu, eikä mitään muuta. Mallit puidaan, kun ne ovat jumissa, toistaen itseään täydellä hinnalla, ohittamalla yksi erityinen kysymys sen sijaan yleensä avaamalla esteitä murto-osalla kupongeista.
Pitkä työ selviää
Jokainen paneelin perustama lemma menee yhteiseen tilikirjaan todisteineen, joten tulokset kirjoitetaan kerran eikä niitä koskaan johdeta uudelleen, ja umpikujat kirjataan, joten kukaan ei kävele takaisin niihin. Ottelut kulkevat palvelinpuolella ja pysähtyvät puhtaana – budjetilla, palveluntarjoajan katkaisulla tai koska suljet välilehden – ja jatkat täsmälleen siihen, mihin ne loppuivat.
Mitä varten tämä ei ole?
Teoreemi on päätesana. Sivusto on rakennettu matematiikalle, logiikalle, teoreettiselle tietojenkäsittelytieteelle, teoreettiselle fysiikalle ja talousteorialle – aloille, joilla väite ratkaistaan todisteella. Biologian, lääketieteen, kemian tai yhteiskuntatieteiden empiiriset kysymykset eivät tuota teoreemoja, ne tuottavat tuloksia, eikä mikään muodollisuus ratkaise niitä. Sisarsivusto referee.chat pyörittää samaa paneeli- ja refereeprosessia ilman Lean-vaihetta, juuri näiden kysymysten kohdalla.