На Hacker News появился ProofForge — открытый проект для ИИ-агентов, которые должны выдавать формальные доказательства, проходящие проверку Lean. Важен не шум вокруг агентов, а проверяемый результат.
OpenAI опубликовала решение одной из задач тысячелетия о существовании и гладкости решений уравнений Навье — Стокса, утверждая, что доказательство получено внутренней системой ИИ и формализовано в Lean. Теперь ключевой вопрос — выдержит ли работа проверку математического сообщества.
Новый выпуск AI Science: три свежие работы о том, как ИИ помогает формализовать сложную математику, проектировать кристаллические структуры и строить приватные медицинские модели прямо на смартфонах.
В научной подборке сегодня один, но очень сильный результат: авторы arXiv-работы утверждают, что система Aristotle впервые полностью автономно решила открытую задачу из списка Эрдёша, а затем оформила доказательство в Lean. Если вывод выдержит проверку, это будет важный шаг от олимпиадных и тестовых задач к настоящему математическому исследованию с машинной верификацией.
