Ange fordran. Kärnan bestämmer om den är bevisad.

En panel av modeller angriper ditt problem med litteraturen, SageMath, PARI/GP och en SMT-lösare, formaliserar sedan resultatet i Lean 4 mot Mathlib. Leans kärna antingen accepterar beviset eller inte, och ingen mängd självsäkra prosa ändrar det. När det misslyckas får du det exakta målet som återstår, vilket är oftast där det informella argumentet var handvred.

Målet

Var specifik om vad gjort betyder. "Beslut om X är sant, och bevisa det" slår "berätta för mig om X".

Baren måste rensas

Var försiktig expert

Vilken kompetent yrkesman skulle acceptera som gjort och korrekt.

Standard för offentliggörande

Skulle överleva peer review: varje påstående som kommer eller härrör, metoder anges, begränsnin…

Formellt bevis

Ett fullständigt avdragsgillt argument. Varje steg rättfärdigas, varje antagande anges, ingen v…

Prisstandard

Baren en Clay Millennium Prize skulle möta: en komplett, fristående, gap-free bevis att expertd…

Beslutsgrad

Tillräckligt med bevis för att agera kommersiellt: alternativ som kostar, risker som nämns, rek…

Skriv mitt eget

Describe your own standard.

Domaren håller denna bar bokstavligen. Be om ett pris-nivå bevis och det kommer att tala klart när panelen inte kommer till korta, snarare än att förklara seger.

Panelen

Fler säten innebär fler vinklar och mer kostnad per runda.

Domare

Regler om kriterierna och kontroll av alla bevis.

Omgångar

Gräns för utgifter

Att slå den pausar match.

Synlighet

Publicera när det är klart

Registrera dig för att starta en match

Nya konton får start kredit, tillräckligt för en riktig match.

En kontroll som inte kan övertygas

Lean 4 med Mathlib typ-kontrollerar det slutliga uttalandet, och ett bevis på att lutar på sorry, native_decide eller en färsk axiom avvisas snarare än räknas. Parallellt med det: SageMath, PARI/GP, Z3, CVC5 och OEIS, så en konstruktion kan beräknas och identifieras innan någon försöker bevisa något om det.

Ett fel är ett fynd

När formaliseringen misslyckas, kan målet Lean inte stängas till vilken plats som helst som är bäst lämpad att attackera den: bara det målet, inte hela historien. Ett förkastat bevis anger gapet exakt, vilket är mer än de flesta informella argument någonsin gör.

Inget bevisas två gånger

Varje lemma panelen etablerar går i en delad liggare med sitt bevis, så det är aldrig åter härledd och återvändsgränder aldrig upprepas. Långa problem pausa och återuppta utan att förlora arbete: stäng fliken och komma tillbaka i morgon.