About Theorem.chat
Theorem.chat математикалык талапты кабыл алып, аны чечүүгө аракет кылат. Сиз талапты жана анын жооп бериши керек болгон стандартты көрсөтөсүз. AI моделдеринин панели - каалаганыңызча, каалаган сатуучудан - ага чабуул жасайт, жана дагы бир модель рефери. Андан кийин аргумент Lean 4 менен Mathlib ортосунда формалдаштырылат, жана Lean ядрасы аны далилдөөгө чечим кабыл алат. Акыркы кадам продукт.
Эмне үчүн башка моделге эмес, өзөккө
Моделге кыйын суроо берип, туура же туура эмес деген жоопту тез табасыз. Бир нече суроо берип, алар көп учурда макул болушат, бул коррекция катары сезилет, бирок чындыгында андай эмес: моделдер машыгуу маалыматтарын жана көз жумган жерлерди бөлүшөт. Биринчисин текшерген экинчи модель дагы эле ошол эле түрдөгү чечим, аны айланасында сүйлөшүүгө болот. Леан ядрасы муну жасай албайт. Ал же аксиомалардан жана Mathlibден билдирүүнү алып келет, же ал эмес, жана ишеним натыйжага таасирин тийгизбейт.
Формалдуу далилди жасалмалоонун адаттагы жолдору текшерилип, алардын бардыгы четке кагылат. sorry менен тескери байланышы бар далилдер, native_decideге кайрылып, ядронду ишенимдүү эсептөөгө мажбурлаган далилдер, же жаңы аксиоманы ачыкка чыгарбаган далилдер табылып, ийгилик катары эсептелбей, четке кагылат.
Панелдин чыныгы аткара ала турган иштери
Аргументация - это дешёвый вариант. Панель работает с литературой - arXiv, OpenAlex, Crossref - поэтому известный результат цитируется, а не плохо переоткрывается. Она имеет SageMath и PARI/GP для вычислений, Z3 и CVC5 для SMT решения, OEIS поиск для идентификации последовательности, которую она построила, и песочную среду Python без доступа к сети. Предположение может быть проверено против десяти тысяч случаев до того, как кто-то потратит раунд на его доказательство, и контрапример немедленно завершает дискуссию.
Экспертиза, лексика эмес
Соответствие не оценивается по качеству аргументов. Заявление разбивается на критерии принятия, и критерий рассматривается только тогда, когда за ним что-то может быть проверено третьей стороной: источник с соответствующим цитатом, или код, который был выполнен с его реальным выходом. Рефери проверяет доказательства до вынесения решения, и не может объявить соответствие законченным, пока критерий открыт.
Сиздин чен
Стандартты сиз тандайсыз, жана арбитр аны сөзмө-сөз карманат. Эксперттин кабыл ала турган стандартын сураңыз, жана сиз ал стандартты аласыз. Ар бир болжол менен толук дедуктивдик аргументти сураңыз, жана сиз анын ордуна аны менен соттолушуңуз керек. Баардык баалуу сыйлыктарды тапшыруу үчүн баррель сураңыз, жана чынчыл жыйынтык, адатта, панелдин кайсы жеринде жетишсиз болгонун так баяндайт - бул ишенимдүү билдирүүдөн көбүрөөк баалуу, сиз өзүңүздү өзүңүз текшеришиңиз керек.
Бул ачык маселелерди чечүүчү машина эмес. Бул машина ар бир аргументти чечилген деп кабыл алуудан баш тартат, эгер ал чечилген эмес болсо, жана кайсы кадам ийгиликсиз болгонун так айтат.
Формалдаштыруу жаңылыштык менен аяктады
Эгерде Lean далилди жаббаса, анда сиз так максатты табасыз. Практикада бул ар дайым формалсыз аргументтин колун сунуп жаткан жери - бул кадам, аны окуган ар бир адам прозалык версияны окуп бүткөндөн кийин, баш ийүү менен жактырышы мүмкүн. Бул максат андан кийин аны чабуул жасоо үчүн эң жакшы орунга өткөрүлөт, буга чейин аракет кылынган нерселер менен бирге, башка эч нерсе жок. Моделдер, алар тыгылып калганда, өздөрү толук баада кайрадан айтып беришет; бир гана конкреттүү суроону тапшыруу, адатта, блоктоону бир аз чектөө менен алып салат.
Узак иш сакталат
Панель түзгөн ар бир лемма өз далили менен биргелешкен журналга кирет, ошондуктан натыйжалар бир жолу жазылып, кайрадан чыгарылбайт, жана бүтпөгөн иштер жазылат, ошондуктан эч ким аларга кайтып келбейт. Соответствия выполняются на сервере и временно останавливаются - на бюджете, на провайдере, или потому, что вы закрыли закладку - и продолжаются точно оттуда, где остановились.
Бул эмне үчүн эмес
Теорема - бул дедукциялык сөз. Бул сайт математика, логика, теоретик информатика, теоретик физика жана экономика теориясы үчүн түзүлгөн - бул тармактардагы талап далилдөө менен чечилген. Биология, медицина, химия же социалдык илимдердин эмпирикалык суроолору теоремаларды жаратпайт, алар табылгаларды жаратат, жана эч кандай формализация аларды чече албайт. Биздин referee.chat аттуу өнөктөш сайтыбыз ошол эле панелдик-референттик процессти Lean кадамынсыз, дал ушул суроолор үчүн жүргүзөт.