Воеводский был инициатором переписки. Мои два письма стали ответами на его два письма, соответственно. Его письма были покороче и публиковать их здесь не стоит, как мне кажется.
я для себя составил такое "оправдание" (не знаю, насколько сильно оно резонирует с авторской мотивацией) проводимой Воеводским работы: пока концептуальных доказательств некоторых фактов нет, нужен способ усовершеноствавать запись формальных доказательств так, чтобы не допускать "глупых", чисто технических ошибок, подобно тому, как в языках программирования совершаются всевозможные проверки, не гарантирующие, что программа будет работать как ожидается, но уберегающие от распространённых промашек.
в текущей математике есть некоторое колическтво резальтатов, в которые все верят, но очень мало кто может/хочет понять их доказательство. яркие примеры: разрешение особенностей, теорема Калаби-Яу. наверняка в коммутативной алгебре и анализе специалисты назывут ещё немало менее известных технически трудных результатов, которые многим нужны для повседневной работы.
то есть да, конечно, стремиться к тому, чтобы доказательства были правильными не потому, что мы проверили все детали и не нашли ошибок, а потому, что на подходящем концептуальном уровне доказательство становится естественным и упрощается, надо. тем не менее, если в текущем сложном неконцептуальном доказательстве (а упрощение доказательства Хиронаки заняло десятки лет) некий автоматический проверяльщик не позволит забыть случай при сложном переборе, это с одной стороны кому-то удобно, с другой стороны --- ещё один заслон от жуликов.
Мне вспоминается, что у самого Воеводского был очень удачный термин "proof assistant". У математика есть компьютер, а в компьютере есть программа-ассистент, которая помогает математику искать дыры в его доказательствах. Невозможно оспорить право математика иметь программу на своем компьютере и пользоваться ею по своему усмотрению.
Проблема возникает в тот момент, когда математики перестают разговаривать друг с другом (хотя бы и в письменной форме, как это обычно делается) -- то есть, пользуясь другой цитатой из Воеводского (по памяти), убеждать других математиков в правильности своих доказательств -- а, вместо этого, предпочитают с компьютерами своими разговаривать, компьютер убеждать и коллегам протокол своего разговора с компьютером вместо мыслей и рассуждений предъявлять. Но, собственно, и это тоже мы не можем никому запретить.
Каковы бы ни были субъективные намерения Воеводского -- и на этот счет, как я погляжу, есть, скажем так, разные сведения или мнения -- я вовсе не склонен думать, что его деятельность сама по себе несет угрозу существованию математики или что-либо в этом роде. Просто те люди, которые реально предпочтут в своих математических занятиях общение с железной машинкой общению, высокопарно говоря, с Богом и людьми -- их и конец постигнет соответствующий. Этих людей, а вовсе не обязательно математику в целом или математическую деятельность человечества в целом.
В этом смысле я думаю, что деятельность Воеводского не нуждается в оправдании. Как не нуждается в специальном оправдании деятельность, скажем так, ненасильственных соблазнителей вообще, от ловеласов до подпольных торговцев героином и т.д. Она нуждается в обсуждении, в осмыслении возможных и ожидаемых последствий, которые будут от нее проистекать, всего спектра таковых последствий.
В чем бы кто-либо ни усматривал пользу или вред, не приходится сомневаться, что возможность купить у дилера героин можно использовать на пользу себе и людям. Так же, как можно найти полезное употребление порнографии, борделю, и т.д. Не приходится сомневаться и в том, что причинить себе или кому-то вред с помощью подобных вещей легче, чем пользу.
Мир -- опасное место, полное соблазнов и угроз. Он останется таковым, кто бы и что с ним ни делал и ни предпринимал. Я склонен верить, что сумма ненасильственной деятельности людей всегда в конечном итоге принесет больше пользы, чем вреда. Это не значит, что каждому отдельно взятому человеку будет польза от всего, что происходит. Но ему дан разум на то, чтобы позаботиться о себе.
Нарисовать катастрофический сценарий постепенного снижения стандартов понимания в математике, начинающегося с тех или иных трудных старинных теорем и прогрессирующего до полной утраты математиками всякого представления о содержании их собственной текущей деятельности, несложно. Но что за беда? В первом из моих писем к Воеводскому по ссылке не случайно упоминается "толпа, бодро марширующая прямиком в пропасть".
Потенциал такого развития существует и существовал изначально; и если так, то должен же кто-то возглавить такую толпу? Воеводскому захотелось выступить в этой роли. Почему бы и нет? Я ему, собственно, так об этом и написал, in so many words, практически. Еще раз: здесь нет ничего, что нуждалось бы в оправдании. На миру и смерть красна. Безумству храбрых поем мы песню. Их пример послужит назиданием потомкам.
В то время, как одни люди отправятся маршировать в эту пропасть, другие будут мирно писать свои статьи, выступать с лекциями и семинарами, и доказывать свои теоремы друг другу, а не железной машинке. А если их результаты логически зависят от теоремы Хиронаки или Калаби-Яу, доказательства которой они не понимают, то будут просто так и говорить: мол, это доказательство по модулю того, а это по модулю сего, которое я не проверял, но надо бы, надеюсь дорасти и когда-нибудь разобраться. Как это делалось от века.
Добавлять ли к этим словам "а ее, кстати, проверили на компьютере" или не добавлять -- вопрос вкуса. Мой совет был бы -- понимать при этом, что приближаешься к совершению акта, подобного введению иглы с сомнительного происхождения препаратом в вену или посещению борделя. Но и это вопрос вкуса тоже. Каждый математик -- взрослый человек, и может вводить и посещать все, что ему заблагорассудится.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2017-11-26 02:27 pm (UTC)no subject
Date: 2017-11-26 04:53 pm (UTC)no subject
Date: 2017-11-26 05:05 pm (UTC)no subject
Date: 2017-11-30 01:56 pm (UTC)в текущей математике есть некоторое колическтво резальтатов, в которые все верят, но очень мало кто может/хочет понять их доказательство. яркие примеры: разрешение особенностей, теорема Калаби-Яу. наверняка в коммутативной алгебре и анализе специалисты назывут ещё немало менее известных технически трудных результатов, которые многим нужны для повседневной работы.
то есть да, конечно, стремиться к тому, чтобы доказательства были правильными не потому, что мы проверили все детали и не нашли ошибок, а потому, что на подходящем концептуальном уровне доказательство становится естественным и упрощается, надо. тем не менее, если в текущем сложном неконцептуальном доказательстве (а упрощение доказательства Хиронаки заняло десятки лет) некий автоматический проверяльщик не позволит забыть случай при сложном переборе, это с одной стороны кому-то удобно, с другой стороны --- ещё один заслон от жуликов.
no subject
Date: 2017-11-30 03:38 pm (UTC)Проблема возникает в тот момент, когда математики перестают разговаривать друг с другом (хотя бы и в письменной форме, как это обычно делается) -- то есть, пользуясь другой цитатой из Воеводского (по памяти), убеждать других математиков в правильности своих доказательств -- а, вместо этого, предпочитают с компьютерами своими разговаривать, компьютер убеждать и коллегам протокол своего разговора с компьютером вместо мыслей и рассуждений предъявлять. Но, собственно, и это тоже мы не можем никому запретить.
Каковы бы ни были субъективные намерения Воеводского -- и на этот счет, как я погляжу, есть, скажем так, разные сведения или мнения -- я вовсе не склонен думать, что его деятельность сама по себе несет угрозу существованию математики или что-либо в этом роде. Просто те люди, которые реально предпочтут в своих математических занятиях общение с железной машинкой общению, высокопарно говоря, с Богом и людьми -- их и конец постигнет соответствующий. Этих людей, а вовсе не обязательно математику в целом или математическую деятельность человечества в целом.
В этом смысле я думаю, что деятельность Воеводского не нуждается в оправдании. Как не нуждается в специальном оправдании деятельность, скажем так, ненасильственных соблазнителей вообще, от ловеласов до подпольных торговцев героином и т.д. Она нуждается в обсуждении, в осмыслении возможных и ожидаемых последствий, которые будут от нее проистекать, всего спектра таковых последствий.
В чем бы кто-либо ни усматривал пользу или вред, не приходится сомневаться, что возможность купить у дилера героин можно использовать на пользу себе и людям. Так же, как можно найти полезное употребление порнографии, борделю, и т.д. Не приходится сомневаться и в том, что причинить себе или кому-то вред с помощью подобных вещей легче, чем пользу.
Мир -- опасное место, полное соблазнов и угроз. Он останется таковым, кто бы и что с ним ни делал и ни предпринимал. Я склонен верить, что сумма ненасильственной деятельности людей всегда в конечном итоге принесет больше пользы, чем вреда. Это не значит, что каждому отдельно взятому человеку будет польза от всего, что происходит. Но ему дан разум на то, чтобы позаботиться о себе.
Нарисовать катастрофический сценарий постепенного снижения стандартов понимания в математике, начинающегося с тех или иных трудных старинных теорем и прогрессирующего до полной утраты математиками всякого представления о содержании их собственной текущей деятельности, несложно. Но что за беда? В первом из моих писем к Воеводскому по ссылке не случайно упоминается "толпа, бодро марширующая прямиком в пропасть".
Потенциал такого развития существует и существовал изначально; и если так, то должен же кто-то возглавить такую толпу? Воеводскому захотелось выступить в этой роли. Почему бы и нет? Я ему, собственно, так об этом и написал, in so many words, практически. Еще раз: здесь нет ничего, что нуждалось бы в оправдании. На миру и смерть красна. Безумству храбрых поем мы песню. Их пример послужит назиданием потомкам.
В то время, как одни люди отправятся маршировать в эту пропасть, другие будут мирно писать свои статьи, выступать с лекциями и семинарами, и доказывать свои теоремы друг другу, а не железной машинке. А если их результаты логически зависят от теоремы Хиронаки или Калаби-Яу, доказательства которой они не понимают, то будут просто так и говорить: мол, это доказательство по модулю того, а это по модулю сего, которое я не проверял, но надо бы, надеюсь дорасти и когда-нибудь разобраться. Как это делалось от века.
Добавлять ли к этим словам "а ее, кстати, проверили на компьютере" или не добавлять -- вопрос вкуса. Мой совет был бы -- понимать при этом, что приближаешься к совершению акта, подобного введению иглы с сомнительного происхождения препаратом в вену или посещению борделя. Но и это вопрос вкуса тоже. Каждый математик -- взрослый человек, и может вводить и посещать все, что ему заблагорассудится.