Дархости худро гузоред. Ядро қарор медиҳад, ки оё он исбот шудааст.

Панели моделҳо масъалаи шуморо бо адабиёт, SageMath, PARI/GP ва ҳалкунандаи SMT таҳдид мекунад, баъдан натиҷаро дар Lean 4 дар муқобили Mathlib шаклӣ мекунад. Ядрои Lean ё исботро қабул мекунад ё қабул намекунад, ва ҳеҷ миқдори эътимоднокии проза инро тағйир намедиҳад. Вақте ки он ноком мешавад, шумо ҳадафи дақиқро, ки боқӣ мондааст, ки одатан дар он ҷо баҳси ғайрирасмӣ буд, даст- гардондан.

Мақсад
Дар бораи маънои иҷрошуда аниқ бошед. 'Ҳисоб кунед, ки оё X ҳақиқат аст, ва исбот кунед, ки он' мебозад 'ба ман дар бораи X бигӯед.
Панели он бояд тоза карда шавад
Судя ин риштаро дар асл нигоҳ медорад. Барои исботи дараҷаи ҷоиза пурсед ва он ба шумо ба таври равшан мегӯяд, ки оё панел камтар аст, на эълони ғалаба.
Панел
Дар ин ҷо барои дарёфти маълумот ва маълумотҳои бештар ба шумо лозим аст.
Судя
Дар асоси талаботҳо ва аз нав санҷиши ҳар як қисмати далелҳо. Дар ҳақиқат моделҳои шуморо мустаҳкам мекунад.
& Доираҳо
Маҳдудияти хароҷот
Дар вақти пахш кардан match боздошта мешавад. Ҳеҷ чиз гум намешавад.
Дидашаванда
Бақайдгирӣ барои оғози match
New accounts get starting credit, enough for a real match.
Проверка, которая не может быть убеждённой

Lean 4 бо Mathlib санҷиши намуди охиринро мегузаронад, ва исбот, ки ба sorry, native_decide ё аксиомаи нав такя мекунад, ба ҷои ҳисоб кардан рад карда мешавад. Дар канори он: SageMath, PARI/GP, Z3, CVC5 ва OEIS, бинобар ин, сохт метавонад ҳисоб карда шавад ва пеш аз он ки касе кӯшиш кунад, ки ягон чизро дар бораи он исбот кунад, муайян карда шавад.

Доводи нокомӣ як кашф аст

Агар дар ин ҳолат, барои дуруст кардани ин масъала, бояд ба дурустии ин масъалаи дигар диққат дод. Агар ин масъала дуруст бошад, пас, барои дуруст кардани ин масъала, бояд ба дурустии ин масъалаи дигар диққат дод.

Ҳеҷ чиз ду бор исбот намешавад

Ҳар як лиммаи панели муайяншуда дар китоби ҳисоб бо исботи он мегузарад, бинобар ин он ҳеҷ гоҳ аз нав бароварда намешавад ва банди қатъшуда ҳеҷ гоҳ аз нав кӯшиш намешавад. Масъалаҳои дароз бе гум кардани кор боздошта ва идома дода мешаванд: ҷадвалбандиро пӯшед ва фардо бозгардед.