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

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.

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

Udariš li ga, meč se zaustavlja.

Vidljivost

Objavi kada završiš

Prijavite se da biste započeli utakmicu

Novi računi dobivaju početni kredit, dovoljno za pravi meč.

Č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.