Аналитическая теория чисел, как и многие другие области современного анализа, часто использует удобные асимптотические обозначения для выражения своих результатов. Обычно применяются обозначения вроде $O$ или $o$, например, для указания границы вида $O(f(n))$ для некоторой неопределённой константы $c$. Такие подразумеваемые константы варьируются от строки к строке, и в большинстве работ их не вычисляют явно. Это упрощает как написание, так и чтение статей (например, можно использовать асимптотические обозначения, чтобы скрыть большое количество членов более низкого порядка), а также означает, что незначительные числовые ошибки (например, забытый множитель два в неравенстве) обычно не влияют на конечные результаты. Однако за это приходится платить: многие результаты в аналитической теории чисел верны только в асимптотическом смысле. Типичный пример — теорема Виноградова, утверждающая, что каждое достаточно большое нечётное целое число можно выразить как сумму трёх простых чисел. В первых доказательствах этой теоремы порог «достаточно большого» не был указан явно.
Явные оценки в аналитической теории чисел
Существуют явные оценки в аналитической теории чисел, в которых все константы вычисляются полностью (и сохраняется множество членов более низкого порядка). Например, в то время как теорема о распределении простых чисел утверждает, что функция подсчёта простых чисел $\pi(x)$ асимптотически равна интегралу $\text{li}(x)$, в недавней работе Фьори, Кадири и Свидинского получена явная оценка.
Такие явные результаты следуют в целом похожим стратегиям доказательства, что и их неявные аналоги, но требуют значительного количества тщательных расчётов и численной оптимизации. Любая данная статья по явной аналитической теории чисел, вероятно, будет опираться на численные результаты, полученные в предыдущих статьях по явной аналитической теории чисел. Хотя авторы прилагают все усилия, чтобы избежать ошибок и внести некоторую избыточность в свою работу, к сожалению, были случаи, когда явный результат, заявленный в опубликованной литературе, содержал численные ошибки, которые ставили под сомнение численные константы в нескольких последующих применениях этих статей.
Проект «Интегрированная явная сеть аналитической теории чисел»
Проект «Интегрированная явная сеть аналитической теории чисел» частично размещён в рамках существующего проекта формализации «Теорема о распределении простых чисел и другие результаты» (PNT+). Этот проект будет состоять из двух компонентов.
1. Краудсорсинговый проект формализации для формализации ряда взаимосвязанных результатов явной аналитической теории чисел в Lean, таких как явная теорема о распределении простых чисел Фьори, Кадири и Свидинского. Уже некоторые более мелкие результаты были в значительной степени формализованы, и мы добиваемся значительного прогресса (особенно с помощью современных инструментов автоформализации на базе ИИ) по нескольким более крупным статьям.
2. Второй компонент, который будет реализован в IPAM при финансовой и технической поддержке Math Inc., будет заключаться в извлечении из этой сети формализованных результатов интерактивной «таблицы» большого количества типов таких оценок, с возможностью добавления или удаления оценок из сети и автоматическим распространением числового влияния этих изменений на другие оценки в сети, подобно тому, как изменение одной ячейки в таблице автоматически обновляет другие ячейки, которые от неё зависят.
Например, можно увеличить или уменьшить числовой порог, до которого проверяется гипотеза Римана, и увидеть влияние этого изменения на явные члены ошибки в теореме о распределении простых чисел; или можно «откатить» всю литературу до определённой даты и увидеть, какие наилучшие оценки различных выражений аналитической теории чисел всё ещё можно получить из литературы, доступной на ту дату.
Изначально эта таблица будет составлена на основе прямых адаптаций различных аргументов из статей, формализованных в сети, но на более амбициозном втором этапе проекта мы планируем использовать инструменты ИИ для модификации этих аргументов, чтобы найти более эффективные соотношения между различными числовыми параметрами, чем те, которые были представлены в исходной литературе.
Проект координируется с помощью системы на основе проблем на GitHub, аналогично тому, как это было сделано для проекта «Теории уравнений». Любой доброволец может выбрать одну из невыполненных задач формализации на странице проблем GitHub и «заявить» её как задачу для работы, в конечном итоге отправив запрос на включение (PR) в репозиторий, предлагая решение (или «отказаться» от задачи, если по какой-либо причине вы не сможете её выполнить).
Как и в других крупных проектах по формализации, в настоящее время разрабатывается неформальный «чертёж», который разбивает доказательства основных результатов нескольких статей по явной аналитической теории чисел на небольшие леммы и подлеммы, большинство из которых можно формализовать независимо, не требуя более широких знаний аргументов из статьи, из которой была взята лемма.
Мы разрешаем использовать ИИ для выполнения задач по формализации доказательств, хотя мы требуем, чтобы использование ИИ было раскрыто, и чтобы код редактировался людьми для удаления избыточности. (Мы ожидаем, что часть сгенерированного ИИ кода будет довольно неэлегантной; но ни одно доказательство этих явных оценок аналитической теории чисел, независимо от того, создано ли оно человеком или ИИ, вряд ли будет настолько красивым или достойным того, чтобы его читать ради него самого, поэтому недостатки использования сгенерированных ИИ доказательств здесь ниже, чем в других случаях использования.)
Мы, конечно, требуем, чтобы все представления соответствовали Lean через систему непрерывной интеграции (CI) GitHub, чтобы любой неправильно сгенерированный ИИ код был отклонён. Мы также осторожно экспериментируем со способами, с помощью которых ИИ может автоматически или полуавтоматически генерировать формализованные утверждения лемм и теорем, хотя здесь нужно быть значительно более внимательным к опасности неформальной формулировки неформально сформулированного результата, поскольку этот тип ошибки не может быть автоматически обнаружен помощником по доказательству.