Смерть математического эго, или как машинный код и японская философия хоронят бумажную науку
Введение
Современная математика вступила в такую фазу своего развития, когда под вопросом оказывается уже не только истинность отдельных результатов, но и сам исторически сложившийся порядок их удостоверения. По мере роста объёма доказательств, усложнения сетей зависимостей и расширения понятийного аппарата прежний режим ручной проверки всё чаще перестаёт обеспечивать прозрачный и воспроизводимый консенсус. Это не означает, что математика утратила строгость. Это означает иное: её традиционные социальные механизмы подтверждения строгости перестали быть достаточными.
Настоящая статья предлагает интерпретационный подход к этой ситуации. Я исхожу из того, что философский язык Киотской школы — прежде всего понятия места, ничто, нигилизма, пустотности и метаноэтического поворота — позволяет описать происходящий сдвиг как перенос центра эпистемической ответственности от авторитета субъекта к безличному проверочному контуру. При этом Киотская школа используется здесь не как доказательная инстанция и не как источник технических решений, а как инструмент философского чтения уже состоявшихся перемен в математике и формальной инженерии.
1. Не кризис истины, а кризис порядка доверия
Слишком часто говорят, будто современная математика переживает кризис в том смысле, что она утратила собственную строгость. Такая формула неточна. Строгость математического вывода как нормативный идеал не исчезла. Изменился другой уровень — уровень социального и институционального удостоверения того, что именно считается действительно проверенным. Иначе говоря, мы имеем дело не с кризисом математической истины как таковой, а с кризисом исторического режима доверия, внутри которого эта истина прежде удостоверялась.
Долгое время считалось почти само собой разумеющимся, что доказательство — это текст, который при достаточной квалификации, времени и добросовестности в конечном счёте может быть реально удержан и проверен человеком. В этом предположении соединились сразу несколько старых идеалов: вера в локальную обозримость доказательства, вера в техническую мощь рецензента и вера в то, что сообщество способно перевести сложный текст в прозрачное знание. Именно эта связка сегодня систематически даёт сбои. Поэтому в центре современной проблемы находится уже не вопрос «можно ли доказать?», а вопрос «каким образом и в каком именно режиме мы вправе считать доказанное проверенным?».
Ещё в 1979 году Ричард ДеМилло, Ричард Липтон и Алан Перлис сформулировали мысль, которая сегодня читается почти пророчески: математическое доказательство действует не в чистом вакууме логики, а внутри социального процесса признания. Авторы использовали этот тезис как аргумент против чрезмерных надежд на формальную проверку программ. Историческая ирония состоит в том, что именно этот тезис сегодня работает против старой системы. Пока доказательства оставались относительно обозримыми, социальный механизм, возможно, был достаточен. Но когда доказательство превращается в многослойную и распределённую конструкцию, социальное признание перестаёт быть надёжным эквивалентом прозрачной проверки.
В этом смысле в истории фундаментального познания вновь и вновь воспроизводится одна и та же когнитивная ошибка, которую можно описать в терминах, близких анти-овеществляющей линии Киотской школы: рабочая схема, авторитет или даже основание познания начинают мыслиться как самодовлеющая сущность. Там, где должно действовать безличное условие проверки, возникает предмет доверия. Там, где должен работать воспроизводимый контур удостоверения, появляется фигура авторитета. Когда предельное основание незаметно превращается в объект, мысль теряет прозрачность и начинает подменять поиск истины защитой институционального консенсуса.
2. Воеводский и Баззард: момент, когда доверие перестаёт быть достаточным
Наиболее выразительным свидетельством этого перелома остаётся опыт Владимира Воеводского. В лекции 2014 года об истоках и мотивациях унивалентных оснований он не просто вспоминал о собственной ошибке; он дал структурный диагноз всей поздней математической культуре. Его знаменитая формула — что трудный технический аргумент, написанный доверенным автором и похожий на уже известные корректные рассуждения, «почти никогда не проверяется в деталях» — важна именно как диагноз, а не как частная жалоба. В ней зафиксирован переход от строгой проверки к правдоподобию, поддержанному репутацией. Это уже не отдельный человеческий сбой, а изменение самого порядка допуска математического текста к статусу знания. (Воеводский, 2014).
Тот факт, что ошибка была обнаружена лишь спустя годы, и притом в ситуации, когда Пьер Делинь внимательно конспектировал и перепроверял лекции, делает этот эпизод особенно показательным. Проблема здесь не в том, что математики ошибаются: они ошибались всегда. Проблема в другом. Когда теоретическая конструкция становится слишком длинной и слишком плотной, сам институт ручной проверки начинает работать не как прозрачная процедура, а как форма распределённого доверия.
Кевин Баззард описывает ту же проблему уже не в исповедальном, а в институциональном регистре. В докладе The Future of Mathematics? он предлагает намеренно грубое определение: «Доказательство — это то, что старейшины нашего сообщества приняли как корректное». В том же выступлении он замечает, что, по его убеждению, ни один живой или мёртвый человек не знает всех деталей доказательства Великой теоремы Ферма. Смысл этих формул не в эпатаже. Они указывают на реальную смену режима математического доверия: от индивидуальной проверяемости к распределённому и модульному принятию. До определённого момента такая модель работала. Но как только доказательства превращаются в многослойные конструкции с огромным числом скрытых зависимостей, модульность начинает легко переходить в коллективную непрозрачность. (Баззард, 2019).
Особенно сильно у Баззарда звучит не столько пессимизм, сколько новая честность. Он не требует невозможного — не требует, чтобы каждый математик лично удерживал в голове всю громаду поздней дисциплины. Но именно поэтому он так настойчиво указывает на необходимость иного порядка строгости. Иначе говоря, Баззард важен не только как сторонник формализованной математики, но и как один из первых крупных современных математиков, который публично отказался поддерживать старую иллюзию: будто институционального доверия по-прежнему достаточно.
3. IUT как симптом: не спор школ, а перегрузка механизма проверки
Спор вокруг интер-универсальной теории Тейхмюллера Синъити Мотидзуки следует понимать именно в этом ключе. Его значение не сводится к вопросу, правы ли в конечном счёте Мотидзуки или его критики. Исторически важнее другое: математическое сообщество столкнулось с корпусом текстов, по отношению к которому не смогло выработать общезначимый, воспроизводимый и признанный всеми сторонами режим удостоверения.
В 2018 году Петер Шольце и Якоб Стикс после интенсивной работы в Киото написали предельно жёстко: «Мы, авторы этой записки, пришли к выводу, что доказательства нет». Независимо от последующих ответов и новых отчётов, этот эпизод уже вошёл в историю математики как симптом предельной нагрузки на ручной институт проверки. Когда ситуация достигает такого состояния, спор перестаёт быть чисто содержательным. Он становится спором об устройстве самого механизма эпистемического арбитража. (Шольце, Стикс, 2018).
Именно поэтому неправильно говорить, будто проблема касается только одной области — например, высшей арифметической геометрии. В действительности IUT важна не как исключительный экзотический случай, а как крайнее проявление общей тенденции. Чем длиннее доказательство, чем сильнее оно завязано на внутренне плотный понятийный аппарат и чем труднее оно редуцируется к локально обозримым шагам, тем менее весомым становится социальный жест «сообщество в целом приняло». Формальная логика по-прежнему требует доказательства; но исторический способ предъявления и признания доказательства уже не совпадает с тем, каким он был в эпоху, когда доказательный текст реально функционировал как объект индивидуального контроля.
4. Скрытая генеалогия: от de Bruijn к машинно проверенной математике
Если смотреть только на новейшие системы вроде Lean и Coq, легко возникает ложное впечатление, будто формальная проверка — изобретение последних полутора десятилетий. На самом деле её генеалогия значительно глубже.
В 1968 году Николаас Говерт де Брёйн опубликовал отчёт AUTOMATH, a Language for Mathematics, где определил AUTOMATH как язык, предназначенный для «выражения детализированных математических мыслей». Уже здесь содержится радикальная идея: математическое рассуждение можно не просто записывать, а переводить в такую форму, где его корректность становится предметом механической проверки. Это не просто шаг к автоматизации; это раннее переопределение самого математического письма.
Ещё более поразителен малоизвестный сегодня факт, что уже в 1970-е годы эта линия привела к крупной опытной формализации. Ламбертус ван Бентем Юттинг перевёл в систему AUTOMATH книгу Эдмунда Ландау Grundlagen der Analysis, а затем опубликовал отчёт Checking Landau’s “Grundlagen” in the Automath System. Само название этой работы звучит почти как манифест новой эпохи: не комментарий к Ландау, не интерпретация, а именно проверка книги в формальной системе. Этот почти забытый эпизод важен не как курьёз, а как свидетельство того, что кризис ручной верификации был распознан задолго до нынешнего бума искусственного интеллекта и машинной формализации. (de Bruijn, 1968; van Benthem Jutting, 1979).
К этой линии примыкает и Mizar — один из старейших и наиболее устойчивых проектов формализованной математики. В обзорной работе о роли математической библиотеки Mizar её авторы подчёркивают, что Mizar стал одной из пионерских систем, подготовивших почву для современных интерактивных систем доказательства. Особенно важно их замечание о том, что поворотным пунктом стало создание организованных библиотек уже формализованного знания, пригодного для повторного употребления. Это кажется технической деталью, но на деле речь идёт об огромной эпистемологической перемене: математическое знание становится не только публикуемым, но и машинно наследуемым. С 1990 года журнал Formalized Mathematics начал публиковать именно такие тексты. Следовательно, новая математика возникла не вчера и не из компьютерной моды; она имеет собственную и уже достаточно длинную институциональную историю. (Bancerek et al., 2018).
5. Что именно меняют современные системы формальной проверки
Современные системы формальной проверки доказательств важны не потому, что они «мыслят лучше человека», а потому, что они перестраивают доверительную архитектуру математического вывода.
В документации Coq прямо сказано, что при выходе из режима доказательства терм доказательства передаётся ядру, которое проверяет его типовую корректность и совпадение типа с утверждением теоремы. В материалах по Lean объясняется сходная логика: окончательная проверка осуществляется малым доверенным ядром, которое заново воспроизводит и сверяет объект доказательства вне зоны действия потенциально ошибочных или ненадёжных внешних компонентов. Это уже не просто удобный инструмент записи. Это новая модель эпистемической ответственности.
Не менее важен и философский аргумент Робина Поллака. В работе How to Believe a Machine-Checked Proof он формулирует суть вопроса почти предельно: чтобы верить машинно проверенному доказательству, достаточно доверять простому проверяющему устройству, которое не содержит ни эвристик, ни процедур поиска, а лишь проверяет явные выводы в заданной логике. Это чрезвычайно сильная мысль. Машина важна не потому, что она «умнее» математика, а потому, что доверительная поверхность может быть радикально сокращена и вынесена в явно очерченную область. Иначе говоря, мы не устраняем доверие; мы делаем его локальным, прозрачным и поддающимся повторной проверке. В эпистемологическом смысле это почти революция. (Pollack, 1997).
Тот же смысл подчёркивал и Томас Хейлс, когда в очерке Formal Proof напоминал, что ядро HOL Light реализуется очень небольшим объёмом программного кода. Независимо от деталей конкретной реализации, сама идея здесь фундаментальна: огромное пространство современных доказательных построений в конечном счёте должно опираться на минимальную зону доверия. Именно это и делает возможным переход от социального убеждения к проверяемому допуску. И поэтому история формализации гипотезы Кеплера столь показательна: первоначальное доказательство было принято, хотя рецензенты не могли полностью удостоверить все вычислительные компоненты; проект Flyspeck возник как ответ именно на этот дефицит окончательной проверяемости. Позднейшая официальная публикация о завершении проекта подчёркивала, что речь идёт о формальном доказательстве гипотезы Кеплера в сочетании систем HOL Light и Isabelle. (Hales, 2008; Hales et al., 2017).
Здесь важна одна принципиальная оговорка. Формальная система не создаёт «абсолютную истину вообще» и не снимает философских вопросов основания. Она не разрешает споры о выборе аксиом, не отменяет философию математики и не превращает машину в новое божество знания. Она делает другое: резко уменьшает объём безотчётного доверия, который приходится возлагать на человека. В этом и состоит её историческое значение. Мы не устраняем философию; мы перестраиваем практику строгости.
6. Киотская школа как философский язык этого перехода
Именно здесь философский аппарат Киотской школы оказывается особенно плодотворным. Подчеркну: он используется интерпретационно, а не как историко-философская санкция для современных программных архитектур.
В поздней мысли Нисиды Китаро центральным понятием становится бассё — «место», внутри которого возможны различение, суждение и определение. В академических обзорах его поздняя мысль описывается как систематическая попытка выйти за пределы жёсткой субъект-объектной метафизики и показать, что основание мысли не должно отождествляться ни с объектом, ни с эмпирическим субъектом, ни с какой-либо позитивной субстанцией. Основание должно оставаться местом, а не превращаться в вещь. Это уточнение чрезвычайно важно для нашей темы. Кризис ручной верификации возникает там, где место проверки незаметно подменяется фигурой проверяющего. Авторитет автора, статус рецензента, престиж школы и историческая инерция журнала начинают играть роль того, что должно было бы принадлежать безличному контуру удостоверения. Так и возникает реификация авторитета. (Maraldo, 2023; Davis, 2023).
У Ниситани Кэйдзи тот же сюжет получает уже не логическую, а экзистенциальную форму. Центральным в его мышлении оказывается различение нигилизма и пустотности. Нигилизм — это распад прежних опор; пустотность — более глубокий, но не нигилистический уровень преодоления этого распада. В современной математике эта схема читается почти буквально. Кризис старой культуры проверки сперва переживается как распад прежних гарантий: если больше нельзя положиться ни на обозримость длинного доказательства, ни на харизму автора, ни на институт старейшин, не рушится ли сама идея строгого знания? Именно это и есть момент нигилистического шока. Но для Ниситани нигилизм не является последней истиной. Он опасен именно тем, что легко превращается либо в отчаяние, либо в поспешный возврат к старым иллюзиям. Выходом становится поворот — тэнкан — и переход к ку, пустотности, где вещи перестают мыслиться как самодовлеющие и возвращаются в режим структурной взаимосвязанности. В приложении к математике это означает: недостаточно разоблачить несостоятельность старого режима доверия; необходимо выстроить новый режим строгости, в котором объект знания уже не зависит от памяти, статуса и харизмы проверяющего субъекта. (Nishitani, 1982; Davis, 2023).
Танабэ Хадзимэ радикализует этот ход ещё сильнее. Его метаноэтика строится на различении дзирики — собственной силы — и тарики — иной силы. Внутри буддийско-философского контекста это означает отказ считать автономный субъект окончательной опорой мышления и действия. В современной математике это различие приобретает поразительно конкретный смысл. Формализация оказывается актом эпистемической аскезы. Математик отказывается от привилегии быть последним арбитром собственного доказательства и передаёт эту функцию внешнему по отношению к нему режиму проверки. Здесь появляется не исчезновение разума, а его новая форма честности. (Tanabe, 1986; Odin, 1987).
7. Практика уже здесь: Coq, Lean, перфектоидные пространства и Жидкостный тензорный опыт
Практика последних лет показывает, что речь идёт уже не о маргинальной технике. Проект Xena Project прямо формулирует свою цель как вовлечение математиков, особенно студентов старших курсов, в использование систем проверки доказательств. Работы по формализации перфектоидных пространств в Lean показали, что интерактивная система доказательства способна работать не только с длинными доказательствами над сравнительно простыми объектами, но и с современными структурами арифметической геометрии. Авторы статьи Formalising Perfectoid Spaces отмечали, что им удалось формализовать достаточно определений и теорем, чтобы определить перфектоидные пространства в Lean. Тем самым формализация перестала быть занятием для узкого круга логиков и стала частью живого движения поздней математики. (Buzzard, Commelin, Massot, 2020).
Особенно символичен так называемый Жидкостный тензорный опыт. В декабре 2020 года Петер Шольце публично предложил сообществу формальной математики проверить ключевую теорему из собственной работы с Дастином Клаузеном. Позднее Кевин Баззард в отчёте о завершении проекта писал, что этот вызов был доведён до конца в июле 2022 года, причём речь шла о формализации сложной теоремы о сложных объектах — именно того рода задачи, которая ещё недавно казалась принципиально недоступной. В этом эпизоде особенно важно, что машины работали уже не с музейной математикой прошлого, а с живым и ещё не остывшим авангардом дисциплины. (Buzzard, 2022; Scholze, 2022).
8. Цайльбергер, метапонимание и новая роль математика
На этом фоне особенно интересен Дорон Цайльбергер. Его формула «Прощай, понимание; здравствуй, метапонимание» часто воспринимается как чистый технорадикализм. Но за этой провокацией скрыта куда более тонкая мысль. Локальное удержание каждой строки доказательства перестаёт быть единственной и высшей формой математической рациональности. На первый план выходит иная способность — понимать архитектуру метода, устройство доказательной схемы, глобальный рисунок алгоритма и контур проверки. Иначе говоря, понимание смещается с уровня индивидуальной бухгалтерии шагов на уровень проектирования самой формы доказательности. (Zeilberger, 2007).
Цайльбергер довёл эту мысль до почти литературного предела, постоянно указывая в числе соавторов свою программу Шалош Б. Эхад. Имя соавтора действительно представляет собой еврейский перевод названия его раннего компьютера AT&T 3B1. Этот жест мог бы остаться просто эксцентрическим перформансом, если бы не его научный смысл: он сознательно размывает границу между человеческим авторским эго и машинной функцией. Даже если не принимать весь радикализм Цайльбергера, он верно схватывает главное: старая граница между человеческим авторством и машинным участием уже не так неподвижна, как казалось ещё недавно. (Zeilberger, 2007; Wolchover, 2013).
9. Не конец математики, а её следующая форма
Современные достижения искусственного интеллекта усиливают обсуждаемый сдвиг, но не отменяют его человеческого смысла. В статье, опубликованной в Nature в 2025 году, зафиксировано, что система AlphaProof в сочетании с AlphaGeometry 2 решила четыре из шести задач Международной математической олимпиады 2024 года и набрала 28 из 42 баллов, то есть показала результат на уровне серебряной медали. Это, безусловно, историческое достижение. Однако его подлинное значение состоит не в том, что машина якобы уже стала новым метафизическим субъектом математики. Напротив, оно показывает, что проверочный и частично поисковый слои математической работы всё глубже переходят в область формализованной машинной процедуры. Следовательно, роль человека смещается не к исчезновению, а к более высокой и более ответственной форме деятельности: к проектированию объектов, языков, инвариантов и контуров проверки.
Именно поэтому вопрос сегодня стоит не как выбор между «живым пониманием» и «холодной машиной». Реальный вопрос другой: кто и на каком уровне несёт ответственность за строгость. До определённого момента математическая культура держалась на героическом идеале: великий математик мыслился как субъект, который одновременно порождает идею, создаёт язык, удерживает доказательство, локально проверяет связность аргумента и вручную передаёт результат сообществу. В таком образе было величие, но в нём же скрывался и предел. По мере роста теоретической сложности этот идеал начал разрушаться не потому, что человеческий ум внезапно ослабел, а потому, что сама архитектура знания стала несоизмеримой со старым ремесленным форматом. Когда доказательство разрастается до сотен страниц, когда оно зависит от многослойных промежуточных теорий, когда один смысловой блок опирается на десятки других, удержать всё это как единый прозрачный объект индивидуального созерцания становится почти невозможно.
Но из этого не следует, что разум капитулирует. Следует лишь то, что меняется масштаб его ответственности. Заканчивается не математика как деятельность разума, а определённый исторический способ её организации. Уходит в прошлое представление о математике как о ремесле тотального ручного владения каждой локальной деталью. На его место приходит другая модель, в которой человек перестаёт быть последней инстанцией построчной проверки, но становится архитектором более высокого порядка. Он задаёт объект, выбирает язык описания, конструирует инварианты, различает допустимое и недопустимое, проектирует сертификационный контур и определяет, что считать достаточным свидетельством корректности. Машина же отвечает за безличное исполнение этого контура, за воспроизводимую проверку и за точное обнаружение сбоя там, где человек слишком легко поддаётся привычке, авторитету и доверительной инерции.
Именно здесь идея метапонимания приобретает свой подлинный смысл. Когда система вроде AlphaProof производит доказательный ход, который не укладывается в привычную интуицию математика, человеческий разум сталкивается не с собственным упразднением, а с испытанием своей интеллектуальной гордыни. Либо мы отвергаем этот ход из эстетического снобизма, цепляясь за старый ремесленный комфорт, либо признаём, что локальная обозримость отдельного сознания уже не может служить универсальной мерой строгости. Переход к метапониманию означает не отказ от мышления, а согласие мыслить на другом уровне: не на уровне ручного сопровождения каждой строки, а на уровне построения самой архитектуры доказуемости. Мы можем принять непривычный, «чуждый» синтаксис машинного поиска лишь потому, что он в конечном счёте упирается в детерминированный проверочный контур, не подверженный ни внушению, ни усталости, ни институциональному давлению.
Отсюда и вытекает подлинная формула новой эпохи. Не машина заменяет математика, и не человек просто «сотрудничает» с машиной в банальном смысле слова. Меняется само распределение эпистемических функций. Человек всё менее выступает последним механическим контролёром каждой локальной детали и всё более — проектировщиком среды, в которой строгость становится воспроизводимой. Машина всё менее является простым вычислительным орудием и всё более — безличным исполнителем режима проверки. В этом и состоит главный смысл современного перелома: не конец человеческой математики, а её переход к новой форме, в которой разум впервые получает шанс освободиться от кустарного бремени тотального ручного контроля и стать архитектором мира, где сложность подчиняется проверяемой форме.
10. GALO AI
Если довести обсуждаемую линию до её инженерного предела, становится ясно, что вопрос уже не исчерпывается судьбой доказательств в чистой математике. На первый план выходит более общий и более жёсткий вопрос: возможна ли такая архитектура вычислительного интеллекта, в которой строгость, воспроизводимость и проверяемость не навешиваются на систему извне в качестве позднего аудита, а изначально встраиваются в само устройство её ядра? Именно в этом горизонте и следует рассматривать архитектуру GALO, разрабатываемую автором (мной).
Исходный замысел GALO состоит в отказе от приоритета эвристически эффективного, но внутренне непрозрачного вычисления в пользу структурно закреплённого и сертифицируемого режима работы. В центре такой архитектуры находятся конечные носители, таблично заданные операции, явно фиксируемые инварианты и независимый проверочный контур, который при любом нарушении не ограничивается общим сигналом сбоя, а обязан предъявить точное свидетельство несостоятельности конкретного перехода. Тем самым радикально меняется само понимание интеллектуальной системы. Она мыслится уже не как чёрный ящик, выдающий статистически правдоподобные ответы, а как дисциплинированная вычислительная среда, где каждый существенный шаг должен быть либо воспроизводимо подтверждён, либо воспроизводимо отвергнут.
В этом отношении GALO представляет собой не просто ещё одну техническую реализацию, а инженерный ответ на тот самый кризис режима доверия, о котором шла речь выше. Если старая математическая культура всё дольше держалась на распределённом авторитете, а современная формализованная математика ищет выход в сокращении доверительной поверхности, то детерминированные архитектуры нового типа делают следующий шаг: они стремятся построить сам вычислительный процесс так, чтобы источник эпистемической непрозрачности был минимизирован не постфактум, а на уровне исходной конструкции. Иначе говоря, задача проверки переносится с внешнего уровня контроля на уровень онтологии самой системы.
Отсюда вытекает и более сильный тезис. GALO претендует не просто на повышение надёжности по сравнению с вероятностными моделями, а на смену самого вычислительного идеала. Речь идёт о переходе от культуры правдоподобия к культуре сертифицируемого перехода, от эмпирически полезного ответа — к структурно удостоверяемому результату, от харизмы модели — к прозрачности её вычислительного контура. В этом смысле GALO может рассматриваться как попытка построить такой тип интеллектуальной архитектуры, в котором вопрос о строгости решается не после вычисления, а до него — на уровне самой формы допустимого действия.
Заключение
Интеграция систем формальной проверки в ядро академической математики диктуется не наивным техноутопизмом и не поверхностной верой в то, будто машина «умнее» человека. Этот переход продиктован куда более серьёзной причиной: исчерпанием старого режима эпистемического доверия. Кризис ручного рецензирования — это не частная неудача нескольких сложных текстов и не временное затруднение на переднем крае науки. Это симптом более глубокой болезни, связанной с тем, что математическая культура слишком долго опиралась на авторитет, распределённое доверие и институциональную инерцию там, где требовался воспроизводимый и безличный контур удостоверения.
История Владимира Воеводского, спор вокруг интер-универсальной теории Тейхмюллера, институциональные диагнозы Кевина Баззарда, ранняя линия от AUTOMATH к формализованной математике, проекты Гонтье и Хейлса, современные достижения Lean, Coq и машинного доказательного поиска — всё это не разрозненные сюжеты, а звенья одного и того же исторического процесса. Математика постепенно перестраивает не свою внутреннюю логическую природу, а форму допуска к строгости. Иначе говоря, меняется не сама истина, а способ её культурного, институционального и вычислительного удостоверения.
Философия Киотской школы даёт для этого перелома редкий по точности язык. Нисида позволяет увидеть опасность превращения основания в предмет. Ниситани — драму распада старых опор и различие между нигилистическим крахом и более глубоким преодолением этого краха. Танабэ — необходимость метаноэтического поворота, в котором субъект отказывается считать себя самодостаточным и соглашается пройти через дисциплину внешнего по отношению к нему контура. Если перевести эту оптику в область математики, то формальная проверка предстаёт не как конец разума, а как новая форма его честности. Машина не становится новым абсолютом. Но она заставляет разум отказаться от старой привилегии — быть последней инстанцией собственной правоты.
Отсюда вытекает и более широкий вывод. Мы входим в эпоху, где интеллектуальная добросовестность всё меньше измеряется способностью производить впечатление глубины и всё больше — способностью строить такие формы знания, которые выдерживают независимую проверку. Это относится не только к доказательству теорем, но и к архитектуре вычислительных систем, к устройству интеллектуальных ядер, к самому понятию научной ответственности. Именно здесь становятся особенно важны проекты нового типа, в которых проверяемость, воспроизводимость и точное свидетельство сбоя встроены в саму конструкцию системы, а не добавляются к ней задним числом в качестве красивой юридической оболочки.
В этом смысле будущее принадлежит не тем, кто громче всех говорит о сложности, гениальности и интуиции, а тем, кто сумеет подчинить сложность форме. Перед нами не спор между человеком и машиной, не романтическая дуэль живого духа с холодным алгоритмом, а куда более глубокий вопрос: способна ли цивилизация отказаться от интеллектуального феодализма, в котором истина допускается через авторитет, и перейти к такому режиму, где истина допускается только через воспроизводимую структуру проверки.
И если академическая математика не встроит этот переход в собственное ядро, она рискует сохранить внешний блеск и внутренне превратиться в прекрасно организованный музей. В таком музее будут по-прежнему звучать громкие имена, вручаться премии, произноситься торжественные речи и публиковаться тексты, которые всё меньше кто-либо способен по-настоящему проверить. Это будет уже не живая строгая наука, а ритуал памяти о ней.
Напротив, подлинно новая математика начнётся там, где закончится культ недоказуемого авторитета. Она начнётся там, где исследователь перестанет играть роль жреца тайного знания и примет на себя более тяжёлую, но и более благородную роль архитектора проверяемой формы. И если этот переход состоится, то историки будущего, вероятно, будут смотреть на нашу эпоху так же, как мы смотрим на позднюю схоластику: с уважением к её изощрённости, но и с ясным пониманием того, что её внутренний предел уже был достигнут.
Именно поэтому нынешний поворот столь важен. Он меняет не только технику доказательства. Он меняет нравственную форму научной строгости. Он меняет само представление о разуме. И он бесповоротно ставит перед нами вопрос, от которого уже невозможно уклониться: хотим ли мы и дальше жить в культуре правдоподобия, или всё-таки готовы войти в культуру доказуемой ответственности.
Список литературы
Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pąk, K. The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar // Journal of Automated Reasoning. 2018. Vol. 61. P. 9–32.
de Bruijn, N. G. AUTOMATH, a Language for Mathematics. T.H.-Report 68-WSK-05. Eindhoven: Technische Hogeschool Eindhoven, 1968.
Buzzard, K. The Future of Mathematics? Доклад в Microsoft Research. 2019.
Buzzard, K. Beyond the Liquid Tensor Experiment. 2022.
Buzzard, K., Commelin, J., Massot, P. Formalising Perfectoid Spaces // Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. New York: ACM, 2020. P. 299–312.
DeMillo, R. A., Lipton, R. J., Perlis, A. J. Social Processes and Proofs of Theorems and Programs // Communications of the ACM. 1979. Vol. 22. No. 5. P. 271–280.
de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J. The Lean Theorem Prover (System Description) // Automated Deduction — CADE-25. Cham: Springer, 2015. P. 378–388.
Davis, B. W. The Kyoto School // Zalta, E. N., Nodelman, U. (eds.). The Stanford Encyclopedia of Philosophy. 2023.
Gonthier, G. The Four Colour Theorem: Engineering of a Formal Proof // Kapur, D. (ed.). Computer Mathematics. Berlin; Heidelberg: Springer, 2007.
Gonthier, G. et al. A Machine-Checked Proof of the Odd Order Theorem // Interactive Theorem Proving. Berlin; Heidelberg: Springer, 2013. P. 163–179.
Hales, T. C. Formal Proof // Notices of the American Mathematical Society. 2008. Vol. 55. No. 11. P. 1370–1380.
Hales, T. et al. A Formal Proof of the Kepler Conjecture // Forum of Mathematics, Pi. 2017. Vol. 5. Article e2.
Hubert, T. et al. Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning // Nature. 2025. Vol. 647. P. 723–729.
van Benthem Jutting, L. S. Checking Landau’s “Grundlagen” in the Automath System. Mathematical Centre Tracts 83. Amsterdam: Mathematisch Centrum, 1979.
Maraldo, J. C. Nishida Kitarō // Zalta, E. N., Nodelman, U. (eds.). The Stanford Encyclopedia of Philosophy. 2023.
Nishida, K. Last Writings: Nothingness and the Religious Worldview. Пер. D. A. Dilworth. Honolulu: University of Hawai‘i Press, 1987.
Nishitani, K. Religion and Nothingness. Пер. J. Van Bragt. Berkeley: University of California Press, 1982.
Pollack, R. How to Believe a Machine-Checked Proof // BRICS Report Series. 1997. Vol. 4. No. 18.
Scholze, P. Liquid Tensor Experiment // Experimental Mathematics. 2022. Vol. 31. No. 2. P. 349–354.
Scholze, P., Stix, J. Why abc is Still a Conjecture. Bonn, 2018.
Tanabe, H. Philosophy as Metanoetics. Пер. Y. Takeuchi, V. Viglielmo, J. W. Heisig. Berkeley: University of California Press, 1986.
The Coq/Rocq Proof Assistant Reference Manual.
The Lean Language Reference.
Voevodsky, V. The Origins and Motivations of Univalent Foundations // The Institute Letter. Summer 2014. Princeton, NJ: Institute for Advanced Study. P. 8–11.
Wolchover, N. In Computers We Trust? // Quanta Magazine. 2013.
Zeilberger, D. Opinion 84: Bye-Bye Understanding, Hello Meta-Understanding. Rutgers University. 2007.
