Хлеб математиков
Что ещё интересно про теорему Гёделя - это контекст, в котором она появилась и против чего она использовалась, как аргумент.
Дело в том, что в 1920-х компьютеры уже маячили на горизонте. В том смысле, что, несмотря на некоторое количество уже созданных счётных машин, они всё ещё оставались фантазией - хрен знает, какими свойствами оная будет обладать. Однако сия фантазия была уже сродни фантазиям 1950-х о полётах в космос: тоже ещё неясно во всех деталях, как оно там будет, но при этом уже ясно, что оно точно возможно, а потому точно как-то будет, причём совсем скоро.
Под этим соусом, разумеется, увлечённые вопросом строили планы и проекты, как эту штуку, которой ещё нет, но которая уже вот-вот, приспособить к народному хозяйству, под коим понималась в основном математика (ну да, машина же - «счётная», а считают - в математике, как ещё-то?).
В результате, у математика Гильберта и ряда его коллег возникла отличная идея.
Машина не устаёт и не ошибается, поэтому мы сделаем с её помощью то, на что у человеков сил не хватает. А именно сформулируем все базовые положения математики и логики в виде некоторого набора аксиом, представляющих из себя правила замены фрагмента формального текстового выражения на какой-то другой фрагмент. И потом запустим полный перебор.
Вполне понятно, что, ввиду потенциальной неограниченности выражений по длине, мы никогда не переберём их все. Но нас вполне устраивает, если мы переберём все осмысленные формальные выражения, скажем, длиной до десяти тысяч знаков - один хрен, теорем, которые в своей формальной записи длиннее, мы ещё не встречали.
«Формальное выражение» - это буквально тот самый текст, который пишется промеж рассуждений на естественном языке.
Например, «x + y = y + x».
А «правило замены» это формальная запись такой модификации текста выражения, которую мы считаем всегда сохраняющей истинность выражения.
Например, «x + 0 → x».
Таким образом, например, можно взять выражение
«x + y = y + x + 0»
И получить из него при помощи данного правила замены вышеуказанное
«x + y = y + x»
Таким способом мы проверим вообще все осмысленные выражения математики на корректность и получим полный набор истинных и ложных формальных выражений, для каждого из которых у нас будет доказательство ложности или истинности: протокол всех текстовых замен в стартовом выражении, которые ведут к какому-то ещё.
Причём сделает это компьютер, которому не лень, не западло, не скучно, перепоя не бывает и внимание у него не рассеянное. Шах и мат, аметисты, у нас все ходы записаны.
Ну или почти все - до десяти тысяч знаков для начала. Однако, поскольку компу не лень, он и дальше тоже продолжит перебирать. И будет перебирать сколь угодно долго, покрывая формальной проверкой всё более и более длинные выражения.
От такого, разумеется, у многих бомбануло.
Дело в том, что это со стороны кажется, будто бы математики - это как компьютеры: ничего кроме циферок и тупых операций с ними не видят. Сами же математики, напротив, про себя зачастую считают, будто они запредельно творческие, и даже сложение в столбик у них прямо как поэзия. Что, впрочем, до внедрения алгоритмических методов в массы правда примерно таким и было: без заранее прописанной последовательности действий даже для решения примитивных в восприятии современника задач приходилось развивать в себе недюжинную изобретательность и очень нехило изощряться.
А уж доказательство теорем - это такое творчество, по сравнению с которым все художники и музыканты - примитивные ремесленники. Только человек - причём особо одарённый смекалкой и фантазией - на такое способен. Счёт в столбик мы, так и быть, передадим подмастерьям, но теоремы-то, теоремы! Отдать их даже не подмастерьям, а вообще какой-то железяке? Да как можно?!
Я не шучу: реал, не только в книгах начала двадцатого века за авторством самых настоящих математиков можно прочитать про такое, но и даже в более поздних - взять того же Пенроуза… Причём и в книгах двадцать первого века это изрядно представлено.
В общем, с одной стороны, подгорает от того, что «железяка отнимет наш хлеб», а с другой - от того, что «железяка в интеллектуальном плане будет не хуже нас».
Но, к счастью, мы скажем, что так несчитово: она так может только с её железячными читами - при помощи механического перебора. Человек, правда, это тоже может в основном только при помощи перебора (эффективного - с предварительным отсечением заведомо тупиковых веток), но в этом всё равно есть полёт и творчество, поскольку он - Человек. Не чета бездушной железяке.
В общем, очень многим в те времена очень хотелось доказать, что с железяками и перебором у вас, технократы, не выгорит. Что Человек может что-то такое, чего принципиально не сможет машина. Что математики в своей человеческой ипостаси никогда не исчезнут. Что нет никаких причин беспокоиться.
Однако вполне понятно, что одно дело заявить «никогда не сможет», но совсем другое - что-то противопоставить алгоритмам, про которые вполне понятно, что, во-первых, они сработают, а во-вторых, их можно запрограммировать (во всяком случае, в доминирующих на тот момент фантастических гипотезах о ближайшем будущем). Тут как бы философия против практики: психологически тяжело на конференции отрицать возможность построения самолёта, когда ты именно на нём на эту конференцию и прилетел.
На тот момент, правда, «самолёта» ещё не было, но на бумажке предложенный метод работал и при этом довольно правдоподобно имитировал финальные результаты живых математиков. И, собственно, сопротивляться ему получалось лишь в том смысле, что «этот ваш “самолёт” даже черепаха обгоняет».
Но обгоняет-то пока оно на бумажке - построй машину, которая считает в тысячу раз быстрее, и всё, аметисты - шах и мат. А если в миллиард раз, то вообще туши свет: никто не сможет сопротивляться.
В общем, ситуация была примерно такой, какой она была в девяностых с шахматами: «компьютер человека никогда не обыграет» уже говорилось как бы в отчаянии, из последних сил. Непричастный ещё мог в это верить, но причастным оставалось только надеяться, что откуда-то возникнет чудесная сила, которая не даст компьютерам совершить последний шаг, после которого в шахматах вечными проигравшими будут уже люди, включая ихних чемпионов мира, хотя совсем ведь ещё недавно компьютер в шахматы обыгрывали даже среднеталантливые школьники.
Собственно, Гёдель такое вот «“у вас с вашими компами ничего не получится” из последних сил» и выдал в виде своих теорем. Причём выдал как раз на той конференции, где обсуждалось, как именно и как скоро всё получится.
Для этих целей он взял давно известную модификацию «парадокса лжеца», которая заключалась в том, что писалось суждение «суждение в красной рамке недоказуемо» и обводилось красной рамкой.
До того момента сие считалось чисто текстовым парадоксом, но компьютеры в своей фантастической интерпретации полагались строго «счётными машинами», а потому это суждение следовало выразить «на языке чисел», чтобы всё стало «честно и научно».
Сейчас всем понятно, что компьютер может и в тексты, и в рисунки, и в музыку, но тогда таковое если кому-то и приходило в голову, то остальным казалось совсем уже запредельно фантастическим. А вот с числами и счётом - да, он может.
В результате, Гёдель придумал очень корявый по нынешним временам способ взаимно однозначного кодирования текстового выражения в число. Это сейчас почти всем почти сразу понятно, что в компьютере любой текст в файле хранится в виде цепочки чисел, которую можно трактовать как одно очень длинное, а тогда сие было неочевидно.
Кроме того, в число кодировались последовательности результатов текстовых замен, поскольку то, что последовательность чисел и даже текстовых строк в компьютере можно хранить и идентифицировать легко и непринуждённо, тоже было ещё не очевидно (а чего вы хотите во времена «машины Тьюринга» - с её помощью даже два числа сложить не так-то просто).
Кроме того, он с помощью этих кодировок придумал, как записать то, что сейчас в куче языков программирования называется «this» - ссылка изнутри объекта на сам этот объект.
Когда это перекочевало из текстовой формы в численную, для тогдашних математиков оно стало как бы «честным», «научным» и «убедительным», а потому вроде как уже могло использоваться в качестве аргумента, тогда как в текстовой форме разновидность «парадокса лжеца» вряд ли кого-то из них в чём-то бы убедила - все ж про неё давно уже знали и так.
Таким образом, есть способ трансляции суждений в числа. Есть этот ваш «алгоритм перебора». И есть некоторое суждение - «модифицированный парадокс лжеца» - на котором этот ваш алгоритм как бы сломается.
Поскольку мало кто представлял себе, что вообще такое «алгоритм в виде программы», прыжки с чисел на логические трактовки текстов, которые они кодируют, и обратно были восприняты как реальное доказательство чего-то критически важного. Например, того, что как бы есть такие числа или операции с оными, с которыми какой-то там компьютерный алгоритм как бы принципиально не справится.
И, с другой стороны, есть Гёдель, который человек, а потому как бы смог, в отличие от этих ваших железяк. Шах и мат, технократы. Компьютер никогда не обыграет человека в математику.
Хрен знает почему, но существование вот этой единственной фразы, про которую «в виде рассуждений на человеческом языке» как бы что-то можно доказать, если много раз натянуть сову на глобус, а вот компьютер «в неё не сможет», убедило кучу тогдашних математиков, что можно даже не трепыхаться: типа, если компьютер чего-то не сможет, то тогда и не надо с его помощью делать вообще что-либо из этой области. И из гипотетического девайса для доказательств он в их восприятии превратился обратно в продвинутую машинку для вычислений - как арифмометр, но только на электричестве.
Правда, к счастью, после появления реальных компьютеров изрядной части программистов было болт положить на всю эту философию, а потому уже лет через десять-пятнадцать автоматические компьютерные доказательства они стали пытаться реализовывать. К девяностым софт уже умел в плане «доказательств перебором» весьма много и в некоторых областях обгонял в этом любого отдельно взятого человека, а сейчас, в 2020-м, он таки да, по заветам Гильберта уже умеет искать доказательства или опровержения для полноценных формальных систем. Причём запрограммировать сам перебор всех возможных текстовых замен, даже если бы он не был встроен в уже существующие библиотеки, на современном языке - дело нескольких часов.
Хотя, таки да, в «парадокс лжеца» компьютер всё ещё не может.
Поскольку в него, на самом деле, не могут и сами люди тоже.
Дело в том, что там проблема не столько в том, чтобы запрограммировать функцию перебора, которая «не сломается», сколько в том, чтобы закодировать само суждение, сохранив и его смысл, и смысл некого «доказательства» касательно него. Это суждение, будучи записанным в тексте, выглядит осмысленным, но на самом деле оно бессмысленно, а потому, видимо, вообще нет аксиоматики, в которой смысл у него появится. Да и аксиоматик, в которой это суждение вообще будет вычислимым, тоже не особо много.
Однако если сосредоточиться на очень нетривиальном переводе его текстовой версии в числа и обратно, то действительно можно не заметить, что где-то в глубине этих конвертаций смысл из выражения исчез и в «численной» его версии тоже.
Но это уже дополнительные детали. Более интересно в этой истории то, что тут мы имеем дело с «богом белых пятен». То, что изначально предназначалось для «фиг вам, технократы», в какой-то момент стало в этой области вообще совсем неприменимо. Поскольку по понятным причинам для работающих с реальными компьютерами давнишние фантазии о будущих гипотетических интересны исключительно как история отрасли или художественные произведения, но не как адекватное современности руководство к действию.
Однако быть удобными для обоснования утешающего тезиса «всегда будет хлеб для живого математика» оно не перестало - просто переместилось туда, где практика ещё не сделала эту философию очевидно бессмысленной. Поэтому с «мы тут говорим о счётных машинах» оно откочевало к общематематической философии и как бы уже там стало гарантировать, что «в математике всегда будет нужна фантазия» и т.п.
Но удобство, разумеется, на этом не закончилось, а потому к «живым математикам» в борьбе за свой хлеб методом теоремы Гёделя присоединились ещё и мистики с шарлатанами, которые на базе того же самого начали утверждать, что «математикой и этой вашей наукой нельзя познать мир во всей его сложности, поэтому покупайте нашу эзотерику - у вас просто нет другого выхода».
Заметьте, это всё на базе одного и того же утверждения, «доказанного» одним и тем же способом: расплывчатые обобщающие формулировки действительно могут творить чудеса: от «нате вам, технократы» к «а вот хрен всей этой вашей науке» за неполный век - неплохой результат, да?
Что касается меня, то я-то родился не в начале двадцатого века, а считать не любил вообще никогда. Поэтому умом я могу понять переживания по поводу того, что у математиков сначала отбирают счёт в столбик, потом численное моделирование, потом аналитическое решение уравнений, потом взятие интегралов, а потом и доказательства, но никаких эмоций по этому поводу ощутить уже не могу.
Ну, кроме положительных.
Да, возможно, для кого-то «заниматься математикой» и «считать в столбик» неразрывно связано, из-за чего появление компьютеров им кажется чем-то сродни появлению автомобилей с точки зрения извозчика.
Для более продвинутых отдать сложение и умножение компьютеру - Ок, но вот поиск формальных доказательств - уже страшно. Типа как для таксиста появление робота-водителя.
И вот всем им надо утешать себя рассуждениями в стиле «компьютеры никогда не смогут», плавно трансформирующихся, аки «бог белых пятен», в «мир сложен и непознаваем этими вашими железяками и науками».
Но вот мне утешать себя что-то как-то не надо.
С моей точки зрения, если компьютер будет делать вообще всё техническое, включая поиск доказательств и даже поиск всех истинных для некоторой аксиоматики суждений, то это зашибись, поскольку самая интересная часть занятий математикой - ставить вопросы о чём-то, что есть или может быть в мире. Формулировка задачи и разработка языка, на котором её можно описать, - вот самая офигенная штука. И этой штукой компьютеры смогут полноценно заниматься весьма нескоро, поэтому все переживающие о вытеснении могут спасть спокойно - по крайней мере, ещё полвека.
А вот считать и искать перебором - да пожалуйста, пусть это делает компьютер. Я буду только рад, поскольку и сейчас стараюсь спихнуть на компьютер вообще всё, что только можно.
Но вот «счетоводам» и прочим любителям тёплой аналоговой бумажки наверно стрёмно.
Впрочем, так уже не первый раз: наверняка в то время, когда сначала вручную, а потом машинным путём создавались, например, таблицы логарифмов, одни этому радовались, а у других от этого бомбило - ведь теперь к ним реже будут обращаться с заказами на механические расчёты. Их клёвый навык обесценивается на глазах. Их статус тает. Обидно.
В общем, будьте уверены, если хоть где-то разговор перешёл с инженерных вопросов на философские, то там совершенно точно есть целая куча чьих-то обидок и страхов. Причём если в этом хоть как-то фигурируют компьютеры - пусть даже гипотетические: сто процентов, что всё это там есть.
doc-файл
Дело в том, что в 1920-х компьютеры уже маячили на горизонте. В том смысле, что, несмотря на некоторое количество уже созданных счётных машин, они всё ещё оставались фантазией - хрен знает, какими свойствами оная будет обладать. Однако сия фантазия была уже сродни фантазиям 1950-х о полётах в космос: тоже ещё неясно во всех деталях, как оно там будет, но при этом уже ясно, что оно точно возможно, а потому точно как-то будет, причём совсем скоро.
Под этим соусом, разумеется, увлечённые вопросом строили планы и проекты, как эту штуку, которой ещё нет, но которая уже вот-вот, приспособить к народному хозяйству, под коим понималась в основном математика (ну да, машина же - «счётная», а считают - в математике, как ещё-то?).
В результате, у математика Гильберта и ряда его коллег возникла отличная идея.
Машина не устаёт и не ошибается, поэтому мы сделаем с её помощью то, на что у человеков сил не хватает. А именно сформулируем все базовые положения математики и логики в виде некоторого набора аксиом, представляющих из себя правила замены фрагмента формального текстового выражения на какой-то другой фрагмент. И потом запустим полный перебор.
Вполне понятно, что, ввиду потенциальной неограниченности выражений по длине, мы никогда не переберём их все. Но нас вполне устраивает, если мы переберём все осмысленные формальные выражения, скажем, длиной до десяти тысяч знаков - один хрен, теорем, которые в своей формальной записи длиннее, мы ещё не встречали.
«Формальное выражение» - это буквально тот самый текст, который пишется промеж рассуждений на естественном языке.
Например, «x + y = y + x».
А «правило замены» это формальная запись такой модификации текста выражения, которую мы считаем всегда сохраняющей истинность выражения.
Например, «x + 0 → x».
Таким образом, например, можно взять выражение
«x + y = y + x + 0»
И получить из него при помощи данного правила замены вышеуказанное
«x + y = y + x»
Таким способом мы проверим вообще все осмысленные выражения математики на корректность и получим полный набор истинных и ложных формальных выражений, для каждого из которых у нас будет доказательство ложности или истинности: протокол всех текстовых замен в стартовом выражении, которые ведут к какому-то ещё.
Причём сделает это компьютер, которому не лень, не западло, не скучно, перепоя не бывает и внимание у него не рассеянное. Шах и мат, аметисты, у нас все ходы записаны.
Ну или почти все - до десяти тысяч знаков для начала. Однако, поскольку компу не лень, он и дальше тоже продолжит перебирать. И будет перебирать сколь угодно долго, покрывая формальной проверкой всё более и более длинные выражения.
От такого, разумеется, у многих бомбануло.
Дело в том, что это со стороны кажется, будто бы математики - это как компьютеры: ничего кроме циферок и тупых операций с ними не видят. Сами же математики, напротив, про себя зачастую считают, будто они запредельно творческие, и даже сложение в столбик у них прямо как поэзия. Что, впрочем, до внедрения алгоритмических методов в массы правда примерно таким и было: без заранее прописанной последовательности действий даже для решения примитивных в восприятии современника задач приходилось развивать в себе недюжинную изобретательность и очень нехило изощряться.
А уж доказательство теорем - это такое творчество, по сравнению с которым все художники и музыканты - примитивные ремесленники. Только человек - причём особо одарённый смекалкой и фантазией - на такое способен. Счёт в столбик мы, так и быть, передадим подмастерьям, но теоремы-то, теоремы! Отдать их даже не подмастерьям, а вообще какой-то железяке? Да как можно?!
Я не шучу: реал, не только в книгах начала двадцатого века за авторством самых настоящих математиков можно прочитать про такое, но и даже в более поздних - взять того же Пенроуза… Причём и в книгах двадцать первого века это изрядно представлено.
В общем, с одной стороны, подгорает от того, что «железяка отнимет наш хлеб», а с другой - от того, что «железяка в интеллектуальном плане будет не хуже нас».
Но, к счастью, мы скажем, что так несчитово: она так может только с её железячными читами - при помощи механического перебора. Человек, правда, это тоже может в основном только при помощи перебора (эффективного - с предварительным отсечением заведомо тупиковых веток), но в этом всё равно есть полёт и творчество, поскольку он - Человек. Не чета бездушной железяке.
В общем, очень многим в те времена очень хотелось доказать, что с железяками и перебором у вас, технократы, не выгорит. Что Человек может что-то такое, чего принципиально не сможет машина. Что математики в своей человеческой ипостаси никогда не исчезнут. Что нет никаких причин беспокоиться.
Однако вполне понятно, что одно дело заявить «никогда не сможет», но совсем другое - что-то противопоставить алгоритмам, про которые вполне понятно, что, во-первых, они сработают, а во-вторых, их можно запрограммировать (во всяком случае, в доминирующих на тот момент фантастических гипотезах о ближайшем будущем). Тут как бы философия против практики: психологически тяжело на конференции отрицать возможность построения самолёта, когда ты именно на нём на эту конференцию и прилетел.
На тот момент, правда, «самолёта» ещё не было, но на бумажке предложенный метод работал и при этом довольно правдоподобно имитировал финальные результаты живых математиков. И, собственно, сопротивляться ему получалось лишь в том смысле, что «этот ваш “самолёт” даже черепаха обгоняет».
Но обгоняет-то пока оно на бумажке - построй машину, которая считает в тысячу раз быстрее, и всё, аметисты - шах и мат. А если в миллиард раз, то вообще туши свет: никто не сможет сопротивляться.
В общем, ситуация была примерно такой, какой она была в девяностых с шахматами: «компьютер человека никогда не обыграет» уже говорилось как бы в отчаянии, из последних сил. Непричастный ещё мог в это верить, но причастным оставалось только надеяться, что откуда-то возникнет чудесная сила, которая не даст компьютерам совершить последний шаг, после которого в шахматах вечными проигравшими будут уже люди, включая ихних чемпионов мира, хотя совсем ведь ещё недавно компьютер в шахматы обыгрывали даже среднеталантливые школьники.
Собственно, Гёдель такое вот «“у вас с вашими компами ничего не получится” из последних сил» и выдал в виде своих теорем. Причём выдал как раз на той конференции, где обсуждалось, как именно и как скоро всё получится.
Для этих целей он взял давно известную модификацию «парадокса лжеца», которая заключалась в том, что писалось суждение «суждение в красной рамке недоказуемо» и обводилось красной рамкой.
До того момента сие считалось чисто текстовым парадоксом, но компьютеры в своей фантастической интерпретации полагались строго «счётными машинами», а потому это суждение следовало выразить «на языке чисел», чтобы всё стало «честно и научно».
Сейчас всем понятно, что компьютер может и в тексты, и в рисунки, и в музыку, но тогда таковое если кому-то и приходило в голову, то остальным казалось совсем уже запредельно фантастическим. А вот с числами и счётом - да, он может.
В результате, Гёдель придумал очень корявый по нынешним временам способ взаимно однозначного кодирования текстового выражения в число. Это сейчас почти всем почти сразу понятно, что в компьютере любой текст в файле хранится в виде цепочки чисел, которую можно трактовать как одно очень длинное, а тогда сие было неочевидно.
Кроме того, в число кодировались последовательности результатов текстовых замен, поскольку то, что последовательность чисел и даже текстовых строк в компьютере можно хранить и идентифицировать легко и непринуждённо, тоже было ещё не очевидно (а чего вы хотите во времена «машины Тьюринга» - с её помощью даже два числа сложить не так-то просто).
Кроме того, он с помощью этих кодировок придумал, как записать то, что сейчас в куче языков программирования называется «this» - ссылка изнутри объекта на сам этот объект.
Когда это перекочевало из текстовой формы в численную, для тогдашних математиков оно стало как бы «честным», «научным» и «убедительным», а потому вроде как уже могло использоваться в качестве аргумента, тогда как в текстовой форме разновидность «парадокса лжеца» вряд ли кого-то из них в чём-то бы убедила - все ж про неё давно уже знали и так.
Таким образом, есть способ трансляции суждений в числа. Есть этот ваш «алгоритм перебора». И есть некоторое суждение - «модифицированный парадокс лжеца» - на котором этот ваш алгоритм как бы сломается.
Поскольку мало кто представлял себе, что вообще такое «алгоритм в виде программы», прыжки с чисел на логические трактовки текстов, которые они кодируют, и обратно были восприняты как реальное доказательство чего-то критически важного. Например, того, что как бы есть такие числа или операции с оными, с которыми какой-то там компьютерный алгоритм как бы принципиально не справится.
И, с другой стороны, есть Гёдель, который человек, а потому как бы смог, в отличие от этих ваших железяк. Шах и мат, технократы. Компьютер никогда не обыграет человека в математику.
Хрен знает почему, но существование вот этой единственной фразы, про которую «в виде рассуждений на человеческом языке» как бы что-то можно доказать, если много раз натянуть сову на глобус, а вот компьютер «в неё не сможет», убедило кучу тогдашних математиков, что можно даже не трепыхаться: типа, если компьютер чего-то не сможет, то тогда и не надо с его помощью делать вообще что-либо из этой области. И из гипотетического девайса для доказательств он в их восприятии превратился обратно в продвинутую машинку для вычислений - как арифмометр, но только на электричестве.
Правда, к счастью, после появления реальных компьютеров изрядной части программистов было болт положить на всю эту философию, а потому уже лет через десять-пятнадцать автоматические компьютерные доказательства они стали пытаться реализовывать. К девяностым софт уже умел в плане «доказательств перебором» весьма много и в некоторых областях обгонял в этом любого отдельно взятого человека, а сейчас, в 2020-м, он таки да, по заветам Гильберта уже умеет искать доказательства или опровержения для полноценных формальных систем. Причём запрограммировать сам перебор всех возможных текстовых замен, даже если бы он не был встроен в уже существующие библиотеки, на современном языке - дело нескольких часов.
Хотя, таки да, в «парадокс лжеца» компьютер всё ещё не может.
Поскольку в него, на самом деле, не могут и сами люди тоже.
Дело в том, что там проблема не столько в том, чтобы запрограммировать функцию перебора, которая «не сломается», сколько в том, чтобы закодировать само суждение, сохранив и его смысл, и смысл некого «доказательства» касательно него. Это суждение, будучи записанным в тексте, выглядит осмысленным, но на самом деле оно бессмысленно, а потому, видимо, вообще нет аксиоматики, в которой смысл у него появится. Да и аксиоматик, в которой это суждение вообще будет вычислимым, тоже не особо много.
Однако если сосредоточиться на очень нетривиальном переводе его текстовой версии в числа и обратно, то действительно можно не заметить, что где-то в глубине этих конвертаций смысл из выражения исчез и в «численной» его версии тоже.
Но это уже дополнительные детали. Более интересно в этой истории то, что тут мы имеем дело с «богом белых пятен». То, что изначально предназначалось для «фиг вам, технократы», в какой-то момент стало в этой области вообще совсем неприменимо. Поскольку по понятным причинам для работающих с реальными компьютерами давнишние фантазии о будущих гипотетических интересны исключительно как история отрасли или художественные произведения, но не как адекватное современности руководство к действию.
Однако быть удобными для обоснования утешающего тезиса «всегда будет хлеб для живого математика» оно не перестало - просто переместилось туда, где практика ещё не сделала эту философию очевидно бессмысленной. Поэтому с «мы тут говорим о счётных машинах» оно откочевало к общематематической философии и как бы уже там стало гарантировать, что «в математике всегда будет нужна фантазия» и т.п.
Но удобство, разумеется, на этом не закончилось, а потому к «живым математикам» в борьбе за свой хлеб методом теоремы Гёделя присоединились ещё и мистики с шарлатанами, которые на базе того же самого начали утверждать, что «математикой и этой вашей наукой нельзя познать мир во всей его сложности, поэтому покупайте нашу эзотерику - у вас просто нет другого выхода».
Заметьте, это всё на базе одного и того же утверждения, «доказанного» одним и тем же способом: расплывчатые обобщающие формулировки действительно могут творить чудеса: от «нате вам, технократы» к «а вот хрен всей этой вашей науке» за неполный век - неплохой результат, да?
Что касается меня, то я-то родился не в начале двадцатого века, а считать не любил вообще никогда. Поэтому умом я могу понять переживания по поводу того, что у математиков сначала отбирают счёт в столбик, потом численное моделирование, потом аналитическое решение уравнений, потом взятие интегралов, а потом и доказательства, но никаких эмоций по этому поводу ощутить уже не могу.
Ну, кроме положительных.
Да, возможно, для кого-то «заниматься математикой» и «считать в столбик» неразрывно связано, из-за чего появление компьютеров им кажется чем-то сродни появлению автомобилей с точки зрения извозчика.
Для более продвинутых отдать сложение и умножение компьютеру - Ок, но вот поиск формальных доказательств - уже страшно. Типа как для таксиста появление робота-водителя.
И вот всем им надо утешать себя рассуждениями в стиле «компьютеры никогда не смогут», плавно трансформирующихся, аки «бог белых пятен», в «мир сложен и непознаваем этими вашими железяками и науками».
Но вот мне утешать себя что-то как-то не надо.
С моей точки зрения, если компьютер будет делать вообще всё техническое, включая поиск доказательств и даже поиск всех истинных для некоторой аксиоматики суждений, то это зашибись, поскольку самая интересная часть занятий математикой - ставить вопросы о чём-то, что есть или может быть в мире. Формулировка задачи и разработка языка, на котором её можно описать, - вот самая офигенная штука. И этой штукой компьютеры смогут полноценно заниматься весьма нескоро, поэтому все переживающие о вытеснении могут спасть спокойно - по крайней мере, ещё полвека.
А вот считать и искать перебором - да пожалуйста, пусть это делает компьютер. Я буду только рад, поскольку и сейчас стараюсь спихнуть на компьютер вообще всё, что только можно.
Но вот «счетоводам» и прочим любителям тёплой аналоговой бумажки наверно стрёмно.
Впрочем, так уже не первый раз: наверняка в то время, когда сначала вручную, а потом машинным путём создавались, например, таблицы логарифмов, одни этому радовались, а у других от этого бомбило - ведь теперь к ним реже будут обращаться с заказами на механические расчёты. Их клёвый навык обесценивается на глазах. Их статус тает. Обидно.
В общем, будьте уверены, если хоть где-то разговор перешёл с инженерных вопросов на философские, то там совершенно точно есть целая куча чьих-то обидок и страхов. Причём если в этом хоть как-то фигурируют компьютеры - пусть даже гипотетические: сто процентов, что всё это там есть.
doc-файл