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

Хтось планує брати участь? Це буде дуже весело!

Одна з причин, чому я дуже чекаю нових архітектур, полягає в тому, що проблеми в алгебраїчній топології фундаментально вимагають інтуїцій, які виходять далеко за межі простих символічних маніпуляцій. Часто набагато легше представити візуальний ескіз аргументу, заснованого на ізотопії/гомотопії, ніж розробити точні формули і зробити його повністю формальним. Я сподіваюся, що поєднання світових моделей, символічної маніпуляції та репрезентацій динаміки об'єктів стане шляхом до абсолютно нових архітектур. Вони нам потрібні, якщо ми хочемо розв'язувати складні математичні задачі, які виходять за межі простого тексту. На зображенні (на основі arXiv: 2107.01664) видно, наскільки легко інтуїтивно визначити парадокс наручників, але наскільки складно написати його формально за допомогою формул.