Adierazi aldarrikapena. Nukleoak erabakitzen du frogatuta dagoen ala ez.

Eredu-panel batek zure arazoa literaturarekin, SageMath, PARI/GP eta SMT ebazle batekin erasotzen du, eta ondoren emaitza Lean 4an formalizatzen du Mathlibren aurka. Lean-en kernelak frogapena onartzen du edo ez, eta ez du ezer aldatzen. Huts egiten duenean, geratzen den helburu zehatza lortzen duzu, normalean argudio informala eskua mugitzen ari zen lekuan.

Helburua

Zehaztu eginak zer esan nahi duen. 'X egiazkoa den erabaki eta frogatu' hobeto da 'Xri buruz hitz egin' baino.

Garbitu behar duen barra

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.

Epaileak barra hori literalki eusten du. Eskatu sari-maila froga bat eta argi eta garbi esango dizu panela gutxiegi denean, garaipena aldarrikatu ordez.

Panela

Eserleku gehiagok angelu gehiago esan nahi du, eta kostu gehiago bira bakoitzeko.

Epaile

Irizpideak arautzen ditu eta froga guztiak berriro aztertzen ditu. Zure eredurik indartsuena balio du.

Rounds

Gastu-muga

Jotzen baduzu partida gelditzen da. Ez da ezer galdu.

Ikusgaitasuna

Argitaratu bukatzean

Erregistratu partida bat hasteko

Kontu berriek kreditu bat dute, benetako partida bat egiteko nahikoa.

Konbentzitu ezin daitekeen egiaztatzailea

Lean 4 eta Mathlib-k azken adierazpena egiaztatzen dute, eta sorry, native_decide edo axioma berri batean oinarritutako froga bat baztertu egiten da zenbatu beharrean. Horren ondoan: SageMath, PARI/GP, Z3, CVC5 eta OEIS, beraz, eraikuntza bat kalkulatu eta identifikatu daiteke inork horri buruz ezer frogatzen saiatu aurretik.

Egiaztapen huts bat aurkitu bat da.

Formalizazioak huts egiten duenean, Lean-ek itxi ezin zuen helburua erasotzeko posiziorik onena duen eserlekura pasatzen da: helburu hori bakarrik, ez historia osoa. Errefusatutako froga batek hutsunea zehazki izendatzen du, argudio informal gehienek inoiz egiten dutena baino gehiago.

Ez da ezer bi aldiz frogatzen.

Panelak ezartzen duen lema bakoitza, bere frogapenarekin batera, liburu partekatu batean sartzen da, beraz, ez da inoiz berriro deribatzen eta ez da inoiz geldirik dauden puntuak berriro saiatzen. Arazo luzeak gelditu eta lan egin gabe jarraitzen dira: itxi fitxa eta itzuli bihar.