Новый журнал потребует доказательств исключительно в Lean
Новый журнал потребует доказательств исключительно в Lean 17 октября 2026 года на блоге Теренса Тао Шаомин Го и коллеги предложили запустить математический журнал с жёстким правилом: статья принимается только если доказательства формально проверены в Lean (интерактивный помощник доказательств, где компьютер сам подтверждает каждый шаг). Это ответ на поток работ с участием LLM (больших языковых моделей). Авторы опасаются незаметных ошибок. Второй принцип журнала — ценность понимания результата важнее приоритета первооткрывателя. Издание будет открытым. Пока это идея для обсуждения сообщества. Она показывает, куда движется математика: ИИ ускоряет открытия, а машинная проверка становится стандартом надёжности... Источники: https://terrytao.wordpress.com/2026/10/17/starting-a-new-journal/ #AI #Mathematics #Lean #LLM #FormalVerification #MathResearch