ChatGPT опроверг гипотезу Эрдёша о единичном расстоянии 20 мая 2026 года. Математики, получившие ранний доступ к доказательству, подтвердили: глубокая теорема теории чисел Голода и Шафаревича из 1960-х позволяет построить контрпример. Естественно, Кевин Баззард сразу спросил, формализован ли контрпример в Lean. Нет.
26 мая пришло письмо от филдсовского медалиста Майка Фридмана, который работает Chief Science Officer в Logical Intelligence — компании, сооснованной Яном ЛеКуном. Их система автоформализовала всю статью ChatGPT в Lean. Баззард и его постдок Томас Браунинг проверили: формализовано именно то, что теорема Голода-Шафаревича влечёт контрпример Эрдёша. Но сама теорема занимает больше ста страниц и требует глобальной теории полей классов — формализация глобального случая тогда ещё была открыта.
26 июня 2026 года всё изменилось. Борис Алексеев из OpenAI сообщил в Lean Zulip, что новая модель Sol полностью формализовала контрпример Эрдёша, не опираясь ни на что, кроме аксиом математики. Sol сгенерировала 1,2 миллиона строк Lean-кода за три недели. Для сравнения: библиотека mathlib, которую писали девять лет, содержит лишь 2,3 миллиона строк. Код Sol доказывал нетривиальные теоремы о когомологиях числовых полей. Баззард запустил его в песочнице — зловредный Lean-код может выполнять произвольные команды.
В начале июля на воркшопе Formalizing Fermat участникам дали доступ к Claude Fable и ChatGPT Sol. Баззард загрузил классические статьи по теории конечных плоских групповых схем, чтобы AI написал изложение. Logos Research, чей инструмент тоже автоформализует математику, заявили: одно из утверждений в pdf ложно, и нашли контрпример. Ошибка действительно была — LLM просто неверно описал стандартную конструкцию. AI не сказал «я не понимаю», а сказал «вот доказательство, что аргумент неверен».
11 июля Akhil Mathew из UChicago прислал сообщение: Sol нашёл контрпример к старому вопросу Гротендика — конечная свободная групповая схема порядка 4 не убивается числом 4. Четыре часа спустя Fable автоформализовала всё в 1076 строках Lean. Баззард скомпилировал код за пять минут — да, это контрпример. Akhil сделал PR в mathlib. Коллега из Imperial сказал, что раз контрпример так легко найти, то 60-летняя проблема Гротендика неинтересна. Баззард вспомнил, что сам когда-то потратил на неё неделю.
Студент Andrew Yang с помощью Sol и Fable написал 250 тысяч строк Lean, полностью завершив формализацию модулярной теоремы подъёма, критичной для доказательства Великой теоремы Ферма. Баззард ответил профессору, считавшему безумцами студентов, платящих 200 долларов за доступ к моделям: «Безумны те, кто не платит».
12 часов назад Levent Alpöge опубликовал в X: Fable нашёл контрпример к гипотезе Якобиана — открытому 100 лет вопросу алгебраической геометрии. Paul Lezeau уже формализовал его вручную и сделал PR в репозиторий Formal Conjectures от DeepMind. Готово.