Я лично перешел черту, и я немного в восторге. Это моя первая полностью автоматизированная, сгенерированная LLM и автоформализованная доказательство новой математической теоремы. Позвольте мне сформулировать задачу: у нас есть три вращающихся круга с шестью позициями каждый, все три пересекаются в общей сложности в шести точках. Докажите, что группа движений, которую они генерируют, является полной симметрической группой S_{12}. Эту задачу я изначально заметил в прекрасной головоломке в игре Machinarium от Amanita Design. Задача не очень сложная, но, по-видимому, имеет два доказательства: 1. Грубая сила поиска по классам сопряженности для представления всех транспозиций (я делал это много лет назад, но никогда не публиковал). 2. Доказательство, сгенерированное LLM (в данном случае произведенное около трех месяцев назад GPT-5-Pro), или, на самом деле, два доказательства, оба блестяще использующие теорему Жордана о примитивных группах (или близкий вариант, который еще более прямой). ( Что мне не хватало до сегодняшнего вечера, так это инструмента для автоформализации этого доказательства. Благодаря @HarmonicMath я получил доступ к их замечательному программному обеспечению, Аристотель. Вкратце, вот что я сделал: A. Автоматически сгенерировал доказательство с помощью LLM (и запустил его несколько раз, чтобы получить значительно улучшенную версию). B. Убрал доказательство до голого математического текста — определений, предложений, лемм, теорем — с доказательствами, предоставленными LLM. C. Запустил систему Аристотель на ночь (через API). Сегодня утром я получил полностью формализованную версию на Lean (около 700 строк кода). Код компилируется, так что теперь у меня есть сертификат, подтверждающий, что сгенерированное LLM доказательство действительно привело к правильному решению. Более того, я получил концептуальное доказательство, лучшее, чем моя собственная грубая сила. Я планирую продвинуть это дальше к более широкому классу таких алгебраических задач. Это небольшой проект, но для меня лично он отмечает веху. Теперь у меня есть инструменты, которые, с моей оркестрацией, могут действительно помочь мне открывать, формализовать и изучать доказательства математических теорем. Это не тривиально. Вопросы: 1. Как это будет масштабироваться в будущем? 2. Сколько обучения будет необходимо для успешного выполнения таких задач? 3. Как мы должны относиться к авторству таких доказательств? 4. Какова более глубокая роль математиков?