Theorem.chat ҳақида
Theorem.chat математик даъвони қабул қилади ва уни ҳал қилишга уринади. Сиз даъво ва унинг жавоб бериши керак бўлган стандартни кўрсатасиз. AI моделлари панели - хоҳлаганингизча кўп, хоҳлаганингизча сотувчидан - унга ҳужум қилади, яна бир модел судя. Сўнгра аргумент Lean 4 га қарши Mathlib да формаллаштирилади, ва Lean ядроси унинг исботланишини ҳал қилади. Бу охирги қадам маҳсулотдир.
Нима учун бошқа модел ўрнига ядровий тизим
Модельга қийин савол беринг ва тўғри ёки нотўғрилиги ҳақида аниқ жавоб оласиз. Кўплаб савол беринг ва улар кўпинча рози бўладилар, бу тасдиқлашдек туюлади, лекин бу шундай эмас: моделлар ўқитиш маълумотларини ва кўр нуқталарни алмашадилар. Биринчисини текширадиган иккинчи модел ҳамон шу турдаги ҳукмдир, ва бу ҳақида гапириш мумкин. Lean ядроси буни қила олмайди. У ёки аксиомалар ва Mathlibдан хулоса чиқаради, ёки чиқармайди, ва ишонч натижага таъсир қилмайди.
Формал исботни сохталаштиришнинг оддий йўллари текширилади ва рад этилади. sorry билан бўшлиқ қолдирадиган исбот, native_decideга мурожаат қилиб, ядрони ишончли ҳисоблашни қабул қилишга мажбур қиладиган исбот ёки жимгина янги аксиотимни киритадиган исбот аниқланадиган ва муваффақият сифатида ҳисобланмасдан рад этиладиган исботдир.
Панелнинг нима қилиши мумкинлиги
Тақдимотлар арзон қисмидир. Панел адабиётлар билан ишлайди - arXiv, OpenAlex, Crossref - шунинг учун маълум натижани яхшилаб қайта ишлаб чиқиш ўрнига, маълум натижани келтириш мумкин. У ҳисоблаш учун SageMath ва PARI/GP, SMT ечими учун Z3 ва CVC5, у қурган кетма-кетликни аниқлаш учун OEIS қидирув ва тармоқга кириши бўлмаган sandbox Python муҳитига эга. Тахминни исботлаш учун бирор киши бир дақиқа сарфламасдан, ўн мингта ҳолатга қарши текширилиши мумкин, ва қарши мисол муҳокамани тезда тугатади.
Ҳужжат, сўзлашув эмас
match аргумент сифати бўйича баҳоланмайди. Даъво қабул қилиш мезонларига бўлинади ва мезон фақат учинчи томон томонидан қайта текширилгандагина ҳал этилади: манбада зарурий парча келтирилган ёки кодда унинг ҳақиқий чиқиши билан амалга оширилган. Арбитр ҳукм чиқаришдан олдин ўз исботини қайта текширади ва у критерий очиқ бўлганда match тугаганини эълон қила олмайди.
Сиз белгилаган
Стандарт сизнинг танловингиз ва ҳакам буни сўзма-сўз ифодалайди. Экспертнинг қабул қилиши мумкин бўлган нарсани сўранг ва сиз буни оласиз. Ҳар бир тахмин билан тўлиқ дедуктив аргументни сўранг ва сиз бунинг ўрнига бунга қарши ҳукм қилинасиз. Ғолиблик учун тақдим этилган материаллар учун талаб қилинадиган даражани сўранг ва ҳаққоний натижа одатда панелнинг камчиликларини аниқ ҳисоблайди - бу сиз ўзингиз текшириши керак бўлган ишончли даъводан кўра кўпроқ фойдали.
Бу ҳақда очиқ гапирадиган бўлсак: бу очиқ муаммоларни ҳал қиладиган машина эмас. Бу масала ҳал қилинмаганда, бир баҳсни ҳал қилинган деб қабул қилишдан бош тортадиган машинадир ва бу сизга қайси қадам хато бўлганини аниқ айтади.
Бузилувчи формализация фойдали чиқинди
Агар Lean исботни ёпмаса, сиз қолган аниқ мақсадни оласиз. Амалдаги ҳолатда бу ҳар доим норасмий баҳс қўл силкитиш билан тугайди - бу қадамни ҳар ким ҳам шеър вариантини ўқиб, бошини эгиб ўтиб кетади. Бу мақсад кейинчалик уни зарба бериш учун энг яхши жойга топширилади, шунингдек, бошқа ҳеч нарса йўқ, фақатгина ҳозиргача синалган нарсалар. Модельлар тўхтаб қолганда, ўзларини тўлиқ қийматда қайта тақдим этишади; бирор бир саволни топшириш эса, одатда, чекловни чекланган очколар учун олиб ташлайди.
Умумий иш сақланиб қолади
Панел томонидан яратилган ҳар бир lemma унинг исботи билан биргаликда ўртоқлашилган китобга киради, натижа бир марта ёзилади ва ҳеч қачон қайта келтирилмайди, ва тўхтаб қолганлар қайд этилади, ҳеч ким уларни қайтадан бошламайди. Matches сервер томонида ишлайди ва тоза ўчириш - бюджет, провайдер узилиши ёки сиз тугмани ёпганингиз учун - ва улар тўхтаган жойдан давом эттирилади.
Бу нима учун эмас
Теорема - бу дедуктив сўз. Бу сайт математика, мантиқ, назарий компьютер фани, назарий физика ва иқтисодий назария учун яратилган - далиллар билан исботланган соҳалар. Биология, тиббиёт, кимё ёки ижтимоий фанлардаги эмпирик саволлар теоремаларни келтириб чиқармайди, улар топилмаларни келтириб чиқаради ва ҳеч қандай формаллаштириш уларни ҳал қилмайди. Бизнинг опа-сингил сайтимиз referee.chat ҳам худди шу саволлар учун Lean қадамисиз бир хил панел-рефери жараёнини бажаради.