Diru la aserton. La kerno decidas ĉu ĝi estas pruvita.

Panelo de modeloj atakas vian problemon per la literaturo, SageMath, PARI/GP kaj SMT- solvilo, poste formaligas la rezulton en Lean 4 kontraŭ Mathlib. La kerno de Lean aŭ akceptas la pruvon aŭ ne, kaj neniu kvanto de konfida prozo ŝanĝas tion. Kiam ĝi malsukcesas vi ricevas la ĝustan celon kiu restas, kiu estas kutime kie la neformala argumento estis man- svingado.

La celo
Estu specifa pri kion signifas farita. 'Decidi ĉu X estas vera, kaj pruvi ĝin' estas pli bona ol 'diri al mi pri X'.
La baraĵo kiun ĝi devas forviŝi
La juĝisto tenas tiun ĉi stangon laŭvorte. Petu pruvon pri premionivelo kaj ĝi diros al vi klare, kiam la panelo malsukcesas, anstataŭ deklari venkon.
La panelo
Pli da seĝoj signifas pli da anguloj, kaj pli da kostoj por ĉiu rondo.
Arbitro
Reguloj pri la kriterioj kaj re-kontrolas ĉiun pecon de pruvo. Valoras vian plej fortan modelon.
Rondoj
Limito de elspezo
Frapante ĝin, la ludo estas paŭzita. Nenio estas perdita.
Videbleco
Registriĝu por komenci ludon
La novaj kontoj ricevas komencan krediton, sufiĉe por vera ludo.
@ info

Lean 4 kun Mathlib tipo-kontrolas la finan deklaron, kaj pruvo kiu apogas sur sorry, native_decide aŭ nova aksiomo estas malakceptita anstataŭ kalkulita. Apud ĝi: SageMath, PARI/GP, Z3, CVC5 kaj la OEIS, tiel ke konstruaĵo povas esti kalkulita kaj identigita antaŭ ol iu ajn provas pruvi ion pri ĝi.

Malsukcesa pruvo estas trovaĵo

Kiam formaligo malsukcesas, la celo Lean ne povis fermi estas transdonita al kiu ajn seĝo estas plej bone poziciigita por ataki ĝin: nur tiu celo, ne la tuta historio. Malpermesita pruvo nomas la malplenon precize, kio estas pli ol plej neformalaj argumentoj iam faras.

Nenio estas pruvita dufoje

Ĉiu lemo kiun la panelo kreas iras en komunan libron kun sia pruvo, do ĝi neniam estas re- derivita kaj senfinaj finaĵoj neniam estas reprovataj. Longaj problemoj paŭzas kaj rekomencas sen perdi laboron: fermu la folion kaj reven' u morgaŭ.