Продукт математики — ясность и понимание, а не теоремы сами по себе. Так считал Билл Тёрстон, и это стало лейтмотивом эссе математика и основателя стартапа Дэвида Бессиса. Он рассказывает, как его лучшая теорема так и не была опубликована — он оставил её намёком на слайде, уйдя в машинное обучение. Его второй лучший результат — Theorem 0.5 в препринте по Garside categories — тоже лёг под сукно. Доказать её было легко, сложность была в другом: придумать концептуальную рамку, в которой она становится очевидной. Настоящая инновация, по Бессису, — не сама теорема, а язык, который её породил, в частности Definitions 2.4 и 9.3. Этот язык позже вошёл в 700-страничную книгу, а сам Бессис использовал Definition 9.3 для решения задачи K(π,1), что подняло его статус. Но, признаётся он, «социальный паразит», решивший гипотезу, — всего лишь тень того математика, который придумал определения.
Бессис противопоставляет «официальную математику» (формальный вывод из аксиом) и «секретную» (интуицию, смысл, нейронную подоплёку). Официальная — это холодная логика, предмет гордости. Секретная — то, о чём не принято говорить: «Первое правило Клуба Интуиции — не упоминать Клуб Интуиции». Он цитирует Г. Х. Харди, который презирал «объяснятелей», и вспоминает ответ Тёрстона на MathOverflow: математика — это про передачу понимания в живом сообществе, а не про кучу теорем.
Но, по мнению Бессиса, эта система дала трещину. Сейчас ИИ, по словам Джеффа Хинтона, сравнивают с Go и шахматами — «закрытой системой с правилами». Это фундаментальная ошибка. Проект First Proof показал, что модели (Google, OpenAI) решили 6–8 из 10 задач, но с оговорками: сгенерировали горы мусора, не могли отличить правильное от неправильного, а решения были нечитаемы. OpenAI сам не знал, какие ответы верны, — пришлось звать математиков-волонтёров. Бессис называет это ключевым моментом: в человеческой математике доказательство и создание концепций идут рука об руку, а у ИИ «смысл» отсутствует. Проблема усугубляется autoformalization. Стартап Math Inc сумел перевести работу Вязовской о сфере в формальный код Lean, но это был «200-тысячный неаудированный виб-код», который никто не рискнёт влить в master. Сообщество математиков требует канонизации — чтобы код был общим, переиспользуемым и понятным человеку. Пока единственный «компилятор», способный оценить ценность доказательства, — это человеческий мозг.