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ää

Careful expert

What a competent professional in the field would accept as done and correct.

Publication standard

Would survive peer review: every claim sourced or derived, methods stated, limitations acknowle…

Formal proof

A complete deductive argument. Every step justified, every assumption stated, no appeals to pla…

Prize standard

The bar a Clay Millennium Prize submission would face: a complete, self-contained, gap-free pro…

Decision-grade

Enough evidence to act on commercially: options costed, risks named, recommendation justified.

Write my own

Describe your own standard.

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

Mikään ei mene hukkaan, jos lyöminen pysäyttää ottelun.

Näkyvyys

Julkaise kun olet valmis

Rekisteröidy aloittaaksesi ottelun

Uusilla tileillä saa aloitusluottoa, joka riittää todelliseen otteluun.

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.