Izrecite tvrdnju.

Panel modela napada vaš problem sa literaturom, SageMath, PARI/GP i SMT rješavačem, zatim formalizira rezultat u Lean 4 protiv Mathlib. Lean-ov kernel ili prihvaća dokaz ili ne, i nikakva količina pouzdane proze to ne mijenja. Kad ne uspije, dobijete tačan cilj koji ostaje, što je obično gdje je neformalni argument bio mazanje rukom.

Cilj
Budite konkretni o tome šta znači "Odluči da li je X istina i dokaži da je" bolje od "Pričaj mi o X".
Bar mora da se očisti
Sudija doslovno drži štap, zatražite dokaz na nivou nagrade i jasno će vam reći kada panel ne uspije, umjesto da proglasi pobjedu.
Panel
Više sjedala znači više uglova i više troškova po rundi.
Sudija
Pravila o kriterijima i ponovno provjerava svaki dokaz vrijedan vašeg najjačeg modela.
Rounds
Limit potrošnje
Pogodim li ga, zaustavit će se match.
Vidljivost
Prijavite se da pokrenete match
Novi računi dobivaju početni kredit, dovoljno za pravih match.
Ček koji se ne može uvjeriti

Lean 4 sa Mathlib tip-provjera završne izjave, i dokaz koji se oslanja na sorry, native_decide ili novi aksiom je odbačen umjesto brojanja. Pored njega: SageMath, PARI/GP, Z3, CVC5 i OEIS, tako da se konstrukcija može izračunatidentificirati prije nego što neko pokuša dokazati bilo šta o tome.

Neuspjeli dokaz je otkriće.

Kada formalizacija ne uspije, cilj koji Lean nije mogao zatvoriti se predaje onome koji je najbolje pozicioniran da ga napadne: samo taj cilj, a ne cijela historija.Odbačeni dokaz precizno imenuje jaz, što je više nego što većina neformalnih argumenata ikada učini.

Ništa se ne dokazuje dvaput.

Svaka lema koju panel ustanovi ide u zajedničku knjigu sa svojim dokazom, tako da se nikad ne izvodi iznova i slijepe točke se nikad ne pokušavaju. Dugi problemi se pauziraju i nastavljaju bez gubitka rada: zatvorite karticu i vratite se sutra.