Theorem.chat гадоў таму.
Theorem.chat прымае матэматычную заяву і спрабуе яе даказаць. Вы вызначаеце заяву і стандарт, які яна павінна адпавядаць. Панэль мадэляў машыннага навучання - колькі заўгодна, ад якога заўгодна вытворцы - атакуе яе, і яшчэ адна мадэль даказвае яе. Затым аргумент фармалізуецца ў Lean 4 супраць Mathlib, і ядра Lean вырашае, ці даказана яна. Апошні крок - гэта прадукт.
Чаму ядра, а не іншая мадэль
Задайце мадэлі цяжкае пытанне, і вы атрымаеце дакладны адказ, ці правільнае гэтае пытанне. Задайце некалькі пытанняў, і яны часта пагадзяцца, што выглядае як пацверджанне, але не так: мадэлі падзяляюць трэніровачныя дадзеныя і сляпыя кропкі. Другая мадэль, якая правярае першую, усё роўна мае тое ж самае меркаванне, і гэта можна абмеркаваць. Леан ядра не можа. Яно альбо выводзіць сцвярджэнне з аксіём і Mathlib, альбо не робіць гэтага, і давер не ўплывае на вынік.
Звычайныя спосабы фальсіфікацыі формальных доказаў правяраюцца і адхіляюцца. Даказ, які пакідае дзіру ў sorry, які заклікае native_decide да таго, каб ядра прымала вылічэнні на давер, або які ціха ўводзіць новую аксіому, выяўляецца і адхіляецца, а не лічыць як паспяховы.
Што можа рабіць панель
Аргументацыя - гэта танная частка. Панель працуе з літаратурай - arXiv, OpenAlex, Crossref - таму вядомы вынік цытуе, а не перавызначае памылкова. У ёй ёсць SageMath і PARI/GP для вылічэнняў, Z3 і CVC5 для вырашэння SMT, OEIS пошук для выяўлення паслядоўнасці, якую яна пабудавала, і асяроддзе Python без доступу да сеткі. Гіпотэза можа быць праверана супраць дзесяці тысяч выпадкаў, перш чым хто- небудзь правядзе круг, каб паспрабаваць даказаць яе, і кантрапрыклад адразу заканчвае абмеркаванне.
Даказванне, а не гаворка
Суадносіны не ацэньваецца па якасці аргументаў. Справа разбураецца на крытэрыі прыняцця, і крытэрый разглядаецца толькі тады, калі штосьці за ім можа быць перапрацавана трэцяй асобай: крыніца з адпаведным цытаваным пасланнем, або код, які быў рэальна выкананы з рэальным вывадам. Арбітр перапрацуе гэтыя доказы сам перад рашэннем, і ён не можа абвясціць суадносіны завершаным, пакуль крытэрый адкрыты.
Вы ўсталявалі стандарт
Стандарт выбіраецца вамі, і суддзя трымаецца яго літаральна. Спытайцеся, што б прыняў дакладны эксперт, і вы атрымаеце тое, што хочаце. Спытайцеся пра поўны дэдуктыўны аргумент з кожным прадказаннем, і вы будзеце судзіцца супраць гэтага. Спытайцеся пра ступень, з якой сутыкнулася б прэмія, і справядлівы вынік звычайна будзе дакладным апісаннем таго, дзе панель не дасягнула мэты - што каштуе больш, чым упэўненая заява, якую вы павінны праверыць самастойна.
Каб быць дакладным: гэта не машына, якая вырашае адкрытыя задачы. Гэта машына, якая адмаўляецца ад аргумента, калі ён не вырашаны, і якая кажа вам, які крок не атрымаўся.
Нерэалізаванае фармалізаванне з' яўляецца карысным вывадам
Калі Lean не зачыніць доказ, вы атрымаеце дакладную мэту, якая застаецца. На практыцы гэта амаль заўсёды месца, дзе нефармальны аргумент быў рукой - крокам, які кожны, хто чытае версію ў празе, мог бы кінуць галавой. Гэтая мэта пасля гэтага перадаецца таму месцу, якое найбольш падыходзіць для нападу на яе, разам з тым, што ўжо было паспрабавана, і нічога іншага. Мадэлі спыняюцца, калі яны застываюць, перапісваючы сябе на ўсю цану; праходжанне аднаго канкрэтнага пытання замест гэтага звычайна адключае частку знакаў.
Доўгая праца перажывае
Кожная лямма, усталяваная панэллю, трапляе ў агульнадаступны журнал з яе даведкай, таму вынікі запісваюцца адзін раз і ніколі не выводзяцца зноў, а застоі запісваюцца, каб ніхто не вяртаўся да іх. Суадносіны выконваюцца на серверы і прыпыняюцца чыста - на бюджэт, на перабоі з пастаўшчыком або таму, што вы закрылі ўкладку - і працягваюцца ў той жа момант, калі яны спыніліся.
Што гэта не для
Тэарэма - гэта дэдуктыўнае слова. Гэты сайт створаны для матэматыкі, логікі, тэарэтычных камп' ютэрных навук, тэарэтычнай фізікі і эканамічнай тэорыі - галін, дзе патрабаванне вырашаецца доказам. Эмпірычныя пытанні ў біялогіі, медыцыне, хіміі або сацыяльных навуках не ствараюць тэорый, яны ствараюць адкрыцці, і ніякая формалізацыя не вырашыць іх. Наш суседні сайт referee.chat запускае той жа працэс "панэлі і рэферэнта" без кроку Lean, менавіта для гэтых пытанняў.