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