The Omega Project — математические выводы и проверка в Lean 4
The Omega Project — компилятор теорий, который выводит, верифицирует, визуализирует и публикует математические утверждения на основе одного уравнения. Проект предназначен для исследователей и математиков, стремящихся к строгому, машиночитаемому и проверяемому построению математических теорий с минимальным набором аксиом.
Возможности и состав проекта
Проект воспроизводит теоретические работы, используя Lean 4 для машинной верификации каждой теоремы и отслеживания цепочки вывода. Он исследует математические структуры, возникающие из динамических систем, наблюдаемых через конечное бинарное окно, и демонстрирует, как эти структуры приводят к появлению арифметики, спектральной теории и других математических концепций.
Начало работы и требования
README предлагает сборку через Lean-инструмент Lake; Mathlib загружается при подготовке зависимостей. Для знакомства полезнее начать с конкретного формального утверждения и его файла, затем проверить, какие определения и предпосылки используются в доказательстве.
Ограничения и выбор сценария
Общее описание теоретического компилятора принадлежит авторам. Проверка в Lean подтверждает конкретную формализацию при её предпосылках, а не любые философские выводы проекта. В README есть открытые и условные результаты; наличие ежедневного CI само по себе не доказывает завершённость теории.
Лицензия и условия использования
GitHub не определяет однозначную стандартную лицензию этого репозитория. Условия использования нужно проверить в README, LICENSE и документации авторов; доступность файлов на GitHub сама по себе не разрешает любое распространение или коммерческое использование.
