dxdt.blog: занимательный интернет-журнал

Anthropic (это Claude) на днях опубликовали, как заявляется, полную “формализацию” для Великой теоремы Ферма. Под “формализацией” тут надо понимать машинное описание всего набора необходимых теорем, за исключением нескольких базовых. С точки зрения алгоритмов, речь там про Lean-код, который подтверждает верность выводов – там заявлено 29511 сопутствующих теорем (это в терминах Lean, но, вообще, тут не так важно), то есть, заведомо необозримый кусок текста, и даже для машинной проверки – требуются сотни гигабайтов памяти (ОЗУ) и многие часы работы компьютера.

Но тут особенно интересен сопутствующий аспект: а именно, то, как новость подаётся. В тексте официальной новости несколько раз упоминаются другие, “человеческие” начинания на пути этой же “формализации”, но эти начинания, пока что, успеха не достигли, что тщательно подчёркивает текст новости. И это так, тут не поспорить. Достигла ли успеха машинная программа с миллионами строк и десятками тысяч “машинных теорем”? Тоже непонятно. Собственно, тут-то и кроется действующий конфликт: с завершающими заявлениями по долгоиграющим популярным темам вокруг теоретической математики начали выступать не университеты какие-нибудь, а коммерческие корпорации, поставляющие мощнейший вычислительный сервис, который принято называть LLM/AI. И выступают эти корпорации тут нынче регулярно: следом за “Ферма-формализацией” – свежее заявление по уравнениям Навье-Стокса от OpenAI (это проблема из раскрученного списка “Задачи тысячелетия”).

Адрес записки: https://dxdt.blog/2026/09/09/19159/