Розробник опублікував Lean-доказ гіпотези Конвея, отриманий за допомогою ШІ Claude
I vibed a proof of Conway's conjecture
Блогер-розробник за місяць роботи з мовною моделлю Claude отримав формальний доказ у системі Lean гіпотези Конвея про «уточнення» (refinement) омніфічних чисел — задачі, яку математик Джон Конвей сформулював 50 років тому в теорії сюрреальних чисел. За словами автора, доказ пройшов автоматичні перевірки в реєстрі Palomar, а кілька фахівців з Lean підтвердили коректність формулювання, хоча незалежної математичної верифікації ще не було. Автор визнає, що результат потребує подальшої перевірки, і запрошує математиків спростувати або підтвердити доказ.
Мовою оригіналу · EN
A blogger spent a month and a large amount of tokens getting the AI model Claude to help produce a Lean proof of Conway's 1976 refinement conjecture about omnific integers in surreal number theory…
Читати оригінал на Hacker News (100+ балів) →
Чому в стрічці: Демонструє здатність ШІ Claude розв'язувати нетривіальні наукові задачі — цікаво з погляду AI-можливостей.