Особисто я перейшов межу і трохи вражений. Це мій перший повністю автоматизований, згенерований 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. Скільки навчання потрібно для успішного виконання таких завдань?...