ИИтог

TheoremDB запустился: открытая база математических задач с проверкой в Lean

инструментыРедакция ИИтогHacker News🔥46Рейтинг ИИтог46Влияние42Новизна55Релевантность62Неожиданность18Участники15Достоверность75

TheoremDB, публичный веб-сервис («workspace»), который собирает математические задачи вместе с историей их решения: что уже доказано, какие подходы провалились и какой код стоит за каждым вычислением. Идея, по словам создателей сайта, в том, что исследовательские агенты (программы, автоматически решающие или проверяющие математические утверждения) часто дублируют работу, потому что прежние попытки и неудачные подходы негде искать. TheoremDB даёт им общий журнал, который можно и искать, и дополнять; авторы сайта сравнивают амбицию проекта с OEIS, известной базой целочисленных последовательностей, только применительно не к последовательностям, а к задачам, подходам, свидетельствам и результатам.

Каждая задача на сайте, это «карточка» с чётко сформулированной целью: например, среди открытых задач числится классический вопрос о сумме трёх кубов, существуют ли целые x, y, z с |x|,|y|,|z| ≤ 10^20, такие что x³+y³+z³=114. Решения к задачам можно присылать с разной степенью доказательности; доказательство, формально проверенное в системе Lean (инструмент для машинной проверки математических доказательств), получает наивысшую степень.

Сайт сейчас в статусе альфа-версии. Публичная запись уже открыта, включая отправку Lean-доказательств через встроенный инструмент TheoremDB Researcher, а вот «семантическое расширение» (semantic expansion), судя по всему, более умный поиск по смыслу задач, пока отключено. Источник не называет ни дату запуска, ни людей или организацию, стоящих за проектом, ни число решённых или открытых задач, ни объём уже поступивших доказательств, ни то, что именно должно измениться после включения семантического расширения.

Ключевые факты

  • TheoremDB, публичная платформа-«workspace» для машинной математики: общий банк задач с историей попыток их решения.
  • Сайт в альфе; публичная запись уже работает, включая отправку доказательств в Lean через инструмент TheoremDB Researcher.
  • Решения ранжируются по степеням доказательности; Lean-проверенное доказательство, высшая степень.
  • Карточка задачи показывает весь путь: что доказано, какие подходы провалились и какой код стоит за вычислениями.
  • Авторы сайта сравнивают долгосрочную амбицию проекта с OEIS, только для задач, подходов и результатов, а не последовательностей.

Почему это важно

Автоматические исследовательские агенты, которые пробуют доказывать или проверять математические утверждения, регулярно повторяют чужую работу: прежние попытки, частичные результаты и тупиковые подходы нигде не зафиксированы централизованно. TheoremDB предлагает решение именно этой проблемы, общий, доступный для поиска журнал задач и подходов к ним, по аналогии с тем, чем OEIS стала для целочисленных последовательностей.

Кому это важно

В первую очередь, разработчикам и операторам исследовательских ИИ-агентов, которые автоматически ищут или проверяют математические доказательства: им нужен общий реестр, чтобы не решать одну и ту же задачу параллельно и не терять неудачные попытки. Также инструмент полезен математикам и командам, которые работают с формальной верификацией доказательств в Lean.

Как это применить

Сайт открыт для публичной записи уже сейчас: доказательство можно отправить через встроенный инструмент TheoremDB Researcher, в том числе формально проверенное в Lean, такие решения получают наивысшую степень доказательности среди возможных градаций. Каждая карточка задачи открывает полный «пакет»: что уже доказано, какие подходы не сработали и какой код стоит за вычислениями. Функция «семантического расширения», по всей видимости, более умный поиск по смыслу задач, в текущей альфе ещё отключена.

Можно ли доверять

Источник, сам сайт TheoremDB, то есть его собственное описание своих функций, а не независимый обзор. Заявленные механики (публичная запись, градации доказательности, отдельный инструмент для Lean-доказательств) описаны конкретно и проверяемо, их видно на самом сайте. Но кто стоит за проектом, кто его финансирует, сколько задач и доказательств уже накопилось, источник не сообщает, и на слово тут верить не приходится: это данные, которые ещё предстоит проверить или дождаться от самих создателей.

Риски и подводные камни

Проект в альфе, функциональность (в частности, семантический поиск) заведомо неполная, а публичная запись без раскрытия того, кто модерирует контент, оставляет открытым вопрос о качестве и защите от мусорных или недобросовестных вкладов. Отсутствие данных о создателях, финансировании и масштабе базы не позволяет оценить, насколько устойчив и жизнеспособен проект за пределами демонстрационного этапа.

«Исследовательские агенты часто дублируют работу, потому что прежние попытки, промежуточные результаты и неудачные подходы негде найти. TheoremDB даёт им общий журнал, который можно искать и дополнять.»

— TheoremDB, текст сайта