Новый журнал потребует доказательств исключительно в Lean

17 октября 2026 года на блоге Теренса Тао Шаомин Го и коллеги предложили запустить математический журнал с жёстким правилом: статья принимается только если доказательства формально проверены в Lean (интерактивный помощник доказательств, где компьютер сам подтверждает каждый шаг).

Это ответ на поток работ с участием LLM (больших языковых моделей). Авторы опасаются незаметных ошибок. Второй принцип журнала — ценность понимания результата важнее приоритета первооткрывателя. Издание будет открытым.

Пока это идея для обсуждения сообщества. Она показывает, куда движется математика: ИИ ускоряет открытия, а машинная проверка становится стандартом надёжности...

Источники:
https://terrytao.wordpress.com/2026/10/17/starting-a-new-journal/

#AI #Mathematics #Lean #LLM #FormalVerification #MathResearch