Выскажусь про гремящий новостной повод: на прошлой неделе «ИИ» «доказал» «семьсот» «теорем», «математика» «в опасности».

На этом канале я постоянно подшучиваю над современными математиками и говорю, что их рыжие кудри изрядно примелькались. За целый год до публичного выпуска ChatGPT я предсказал, что игнорировать успехи в компьютерной формализации математики им будет нельзя.

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

Я часто повторяю, что у меня «плохо» с математикой, и я её «не понимаю», но я имею ввиду нечто другое, нежели 99% населения Земли, когда они говорят, что у них плохо с математикой, и они её не понимают. По сравнению с 99% населения Земли мне «легко» даются математические предметы: я способен учиться решать задачи и сдавать эзамены.

«Плохо» в моем случае означает, что я не получаю от процесса «удоволетворения», потому что нотация и структура доказательств в учебниках математики для меня недостаточно формальны и, как следствие, «непонятны» (легкая форма аутизма). Долгое время я списывал «непонимание» на обстоятельства среды в ракетном ПТУ на Яузе, там не было ни сильных преподавателей, которые могли что-то объяснить, ни сильных студентов, которые хотели что-то понять. Откосить от армии, бухнуть на скамеечке у «Самохвала», не лишиться койки в общаге — такой был уровень контингента.

Лишь чудом попав в аспирантуру по столярному делу и познакомившись с шведским и шотландским уставами^W^W^W^Wсистемами формальных доказательств, основанных на интуиционистских логиках, где есть т.н. «вычислительное содержание» (доказательства теорем соответствуют компьютерным программам, и наоборот), я смог, наконец-то, «понять» программу математики для младшекурсников инженерных специальностей!

Помню свой восторг по этому поводу, но он продолжался недолго. Оказалось, что я, все же, не математик. Математика не сводится к логике и существует вне её, несмотря на то, что математический прогресс отчасти опирается на логический инструментарий, равно как и физика не сводится к математике и существует вне её, хотя и пользуется математическим инструментарием.

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

Я могу пойти еще дальше и сказать, что обещанный рост скорости роста математического знания до порога, за которым это знание перестает понимать человек, не имеет смысла, потому что математика это и есть занятие, благодаря которому человек может что-то сам понять. «Нечеловеческая математика» это оксюморон.

Американцам сложно это объяснить, потому что они буксуют за пределами схемы «товар-деньги-товар». В представлении американца математик это азиат, который черкает какие-то свои азиатские закорючки мелом на доске. Значит, можно «решить всю математику», заменив азиата на «китайский мозг» языковых моделей.

Таким методом можно «решить» что угодно. Например, к 1991 году СССР «решил» не только всю математику, но всю физику, всю химию, всю биологию и все прочие науки: кандидаты и доктора, младшие и старшие научные сотрудники массово отправились на улицу торговать турецкими пуховиками. Нужда в них отпала, потому что была остановлена гонка ядерных вооружений.

В Кремниевой Долине тоже можно сказать: ара пох чка, всем спасибо, все свободны. Математики за первый курс (анализ и линейная алгебра), второй (многомерный анализ и теория вероятности) и немного за третий (теория оптимизации) достаточно, чтобы «решить» все проблемы человечества. Нечего прохлаждаться за деньги налогоплательщиков. Экономика должна быть экономной!