24-Rabi-al-Awwal-1448

Claude за 11 дней формализовал теорему Ферма. 13 миллионов строк кода на Lean, 29 500 промежуточных теорем, около 6 миллиардов выходных токенов, работа почти без человека. Anthropic разобрали это у себя, дальше разошлось по новостям.

Теорему не доказали заново, её доказал Уайлс ещё в девяностых. Сделали другое: перевели доказательство на язык, на котором его может проверить машина. Раньше на такую работу закладывали годы труда живых математиков.

И тут интересно не «ИИ умный», а совсем другое.

Lean это компилятор для доказательств. Он либо принимает шаг, либо не принимает. С ним нельзя договориться, ему нельзя понравиться, его нельзя убедить красивой формулировкой. Он не смотрит на репутацию автора и на то, сколько до этого было правильных шагов.

Именно поэтому модель можно было отпустить на 11 дней почти автономно. Не потому что она перестала ошибаться, а потому что каждая её ошибка немедленно упиралась в стену. 29 500 промежуточных теорем это 29 500 мест, где враньё не проходит.

У нас в исламских науках эта проблема решена тысячу лет назад и называется إسناد. Не «шейх сказал», а цепочка передатчиков, каждый из которых проверяем отдельно. И الإجازة, которую не выдают за посещаемость: сядь и сдай наизусть тому, кто сам сдавал. Верификация встроена в сам способ передачи знания.

Так что новость не как «модель осилила Ферма», а как напоминание о том, где ИИ можно отпускать, а где нельзя.

Есть верификатор - отпускай. Компилятор, тесты, замер на весах, шейх, который принимает наизусть. Модель может ошибаться сколько угодно, ошибки отсекутся на входе.

Нет верификатора - не отпускай. Тексты, советы, аналитика, «объясни мне эту тему». Там ошибка выглядит ровно так же убедительно, как правда, и проверять её будешь ты сам, тем самым знанием, за которым и пришёл.

6 миллиардов токенов ради одного слова «доказано» звучит как безумная цена. Но это цена не за доказательство, а за то, что теперь его правильность не надо принимать на веру ни от Уайлса, ни от Claude.

А вот вопрос, который меня по-настоящему цепляет. Формализация тянулась годами именно потому, что была дорогой. Теперь она стоит 11 дней. Что произойдёт с математикой, когда проверяемость перестанет быть роскошью и станет нормой?

И тот же вопрос себе: а где в вашей работе стоит компилятор/верификатор? Если ответа нет, то любой ваш агент работает на честном слове.