Jadro rozhodne, či je tvrdenie dokázané, alebo nie.

Panel modelov zaútočí na váš problém s literatúrou, SageMath, PARI/GP a SMT riešiteľom, potom formalizuje výsledok v Lean 4 proti Mathlib. Lean kernel buď akceptuje dôkaz alebo ho neprijíma, a žiadne množstvo sebavedomej prózy to nezmení. Keď zlyhá, dostanete presný cieľ, ktorý zostal, čo je zvyčajne tam, kde neformálny argument bol mávanie rukou.

Cieľ

Buďte konkrétni o tom, čo znamená "Rozhodnite sa, či je X pravdivé a dokážte to" je lepšie ako "povedzte mi o X".

Bar, ktorý musí vyč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.

Požiadajte o dôkaz o úrovni ceny a bude vám jasne povedať, keď panel nedosiahne, skôr ako vyhlásiť víťazstvo.Vyberte si z dvoch možností:

Panel

Viac miest znamená viac uhlov a viac nákladov na kolo.

Rozhodca

Rozhodne o kritériách a znovu skontroluje každý dôkaz, ktorý stojí za váš najsilnejší model.

Kolo

Limit výdavkov

Zasiahnutie pozastaví zápas. Nič nie je stratené.

Viditeľnosť

Publikovať po dokončení

Zaregistrujte sa a začnite zápas

Nové účty dostanú počiatočný kredit, dostatok pre skutočný zápas.

Kontrolór, ktorý sa nedá presvedčiť

Lean 4 s Mathlib kontroluje typ konečného výroku a dôkaz, ktorý sa opiera o sorry, native_decide alebo novú axiómu je zamietnutý namiesto toho, aby bol započítaný.Vedľa neho: SageMath, PARI/GP, Z3, CVC5 a OEIS, takže konštrukcia môže byť vypočítaná a identifikovaná skôr, ako sa niekto pokúsi o jej dokázanie.

Neúspešný dôkaz je nález

Keď formalizácia zlyhá, cieľ, ktorý Lean nedokázal dosiahnuť, je odovzdaný tomu, kto je najlepšie pripravený na jeho napadnutie: len tomuto cieľu, nie celej histórii.Zamietnutý dôkaz presne pomenúva medzeru, čo je viac ako väčšina neformálnych argumentov.

Nič sa nedokazuje dvakrát

Každé lemma, ktoré panel vytvorí, ide do zdieľanej knihy s dôkazom, takže sa nikdy neodvodzuje znova a slepé miesta sa nikdy neskúšajú znova.Dlhé problémy sa pozastavia a pokračujú bez straty práce: zatvorte kartu a vráťte sa zajtra.