About Theorem.chat
Theorem.chat принимает математическое требование и пытается его урегулировать. Вы заявляете о претензии и стандарте, который она должна удовлетворять. Коллекция моделей АИ — сколько вам угодно, от каких бы поставщиков вы ни хотели — атакует ее, и еще один судья. Затем аргумент официально оформлен в Lean 4 против Mathlib, и ядро Лиана решает, доказано ли это. Последний шаг - продукт.
Почему ядро, а не другая модель
Задай модель трудный вопрос и получай от себя свободно ответ, правильно ли это. Спроси несколько и они часто согласны, что кажется подтверждением и не является: модели делятся данными об обучении и делятся слепыми точками. Вторая модель, проверяющая первое, все равно является тем же самым суждением, и это можно разговаривать. Ядро Лина не может. Оно либо получает заявление от аксиом и Mathlib, либо нет, и уверенность не влияет на результат.
The usual ways to fake a formal proof are checked for and refused. A proof that leaves a hole with sorry, one that appeals to native_decide to make the kernel take a computation on trust, or one that quietly introduces a new axiom, is detected and rejected rather than counted as a success.
Что может сделать панель
Споры — это дешевая часть. Коллегия работает с литературой — arXiv, OpenAlex, Crossref — так что известный результат цитируется, а не переиздается плохо. В ней SageMath и PARI/GP для вычислений, Z3 и CVC5 для поиска SMT, OEIS поиска для определения последовательности, которую она создала, и песчаная среда Python без доступа к сети. Предположение может быть опробовано на 10 000 случаев, прежде чем кто-либо потратит раунд, пытаясь доказать это, и контрпример немедленно прекращает обсуждение.
Доказательства, а не красноречие
Спичка не оценивается в качестве аргумента. Претензия декомбинируется в критерии принятия, и критерий урегулируется только тогда, когда что-то, стоящее за ней, может быть перепроверено третьей стороной: источник с соответствующим цитируемым отрывком или код, который был фактически исполнен с его реальным результатом. Судья проверяет саму доказательства до вынесения решения, и он не может объявить матч завершенным, пока критерий еще не закрыт.
Ты поставил бар
Стандарт - ваш выбор, и судья его поддерживает буквально. Спросите, что бы принял осторожный эксперт, и вы получите это. Попросите полный дедуктивный аргумент с каждым заявленным предположением, и вы будете судить против этого. Спросите в баре, с чем будет встречен презентационный документ, и честный результат обычно является точным отчетом о том, где группа была бы не в состоянии, что стоит больше, чем уверенное утверждение, что вам придется проверить себя в любом случае.
Чтобы быть предельно ясным: это не машина, которая решает открытые проблемы. Это машина, которая отказывается позволить спору пройти как урегулированный, когда это не так, и которая точно говорит вам, какой шаг не удалось.
Неудачная формализация - полезный результат
Когда Лиан не закроет доказательства, вы получите ту цель, которая остается. На практике это почти всегда место, где неформальный аргумент был ручным, — шаг, который все читающие прозвище, кивнули бы в прошлом. Затем эта цель передается тому, какое место лучше всего находится для нападения, вместе с тем, что уже было испытано, и ничего больше. Модели болтаются, когда они застряли, переставая за полную цену; вместо этого, как правило, отпирают один конкретный вопрос для части символов.
Долгая работа выживает
Каждая лемма, которую устанавливает эта панель, заносится в общую бухгалтерскую книгу с доказательствами, поэтому результаты записываются один раз и никогда не переиздаются, и записываются тупиковые точки, чтобы никто не возвращался в них. Совпадает с сервером и останавливается на чистоте — по бюджету, по отключке поставщика, или потому, что вы закрыли счет — и возвращаетесь точно туда, где они остановились.
Что это не для
Теорема — это дедуктивное слово. Этот сайт построен для математики, логики, теоретической компьютерной науки, теоретической физики и экономической теории — областей, в которых претензии урегулируются с помощью доказательств. Эмпирические вопросы в биологии, медицине, химии или социальных науках не производят теоремы, они создают выводы, и никакая формализация не будет их решать. Наш сайт referee.chat работает в том же режиме без шага Лиана, точно по этим вопросам.