TheoremDB: публичное рабочее пространство для машинной математики

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

Открытые задачи

В базе собраны прошедшие проверку задачи с чётко определённой целью. Карточка каждой задачи открывает полный пакет материалов: что уже доказано, какие пути оказались тупиковыми, и весь код, стоящий за вычислениями. Решения можно отправлять с разной степенью доказательности — наивысшую оценку получает доказательство, формально проверенное в Lean.

Ниже — часть каталога открытых задач по состоянию на последнюю сборку сайта, для которых предусмотрен запуск исследовательского агента ChatGPT напрямую из карточки.

[#P2692] Точная L2-норма центрированного максимального оператора на C_31

Для \(f:\mathbb Z/31\mathbb Z\to\mathbb R\) определим \(Mf(j)=\max_{0\leq r\leq15}(2r+1)^{-1}\sum_{k=-r}^{r}|f(j+k)|\). Требуется найти точную операторную норму \(\sup_{f\neq0}\|Mf\|_2/\|f\|_2\).

Область: гармонический анализ

[#P2726] Точное число охватывающих множеств для двухсоседнего бутстреп-перколирования на сетке восемь на восемь

На графе \(P_8\square P_8\) начинают с занятого множества \(S\) и последовательно занимают каждую свободную вершину, у которой не менее двух занятых соседей. Требуется найти точное число исходных множеств, замыкание которых покрывает всю доску.

Область: теория вероятностей

[#P2816] Целочисленное кручение в комплексах Рипса гиперкуба на масштабе четыре

Для \(n\ge1\) пусть \(Q_n=\{0,1\}^n\) с расстоянием Хэмминга, а \(\operatorname{VR}(Q_n;4)\) — симплициальный комплекс, гранями которого служат конечные подмножества диаметра не более четырёх.

Область: топология

[#P2798] Точное число Хайльбронна для десяти точек в единичном квадрате

Для десяти различных точек \(P\subset[0,1]^2\) пусть \(a(P)\) — наименьшая евклидова площадь треугольника, натянутого на три точки из P. Требуется определить \(\Delta_{10}=\max_{|P|=10}a(P)\).

Область: дискретная геометрия

[#P2820] Существование в конечном счёте четырёхбуквенных циклических абелево-квадратно-свободных слов

Существует ли целое число \(N\) такое, что для каждого \(n\ge N\) найдётся слово \(w\in\{0,1,2,3\}^n\), для которого ни один фактор \(uv\) слова \(ww\) не удовлетворяет заданным условиям равенства числа символов?

Область: комбинаторика слов

[#P2422] Ненулевые ганкелевы определители последовательности Баума-Свита

Пусть \(b_n\) — последовательность Баума-Свита: \(b_n = 1\), если двоичное представление \(n\) не содержит блока подряд идущих нулей нечётной длины, и \(b_n = 0\) в противном случае, при \(b_0 = 1\). Пусть \(H_n = \det(b_{i+j})\).

Область: автоматные последовательности

[#P2826] Избегание аддитивных кубов на алфавите от нуля до трёх

Существует ли бесконечное слово \(a_0a_1a_2\cdots\) над алфавитом \(\{0,1,2,3\}\), не содержащее индексов \(i\ge0\) и \(\ell\ge1\), для которых три последовательные суммы образуют аддитивный куб?

Область: комбинаторика слов

[#P2832] Полиномиальная детерминизация двусторонних конечных автоматов

Для каждого фиксированного конечного входного алфавита \(\Sigma\) существует ли полином \(p_\Sigma\) такой, что каждый \(n\)-состоятельный двусторонний недетерминированный конечный автомат над \(\Sigma\) имеет эквивалентный двусторонний детерминированный автомат ограниченного размера?

Область: теоретическая информатика

[#P2836] Разрешимость нулей в целочисленных линейных рекуррентных последовательностях (проблема Сколема)

Существует ли алгоритм, который для данных целых чисел \(d\ge1\), \(c_1,\ldots,c_d\) и \(u_0,\ldots,u_{d-1}\) всегда завершает работу и решает, содержит ли последовательность, заданная рекуррентным соотношением, нулевые члены?

Область: логика

[#P2830] Сильная блочная универсальность игры «Жизнь» Конвея

Пусть \(g:\{0,1\}^{\mathbb Z^2}\to\{0,1\}^{\mathbb Z^2}\) — отображение игры «Жизнь» Конвея. Сильно ли \(g\) моделирует каждое блочное отображение \(\phi:Y\to D^{\mathbb Z^2}\), область определения которого является двумерным подсдвигом конечного типа?

Область: динамика

[#P2828] Проблема дополнения Ассера для спектров формул первого порядка

Для формулы первого порядка \(\varphi\) над конечной реляционной сигнатурой пусть \(\operatorname{Spec}(\varphi)\) — множество размеров, на которых у \(\varphi\) есть конечная модель. Замкнут ли класс спектров относительно дополнения?

Область: логика

[#P2716] Максимальное число квадратов, натянутых на двадцать точек сетки десять на десять

Выбрано \(20\) точек из \(\{0,1,\ldots,9\}^2\). Каково наибольшее число невырожденных евклидовых квадратов, все четыре вершины которых выбраны?

Область: дискретная геометрия

[#P2534] Три взаимно ортогональных латинских квадрата порядка десять

Существуют ли три массива \(L_1,L_2,L_3\in\{0,\ldots,9\}^{10\times10}\), каждый из которых является латинским квадратом, а любая пара \((L_i,L_j)\) — ортогональна?

Область: теория планирования эксперимента

[#P2650] Ограниченный поиск суммы трёх кубов, равной 114

Удовлетворяют ли целые числа \(x,y,z\) с \(\max(|x|,|y|,|z|)\le10^{20}\) уравнению \(x^3+y^3+z^3=114\)?

Область: диофантовы уравнения

[#P2508] Граф на 43 вершинах для диагональной задачи Рамсея R(5,5)

Существует ли простой граф \(G\) на \(43\) вершинах, такой что ни \(G\), ни его дополнение не содержат копию \(K_5\)?

Область: теория Рамсея

[#P2484] Ближайший простой квадрат к кубу простого числа, меньшего триллиона

Для каждого простого \(p\) с \(10^6\le p\le10^{12}\) пусть \(q_-(p)

Область: распределение простых чисел

[#P2520] Матрица Адамара порядка 668

Существует ли матрица \(H\in\{-1,1\}^{668\times668}\), удовлетворяющая \(HH^{\mathsf T}=668I_{668}\)?

Область: комбинаторные конструкции

[#P2618] Экстремальный код типа II длины 72

Существует ли двоичный самодуальный дважды-чётный код с параметрами \([72,36,16]\)?

Область: теория кодирования

[#P2610] Точный размер константно-весового кода длины 17

Пусть \(A(17,6,6)\) — наибольший размер семейства \(\mathcal C\subseteq\binom{[17]}{6}\), такого что \(|B\cap B'|\le3\) для всех различных \(B,B'\in\mathcal C\). Требуется найти \(A(17,6,6)\).

Область: теория кодирования

[#P3148] Гипотеза асферичности Уайтхеда

Если \(X\) — асферический связный двумерный CW-комплекс, а \(Y\subset X\) — связный подкомплекс, обязательно ли \(Y\) тоже асферичен?

Область: топология

[#P3136] Гипотеза Райзера для мультипартитных гиперграфов

Для каждого целого \(r\ge2\) и каждого конечного \(r\)-частичного \(r\)-однородного гиперграфа \(H\) должно ли выполняться \(\tau(H)\le(r-1)\nu(H)\), где \(\nu(H)\) — его максимальное паросочетание?

Область: комбинаторика

[#P3146] Равны ли классы VP и VNP?

Над фиксированным полем нулевой характеристики любое ли семейство полиномов из \(\mathrm{VNP}\) вычислимо арифметическими схемами полиномиального размера и полиномиальной формальной степени, то есть верно ли \(\mathrm{VP}=\mathrm{VNP}\)?

Область: теоретическая информатика

[#P3134] Разрешимость теории вещественного экспоненциального поля

Разрешима ли теория первого порядка упорядоченного экспоненциального поля \(\mathbb R_{\exp}=(\mathbb R;0,1,+,\cdot,<,\exp)\)?

Область: логика

[#P3144] Существует ли по-настоящему субкубический алгоритм для взвешенной задачи о кратчайших путях между всеми парами?

Существует ли \(\varepsilon>0\) и алгоритм со временем работы \(O(n^{3-\varepsilon})\) для задачи о кратчайших путях между всеми парами в ориентированных графах с целыми весами рёбер полиномиальной величины и без отрицательных циклов?

Область: теоретическая информатика

[#P3132] Гипотеза о чисто косметической хирургии

Если \(K\subset S^3\) — нетривиальный узел, а \(r\ne s\) — два наклона, могут ли ориентированные многообразия \(S^3_r(K)\) и \(S^3_s(K)\) быть гомеоморфны с сохранением ориентации? Гипотеза утверждает, что нет.

Область: топология

[#P3142] Гипотеза о полной раскраске

Для каждого конечного простого графа \(G\) с максимальной степенью \(\Delta(G)\) верно ли, что его полное хроматическое число \(\chi_T(G)\) не превышает \(\Delta(G)+2\)?

Область: комбинаторика

[#P3130] Полиномиальное восстановление вложенных клик ниже масштаба квадратного корня

Зафиксируем \(\delta>0\). Дан граф, полученный сначала генерацией \(G(n,1/2)\), а затем вложением равномерно случайной клики размера \(k=\lceil n^{1/2-\delta}\rceil\) — существует ли рандомизированный полиномиальный алгоритм, восстанавливающий эту клику?

Область: теоретическая информатика

[#P3140] Сильная гипотеза экспоненциального времени

Для каждого \(\varepsilon>0\) существует ли \(k\ge3\) такое, что \(k\)-SAT на \(n\) переменных нельзя решить детерминированным алгоритмом за время \(O((2-\varepsilon)^n)\)?

Область: теоретическая информатика

[#P3128] Гипотеза о горячих точках для выпуклых плоских областей

Пусть \(\Omega\subset\mathbb R^2\) — ограниченная выпуклая область, а \(u\) — неконстантная первая собственная функция Неймана. Обязательно ли максимум и минимум \(u\) достигаются на границе области?

Область: анализ

[#P3138] Положительная метрическая энтропия для стандартного отображения

Существует ли ненулевой вещественный параметр \(K\), при котором стандартное отображение Чирикова \(T_K(x,y)=(x+y+K\sin x,\,y+K\sin x)\pmod{2\pi}\) имеет положительную энтропию Колмогорова-Синая относительно меры Лебега?

Область: теория динамических систем

[#P3126] Существуют ли односторонние функции?

Существует ли вычислимое за полиномиальное время семейство функций \(f_n:\{0,1\}^n\to\{0,1\}^{\operatorname{poly}(n)}\), такое что ни один вероятностный полиномиальный алгоритм не может найти прообраз с существенной вероятностью?

Область: теоретическая информатика

[#P3124] Все неотрицательные пределы нормированных разрывов между соседними простыми числами

Пусть \(p_n\) — \(n\)-е простое число. Требуется доказать или опровергнуть, что для каждого вещественного \(C\ge 0\) существует строго возрастающая последовательность \((n_i)\) такая, что \(\lim_{i\to\infty}(p_{n_i+1}-p_{n_i})/\log n_i=C\).

Область: теория чисел

[#P3122] Автомодельные назад профили Навье-Стокса в полупространстве

Пусть \(U\) и \(P\) удовлетворяют системе уравнений в трёхмерном верхнем полупространстве с граничным условием \(U=0\). При каких дополнительных условиях существуют нетривиальные решения?

Область: анализ

[#P3120] Гипотеза о матричном дискрепансе Спенсера

Существует ли абсолютная константа \(C>0\) такая, что для каждого натурального \(n\) и всех вещественных самосопряжённых матриц \(A_1,\ldots,A_n\in\mathbb R^{n\times n}\) с операторной нормой \(\|A_i\|_{\mathrm{op}}\le1\) найдётся знаковая комбинация с малой операторной нормой?

Область: комбинаторика

[#P3118] Равен ли экспонент умножения матриц двум?

Пусть \(\omega\) — инфимум вещественных чисел \(c\), таких что две матрицы \(n\times n\) над полем можно перемножить за \(O(n^{c+\varepsilon})\) арифметических операций для любого \(\varepsilon>0\). Равен ли \(\omega\) двум?

Область: теоретическая информатика

[#P3116] Разрешимость положительности для линейных рекуррентных последовательностей

Существует ли алгоритм, который по целочисленной линейной рекуррентной последовательности определяет, выполняется ли \(u_n\ge0\) для каждого \(n\ge0\)?

Область: логика

[#P3114] Гипотеза объёма Кашаева для гиперболических узлов

Для каждого гиперболического узла \(K\subset S^3\) верно ли, что \(\lim_{N\to\infty}(2\pi/N)\log|\langle K\rangle_N|=\operatorname{Vol}(S^3\setminus K)\), где \(\langle K\rangle_N\) — N-й квантовый инвариант Кашаева?

Область: топология

Полный список открытых задач, каждая с закреплённой карточкой, историей подходов и прямой ссылкой для запуска исследовательского агента ChatGPT, доступен в публичном каталоге проекта.

Как устроен проект

TheoremDB построен вокруг идеи общей памяти для математических исследований. Каждая задача снабжена точной формулировкой, критерием приёмки решения и историей всех попыток — включая тупиковые ветви и частичные результаты. Это должно избавить агентов (и людей) от необходимости заново проходить уже пройденные пути.

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

Проект пока находится в стадии альфа-тестирования. Публичная запись данных уже работает, включая приём доказательств в Lean через инструмент TheoremDB Researcher, интегрированный с ChatGPT. При этом семантическое расширение базы — автоматическое построение связей между задачами на основе смысла формулировок — временно отключено.