Ytimen päätös on, onko se todistettu.

Mallipaneeli hyökkää ongelmasi kimppuun kirjallisuuden, SageMath, PARI/GP ja SMT:n ratkaisijan kanssa, sitten virallistaa tuloksen Lean 4 Mathlib vastaan. Laihon ydin joko hyväksyy todisteet tai ei hyväksy niitä, eikä mikään varma proosa muuta sitä. Kun se ei onnistu, saat tarkan tavoitteen, joka jää jäljelle, eli yleensä epävirallinen argumentti oli käsin heiluva.

Tavoite
"Päättäkää, onko X totta ja todistakaa, että se voittaa, kertokaa X:stä."
Baari täytyy tyhjentää
Tuomari pitää tätä rimaa kirjaimellisesti. Pyydä palkintotasoista todistetta, niin se kertoo selvästi, milloin paneeli ei onnistu, sen sijaan että julistaisi voittoa.
Paneeli
Lisää istuimia lisää kulmat, ja enemmän kustannuksia per kierros.
Tuomari
Kriteerejä koskevat säännöt ja todistusaineiston uudelleentarkastus ovat vahvimman mallisi arvoisia.
Kierros
Kulutusraja
Jos osumme siihen, match pysähtyy.
Näkyvyys
Ilmoittaudu aloittaaksesi match
Uusilla tileillä saa luottoa, joka riittää todelliseen match:een.
Tarkastaja, jota ei voi suostutella

Lean 4, jossa on Mathlib tyyppitarkastusta loppulausunnon, ja todiste, joka nojaa sorry, native_decide tai tuoreeseen aksioomiin, on hylätty sen sijaan, että se laskettaisiin. Sen lisäksi: SageMath, PARI/GP, Z3, CVC5 ja OEIS, niin rakennus voidaan laskea ja tunnistaa, ennen kuin kukaan yrittää todistaa siitä mitään.

Epäonnistunut todiste on havainto

Kun virallistaminen epäonnistuu, Lean ei päässyt lähellekään, vaan sille, jolla on parhaat mahdollisuudet hyökätä, annetaan vain tuo tavoite, ei koko historia. Hylätty todiste osoittaa aukon tarkasti, mikä on enemmän kuin epävirallisimmat väitteet koskaan.

Mitään ei ole todistettu kahdesti

Jokainen paneelin perustama lemma menee todisteineen yhteiseen tilikirjaan, joten sitä ei koskaan johdeta uudelleen eikä umpikujaa koskaan yritetä uudelleen. Pitkät ongelmat taukoavat ja jatkuvat ilman, että työ loppuu: sulje välilehti ja palaa huomenna.