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

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

Мэта

Вызначце, што азначае дзеянне. 'Вызначце, ці праўдзівы X, і дакажыце гэта' перамагае 'паведаміце мне пра X'.

Паказваць лінію

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.

Арбітр трымае гэты бар літаральна. Запытаеце доказ узроўню прыза і ён паведаміць вам, калі панель не падыходзіць, а не абвяшчае перамогу.

Панель

Большасць з іх — звычайныя вёскі, і толькі некалькі — гарадскія.

Арбітр

Правілы па крытэрах і перапрацаваныя ўсе доказы. Варта вашага найбольш моцнага мадэлі.

Кругі

Абмежаванне выдаткаў

Націск на яе прыпыняе гульню. Нічога не страчана.

Бачнасць

Апублікаваць пасля завяршэння

Зарэгіструйцеся, каб пачаць гульню

Новы рахунак атрымлівае стартавы крэдыт, дастаткова для рэальнага матчу.

Праверка, якую нельга пераканаць

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

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

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

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

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