Задайце заяву. Ядро вырашае, ці даказана яна.

Панель мадэляў атакуе вашу праблему з літаратурай, SageMath, PARI/GP і рашальнікам SMT, затым фармалізуе вынік у Lean 4 супраць Mathlib. Ядро Lean альбо прымае доказ, альбо не, і ніякая колькасць упэўненай празы не змяняе гэта. Калі ён не паспяхова, вы атрымліваеце дакладную мэту, якая застаецца, якая звычайна была нефармальным аргументам.

Мэта
Вызначце, што азначае дзеянне. 'Вызначце, ці праўдзівы X, і дакажыце гэта' перамагае 'паведаміце мне пра X'.
Паказваць лінію
Арбітр трымае гэты бар літаральна. Запытаеце доказ узроўню прыза і ён паведаміць вам, калі панель не падыходзіць, а не абвяшчае перамогу.
Панель
Большасць з іх — звычайныя вёскі, і толькі некалькі — гарадскія.
Арбітр
Правілы па крытэрах і перапрацаваныя ўсе доказы. Варта вашага найбольш моцнага мадэлі.
Кругі
Абмежаванне выдаткаў
Націск на яе прыпыняе гульню. Нічога не страчана.
Бачнасць
Зарэгіструйцеся, каб пачаць гульню
Новы рахунак атрымлівае стартавы крэдыт, дастаткова для рэальнага матчу.
Праверка, якую нельга пераканаць

Lean 4 з Mathlib правярае тып канчатковага выказвання, і доказ, які грунтуецца на sorry, native_decide або на новай аксіоме, адхіляецца, а не лічыцца. Паблізу ад яго: SageMath, PARI/GP, Z3, CVC5 і OEIS, так што канструкцыя можа быць вылічана і вызначана, перш чым хто- небудзь паспрабуе даказаць што- небудзь пра яе.

Недакладнае даказанне - гэта знаходка

Калі формалізацыя не атрымліваецца, мэта, якую Lean не можа зачыніць, перадаецца таму, хто найлепш падыходзіць для яе атакі: толькі гэтай мэты, а не ўсёй гісторыі. Адхіленае даказанне называе прабел дакладна, што больш, чым большасць нефармальных аргументаў.

Нішто не даказваецца два разы

Кожная лямма, усталяваная панеллю, трапляе ў агульнадаступны журнал з яе даведкай, таму яна ніколі не выводзіцца зноў і застоі ніколі не спрабуюць зноў. Доўгія задачы прыпыняюцца і працягваюцца без страты працы: закрыць картку і вярнуцца заўтра.