LongTails: агенты ищут новые оценки сложности в оптимизации с проверкой каждой через Lean

LongTails это открытый фреймворк на Lean 4 для автоматического поиска результатов в оптимизации. Авторы Александр Тюрин, Куоквьет Фам, Валентин Хрульков и Иван Оселедец, лицензия Apache 2.0, репозиторий создан 14 октября.

Задача описывается как Setup: типы запросов и ответов оракула, допустимые параметры, допущения о выпуклости и липшицевости, критерий успеха. Результат это теорема result : Convergence spec budget с явной формулой числа вызовов оракула. Проверяет Comparator: он сверяет теорему и бюджет с Setup, поэтому лишнее допущение, недосчитанный вызов или sorry не проходят.

🔧 Пример. Для (L0, L1)-гладкости известны две оценки: у Тюрина O‌(√(L0R²/ε) + L1R) по градиентам, у Ванкова и соавторов O‌((1+ν)[√(L0R²/ε) + (L1R)^(2/3)]) с ценой точного одномерного поиска ν. Новая оценка обходится только градиентами: O‌(√(L0R²/ε) + (L1R)^(2/3)). Член L1R улучшен до степени 2/3, множитель (1+ν) убран.

Агент, Codex или Claude Code, формализует Setup, сверяет допущения с задачей, затем ищет метод и доказательство. Результаты приходят ветками agent/*, к 30 октября закрыто 84 пул-реквеста. Сборка одной теоремы занимает 2–3 минуты после кэша Mathlib, аудит запускает python3 run_comparator.py.

📊 На 30 октября на сайте 132 setup'а с доказанными оценками, в репозитории 145 разборов новизны. Разбор это таблица прежних работ со ссылками на arXiv, датой поиска, вердиктом и уверенностью; звёзды вклада выставляют Codex и Claude Code.

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

📎 Сайт: https://k3nfalt.github.io/longtails/
GitHub: https://github.com/k3nfalt/longtails/


#Lean #Математика #AI
———
@tsingular