На 4 септември Anthropic публикува доказателство на Голямата теорема на Ферма, проверено докрай в Lean. Claude е работил основно сам 11 дни, написал е 13 милиона реда и е доказал 29 500 междинни теореми, използвани в крайния резултат. Общността очакваше формализирането да отнеме години.
- Доказателството следва опростен вариант на пътя на Уайлс; математическата намеса на хората се свежда до редки общи указания от изследователя Tianyi Peng.
- Проверено е от Lean само с трите му стандартни аксиоми; Кевин Бъзард, който води общностния проект от 2024 г., го е прегледал.
- Около шест милиарда изходни токена от вътрешен модел, сравним с Claude Fable 5.1.
Сто двайсет и девет страници. Толкова е първото доказателство на Уайлс от 1995 г., а проверката му отнема месеци на няколко математици.
Новото доказателство е 13 милиона реда код и го проверява машина, стъпка по стъпка, без да прескача очевидното.
Важно е какво точно е новото. Claude не е открил ново доказателство - теоремата е доказана преди повече от трийсет години. Новото е проверката: превръщането на човешкото доказателство във вериги, които машина минава от начало до край.
И една подробност, която ме спечели повече от числата. Anthropic сама пише, че доказателството вероятно е много по-дълго, отколкото трябва. Mathlib е стегната и прегледана, а това е тромаво, но вярно. Като първа версия на нещо, за което хората очакваха години, тромаво и вярно стига.
За който преподава или пише математика, най-показателен е последният им пример: формализиране на теоремата на Виноградов за три прости числа за три дни, с три лични абонамента Claude Max. Това вече не е проект само за лаборатория с бюджет.