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.
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
De match pauzeren, er is niets verloren.
Zichtbaarheid
Meld je aan om een match 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.