Сөзіңізді айтыңыз. Өзегі оның дәлелденетінін анықтайды.

Моделдердің панелі сіздің мәселеңізге әдебиеттермен, SageMath, PARI/GP және SMT шешушісімен шабуыл жасайды, содан кейін нәтижесін Lean 4 және Mathlib- ге қарсы формализациялайды. Lean өзегі дәлелдемені қабылдайды немесе қабылдамайды, және ешбір сенімді проза бұл өзгермейді. Егер ол сәтсіз болса, сізге қалған мақсатты, әдетте, бейресми дәлелдеме қолды ысқыру болған жерді көрсетеді.

Мақсат
done дегеннің мағынасын анықтаңыз. 'X дегеннің дұрыс па, жоқ па, анықтап, дәлелдеп 'X туралы айтып бер' дегенді жеңеді.
Тазалау керек жолақ
Арбитраждық судья бұл шамды шын мәнінде ұстайды. Алғашқы дәлелдемені сұраңыз, ол жеңіс туралы жариялау емес, панелдің кемшілігі туралы анық айтатын болады.
Панель
Көп орын - көп бұрыш, бір раундқа көбірек шығын.
Арбитр
Критерий бойынша ережелер мен дәлелдердің әрбірін қайта тексереді. Сіздің ең мықты моделіңізге лайық.
Турлар
Қолдану шегі
Оны басып match-ды тоқтатуға болады. Ештеңе жоғалмайды.
Көрінетіні
match-ды бастау үшін тіркеліңіз
Жаңа шоттар үшін бастапқы кредит, шынайы match-ға жеткілікті.
Қабылданбайтын тексергіш

Lean 4 және Mathlib соңғы шартты тексереді, sorry, native_decide немесе жаңа аксиомаға негізделген дәлелдеу есептелмей, жоққа шығарылады. Оның жанында: SageMath, PARI/GP, Z3, CVC5 және OEIS, сондықтан құрылымы ешкім дәлелдеп көрмес бұрын есептеп, анықтап алуы мүмкін.

Қате дәлелдеу - бұл табылған

Формалдау сәтсіз болғанда, Lean-ның қол жеткізе алмайтын мақсаты оны тоқтатуға ең жақсы орынға беріледі: тек осы мақсат, бүкіл тарих емес. Қабылданбаған дәлелдеу арақашықтықты нақты атайды, бұл көпшілік бейресми аргументтерден гөрі көп.

Ештеңе екі рет дәлелденбейді

Панельдегі әрбір анықталған лемма өзінің дәлелімен бірге ортақ журналға жазылады, сондықтан ол қайтадан шығарылмайды, бітпейтін мәселе қайтадан шешілмейді. Ұзақ уақытқа созылған мәселелер жұмысты жоғалтпай тоқтатылады және қайтадан басталады: қойындыны жабып, ертең қайталаңыз.