De kernel beslist of het bewezen is.

Een panel van modellen valt je probleem aan met de literatuur, SageMath, PARI/GP en een SMT-oplosser, formaliseert dan het resultaat in Lean 4 tegen Mathlib. Lean's kernel accepteert ofwel het bewijs of niet, en geen enkele hoeveelheid zelfverzekerde proza verandert dat. Als het mislukt krijg je het exacte doel dat overblijft, dat is meestal waar het informele argument was hand-waaiend.

Het doel

Wees specifiek over wat gedaan betekent. 'Beslis of X waar is, en bewijs het' is beter dan 'Vertel me over X'.

De bar moet leeg.

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.

De scheidsrechter houdt deze bar letterlijk. Vraag om een prijs-niveau bewijs en het zal u duidelijk vertellen wanneer het panel tekort komt, in plaats van de overwinning te verklaren.

Het paneel

Meer stoelen betekent meer hoeken, en meer kosten per ronde.

Scheidingsteken

Regels over de criteria en controleer elk bewijsstuk opnieuw.

Rondes

Maximum uitgaven

Als je hem raakt, is er niets verloren.

Zichtbaarheid

Publiceren als het klaar is

Meld je aan om een overeenkomst te starten

Nieuwe rekeningen krijgen krediet, genoeg voor een echte match.

Een controler die niet kan worden overgehaald

Lean 4 met Mathlib type-checks de definitieve verklaring, en een bewijs dat leunt op sorry, native_decide of een vers axioma wordt afgewezen in plaats van geteld. Daarnaast: SageMath, PARI/GP, Z3, CVC5 en de OEIS, zodat een constructie kan worden berekend en geïdentificeerd voordat iemand probeert om iets te bewijzen.

Een mislukt bewijs is een bevinding

Wanneer de formalisering mislukt, wordt het doel dat Lean niet kon sluiten, aan de beste plek gegeven om het aan te vallen: juist dat doel, niet de hele geschiedenis. Een afgewezen bewijs noemt precies de kloof, die meer is dan de meeste informele argumenten ooit doen.

Niets is tweemaal bewezen.

Elke lema die het panel vaststelt gaat in een gedeeld grootboek met zijn bewijs, dus het wordt nooit opnieuw afgeleid en dode eindjes worden nooit opnieuw opgepakt. Lange problemen pauzeren en hervatten zonder werk te verliezen: sluit de tab en kom morgen terug.