Мне кажется, что все это постепенно сползло к полному бреду. "Проверка теоремы Жордана" меня добила.

Как говорят американцы, let us change the topic. Вы с работами Харви Фридмана знакомы?

"Проверка теоремы Жордана" на компьютере – дурдом, конечно. Напоминает построение, циркулем и линейкой, правильного 65537–угольника.

Да просто это не математика. А если программистам (или еще кому-то) хочется таким образом поразвлекаться -- жалко что ли? Пусть развлекаются. Может язык новый придумают.

конечно – это (не очень убедительная) демонстрация прототипа некоторого средства, которое, может быть, когда–нибудь будет полезно математикам.
по крайней мере, когда надо referee reports писать :)
А может, и не только. Может, лет через 50 соавтор будет соавтору посылать доказательства в таком формате, чтоб компьютер мог их заодно проверить.

Описываемая таким образом перспектива мне совсем не нравится. Но я не думаю, что до такого дойдет. А так -- любые исследования могут когда-то оказаться полезными. От того, что появились электронные переводчики (полезные для каки-то определенных целей) с искусством художественного перевода ведь ничего не случилось. А вот филология всякая в процессе их разработки, наверное, сильно продвинулась.
Так что и математике такие разработки, мне кажется, никак не угрожают.
Если кто-то считает, что определенную часть его работы эффективнее сможет выполнить компьютер -- пожалуйста. Главное, чтобы остальных это делать не заставляли :-)

это вопрос разработки языка, на котором излагаются формальные аргументы.
Если большинство в какой–то момент начнет этими средствами активно пользоваться,
сама понимаешь, к чему это приведет.
Точно так же, как сейчас со всякого рода компьютерной алгеброй стало.

Гораздо любопытнее дело обстоит с автоматическим доказательством теорем...
Что компьютер сможет в не столь отдаленном будущем в каких–то специфических областях доказывать технические леммы лучше человека, не сомневаюсь (достаточно на шахматы посмотреть)

Я не верю, что большинство работающих чистых математиков начнет активно пользоваться этими средствами. Компьютерной алгеброй если кто и пользуется, то в довольно ограниченном числе областей, и потом обычно все равно полученный таким образом результат переписывается по-человечески. Не всегда -- например, при вычислении симметрий УрЧП жуткие аналитические вычисления, и народ, этим занимающийся, эти формулы вполне устраивают, там целые программы по поиску "всех симметрий" нужных уравнений. Но я так поняла, что многие эту деятельность математикой и не считают. А в приличной математике все равно и результаты приличные, излагаемые без помощи компьютера.

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

Кстати, ignat@lj сказал, что вам может будет интересно посмотреть на это.

Мне не понравилось то, что falcao@lj там говорил про "обязательную машинную проверку" доказательств. Это не сдвиг "человеческой" части, а попытка подменить человеческое понимание машинным, мне кажется. Но дискутировать на эту тему как-то нет желания. А то, что какие-то рутинные элементы передаются машине, не страшно. Но вот мне, например, больше нравятся те разделы математики, в которых этой рутинной -- доступной машине -- части просто нет. То есть я предпочту не передавать часть работы машине, а заниматься работой, в которой такой необходимости просто не возникает. Не потому, что я плохо отношусь к компьютерам или программированию. "Смешивать два этих ремесла есть тьма охотников, я не из их числа".

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

Я ничего не вижу плохого в возможности проверять те или иные сомнительные моменты в доказательствах. Ведь такие ситуации то и дело реально возникают. Раз люди не вполне справляются, то пусть им помогают машины.

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

Я боюсь, что хозяину журнала обсуждение этой темы надоело еще на ее прежнем месторасположении...

Я не вижу плохого в этом: "стало возможным написать в машинных кодах реализацию любого алгоритма, изложенного человеческим языком", но вижу в этом: "возможности проверять те или иные сомнительные моменты в доказательствах. Ведь такие ситуации то и дело реально возникают. Раз люди не вполне справляются, то пусть им помогают машины." Мне кажется, что это как раз та область, где справляться должны люди. Аналогия: можно сказать -- что-то люди плохо стали справляться с написанием стихов, давно у нас не было Пушкиных. Пусть-ка им в этом помогут машины.

То есть мне кажется, что такие ситуации, когда люди "не вполне справляются с проверкой доказательства", делятся на два типа:
1) доказательства нет, а есть только его видимость, или оно плохо изложено. Чем тут поможет машина?
2) доказательство на данном этапе не умеют проводить на уровне, доступном для понимания человеку, а только с машинными вычислениями. Эта тема много обсуждалась, вряд ли я что-то новое скажу. Машина и так уже применена, но толку-то?

Этот момент я тоже многократно разъяснял. Надо ли доказывать, что часто авторы статей ссылаются на некие "очевидности", которые совсем не очевидны? И часто это сходит с рук. Рецензент может придраться, а может поверить автору на слово. Если автор будет знать, что от него могут потребовать свидетельства "очевидности", то он предпочтёт продумать аргументацию более тщательно.

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

Потенциальная возможность машинной верификации должна просто дисциплинировать. Тут вполне работает афоризм, хорошо известный шахматистам: "угроза сильнее её исполнения".

"Если автор будет знать, что от него могут потребовать свидетельства "очевидности", то он предпочтёт продумать аргументацию более тщательно"

Ну так и пусть он знает, что могут потребовать, и если не разъяснит, то никто его уважать не станет. Надо менять порядки, чтобы так было. Но при чем тут машины?

"Потенциальная возможность машинной верификации должна просто дисциплинировать"

Мне кажется, что очень многих такая угроза (заставить сводить доказательство к стандартным макросам) просто отпугнет от математики. И очень многие результаты не будут рассказываться из-за того, что автор будет предвидеть эту тягомотину с "машинной верификацией". Тогда уж проще вообще никому свои результаты не рассказывать, ну или близким знакомым только. Вы предлагаете создать барьер перед авторами. Причем этот барьер будет выше всего для оригинальных, нестандартных идей.

Дисциплинировать надо совсем другими методами, мне кажется.

Да, а не понравились мне ваши слова (там уже все очень разрослось и нужный комментарий найти трудно, так что я по памяти) о том, что если какое-то место в доказательстве непонятно, то надо обязать автора привести его к понятному машине виду.

Я высказывал более слабое утверждение. Если есть сомнительное место, то автор должен уметь его разъяснить. Даже сейчас это так - Вы делаете доклад, Вам задают вопросы. Или могут задать вопрос по e-mail. Говоря о предполагаемом будущем, я имел в виду, что разъяснение должно быть понятно квалифицированному "программисту". Учтите, что многие вещи к тому моменту для "программиста" станут уже стандартными макросами. А от математика ничего принципиально нового не потребуется. Зато никто из скептиков не сможет потом говорить о сомнительности.

Должен разъяснить -- да, конечно. Но почему программисту? И зачем необходимо, чтобы программист это объяснение переработал в программу и поставил клеймо ОТК?

"разъяснение должно быть понятно квалифицированному "программисту". Учтите, что многие вещи к тому моменту для "программиста" станут уже стандартными макросами. Зато никто из скептиков не сможет потом говорить о сомнительности."

Вот это мне и не нравится. Сведение изложения доказательства к последовательности применения стандартных макросов. Я понимаю, что вы говорите не о полной замене нормальных изложений такими стандартными схемами, а об их дублировании (то есть человеческое изложение плюс машинная расшифровка). Но смысл этого занятия мне непонятен. А если это станет обязаловкой, или в непродублированное доказательство будет принято не верить, то это уже откровенный вред.

Я отвечу сразу по обеим записям, так как говорится об одном и том же.

Я ни с чем сказанным Вами спорить не буду по очень простой причине: я Вас в какой-то мере знаю по многим высказываниям, и потому могу быть уверенным, что любое конкретное явление, связанное с проблемой машинной верификации мы оценили бы одинаково. То есть представления о том, "что такое хорошо и что такое плохо" у нас одинаковые. Думаю, и у большинства математиков тоже.

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

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

Вчера я долго участвовал в дискуссии в состоянии "сидения на чемоданах" - вечером надо было ехать в Москву. Поэтому я писал в несколько нервном состоянии и, возможно, не учитывал чисто человеческой реакции участников дискуссии на сказанное. (В спокойной обстановке и при отсутствии спешки я мог бы позволить себе большую осмотрительность.) Ей богу, я не говорил и не имел в виду ничего, противоречащего здравому смыслу или нормальным общепринятым математическим вкусам. По-моему, я тоже давно участвую в разных дискуссиях, меня многие знают, поэтому я скромно надеялся и надеюсь на то, что меня не будут подозревать в пропаганде какой-либо ерунды. Даже если написанное мной производит такое впечатление, то надо трижды перечитать и попытаться истолковать безобидно. Я за то, чтобы коллеги доверяли друг другу, а не сражались за непонятно кому нужную "правду".

Я ничего не имею против разработок таких языков и программ. И согласна, что это может быть полезно для каких-то своих целей, например, лучше понять то, как мы рассуждаем (в каких-то простых вещах). Но нарисованная перспектива (то, как я ее поняла) предлагать математикам не очень понятные места их рассуждений сводить к виду, понятному машине (пусть даже с помощью программистов) меня приводит в ужас (я представляю себя на месте такого математика :) То есть против такой деятельности я ничего не имею, если она не будет называть себя математикой (как вы и говорили), и если ее не будут навязывать математикам для использования в каких-то ситуациях.

А так со всем сказанным вами в этом последнем комментарии я согласна.

Сейчас до меня стало доходить, что Вас и других мог смутить некий пример, который я приводил. Сейчас трудно его отыскать в недрах дискуссии. Фраза про математика, любящего задвигать фуфло в доказательствах, звучала примерно так: а сейчас садись, голубчик, за монитор и формализуй своё доказательство. Но ведь это был некий гротеск - его нельзя воспринимать 1:1. Я часто использую подобные вкрапления. Можно ещё добавить, что я говорил о "наболевшем", так как знаю много примеров циничного задвигания фуфла в своей области (и очень часто речь идёт о хороших математиках, которые заявляют, что сделали нечто). Я Вам могу приватным образом сообщить целый список таких примеров. Причём это делается в почти что комбинаторной области. А уж какой шабаш царит в других, менее комбинаторных областях, мне даже страшно вообразить.

Да я тоже фуфла видела много. Наши с вами расхождения в том, что я считаю, что формализация тут абсолютно ни при чем. И фуфло можно якобы формализовать (но поскольку при этом получится совершенно нечитаемый человеком вид, то никаких выводов сделать будет нельзя), и замечательные результаты не требуют никакой формализации для того, чтобы мы были уверены в их правильности. Это совершенно перпендикулярные вещи, мне кажется. (Не говоря уж о том, что я лично вообще больше ценю не конкретные результаты, а новые понятия и взаимосвязи, которые возникают в том числе при их доказательстве -- тут уж формализация вообще ничего не дает.)

Не то вы, не то fuia-krucha@lj в том треде писали про таблетки. Здесь, мне кажется, применима та же аналогия: формализация для проверки доказательств и избавления от фуфла -- это как лечение рака анальгином.

"Сейчас трудно его отыскать в недрах дискуссии"

Ну вот я поискала.

упоминания о сомнительных местах во многих доказательствах. В этом случае наличие хорошо разработанной системы проверки могло бы помочь. Автор (или кто-то, им для этого нанятый) доводит доказательство "до ума". Если его в итоге удаётся формализовать, то всё в порядке (http://furia-krucha.livejournal.com/13721.html?thread=75417#t75417)

Если подобной деятельностью не заниматься, то сомнения в правильности будут возникать то там, то тут. А так появляется надёжный способ верификации. (http://furia-krucha.livejournal.com/13721.html?thread=82329#t82329)

Предположим, кто-то усомнился в каком-то переходе в доказательстве ВТФ. Авторы дают разъяснения, скажем, своим аспирантам. Те начинают сотрудничать с "программистами" - теми, кто содержательные математические соображения переводят на некоторый промежуточный язык (аналог, допустим, Алгола). Потом компьютер автоматически генерирует машинный код, и дело в шляпе. (http://furia-krucha.livejournal.com/13721.html?thread=82329#t82329)

Потенциальная возможность машинной верификации должна просто дисциплинировать.

Вот это все мне ужасно не нравится!

> И фуфло можно якобы формализовать (но поскольку при
> этом получится совершенно нечитаемый человеком вид,
> то никаких выводов сделать будет нельзя)

"Это у корне невэрно", как говорил Леонид Ильич Брежнев в анекдоте. Я об этом писал; придётся напомнить ещё раз.

Допустим, получен километровый текст формального вывода предложения T. Сам вывод человеку прочитать нет возможности, но есть соответствующий файл. Проверка того, что этот файл представляет собой формальный вывод в исчислении предикатов из заданного списка аксиом, достигается при помощи очень простой и короткой программы, которую в состоянии написать каждый. Причём даже если у разработчиков системы (которую нам и не предъявляют) были "баги", то это ни на что не влияет. Я это считаю очень важным моментом.

> я лично вообще больше ценю не конкретные
> результаты, а новые понятия и взаимосвязи

Так ведь и я тоже (я мыслю идеями, а не утверждениями). Можно сюда же добавить новые приёмы доказательства и ещё много всего, что можно назвать творческим и полезным. Но формальная проверка этого никак не затрагивает и не убивает. Это действительно "перпендикулярная", дополнительная вещь. Как говорил Чичиков, желая прикупить "мёртвых душ" -- "и кресты, и могилы - всё это вам остаётся!" :)))

Про "таблетки" писал я, но это было при обсуждении ТМД. В этом вопросе, как я понимаю, Вы со мной были принципиально согласны.

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

Чем Вам не нравится тот же пример с ВТФ? Ходили недавно слухи о том, что какой-то переход там то ли сомнителен, то ли ещё что-то? Так вот пусть те, кто сомневается, делают машинную проверку. Этого Вы ведь не можете никому запретить. Уайлс занимается себе математикой, а любой желающий в любом уголке земного шара пусть себе проверяет. Это, если угодно, его личная проблема. Математику это вообще не трогает из-за совершенно верно отмеченного Вами факта "перпендикулярности".

"Про "таблетки" писал я, но это было при обсуждении ТМД. В этом вопросе, как я понимаю, Вы со мной были принципиально согласны."

Да, согласна, и с вами, и с furia-krucha@lj.

"Так вот пусть те, кто сомневается, делают машинную проверку. Этого Вы ведь не можете никому запретить."

Запретить я, разумеется, не могу. Но признавать такую проверку что-то доказывающей мне не хочется. Я не считаю это "способом верификации".
"Если его в итоге удаётся формализовать, то всё в порядке" -- вас такая проверка убедит в правильности доказательства, или вы все же захотите убедиться в этом самостоятельно? (почему-то я уверена во втором :)
Хорошо, вы говорите, что пусть проверяют те, кому это надо, и кого такая проверка в чем-то убеждает. Но ведь при этом критерии математической истины смещаются и размываются.

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

Мне тоже кажется, что на эту тему уже всё сказано. Будем считать, что какой-то "общий знаменатель" получен, хотя и с несколько разными "числителями" :)

Вы затронули вопрос о критериях математической истины. Об этом следует сказать несколько слов. Я думаю, правильнее ставить вопрос о собственных критериях веры в правильность результата, так как объективный смысл всегда один - существование доказательства.

Я могу верить в правильность результата на основании того, что сам его хорошо понимаю и могу воспроизвести. Могу верить на основании свидетельств авторитетных специалистов, как в случае с ВТФ. Но ценность такого убеждения гораздо ниже. Это как самому съесть что-то или увидеть как кто-то ест. Наконец, если мне предъявят на CD файл с формальным доказательством чего-либо и я проверю при помощи простой программы его синтаксическую правильность, то степень уверенности в истинности будет абсолютной, хотя внутренняя ценность этого лично для меня близка к нулю. Мы ведь не только стремимся получать истинные и новые утверждения, но ещё и "кушать" их. В этом смысле компьютерный продукт совершенно безвкусен, хотя и безвреден для здоровья. А иногда даже полезен - подобно каким-то микроэлементам, если их не хватает в организме.

Да-да, про безвкусность хорошо сказано.

Меня файл не убедит. В бОльшей степени даже, пожалуй, убедит практическое применение -- например, на основе этой теории разработана какая-то новая физика, и вот результат -- самолеты летают и не падают :-)

Сам по себе анализ систем вывода, наверное, имеет смысл - в частности в терминах систем вывода удаётся сфорулировать многие задачи из computational complexity, а учитывая некоторый прогресс Разборова, Вигдерсона, Раза и т.д в этом направлении они привлекли много внимания, но, конечно, "Проверка теоремы Жордана" и подобное, мягко говоря, удивляет.

Да, я подписан на FOM и пропустить мимо глаз анонсы результатов чуть ли не самого активного участника (не перестаю удивляться, как ему удаётся одновременно и _продуктивно_ вести столько бесед) было бы весьма и весьма затруднительно.
Мне изначально нравились результаты в этом направлении, его и других, но последние просто впечатляют - настолько тонок барьер между доказуемым и недоказуемым (как раз последние "манускрипты-абстракты" у него на сайте): какое-то добавление численного параметра переводит утверждение о конечных графах из доказуемого в небольших фрагментах арифметики Пеано в недоказуемое в ZFC без больших кардиналов (вплоть до Мало). Конечно, вещь гораздо менее естественная, чем известные подобные результаты, но достигнутая точность контроля удивительна. Настолько, что даже "логическая мечта" Шелаха о аналоге форсинга для теории чисел не кажется столь уж эвфемерной.

А вы не знаете, можно ли где-нибудь найти доступное изложение какого-нибудь результата этого сорта? Не обязательно самого нового.

Правильно я понимаю, что его методы - теоретико-модельные? Я не очень хорошо понимаю, что именно я этим хочу сказать. Например, теорема Кирби-Париса-Харрингтона - теоретико-модельная (особенно в исходном варианте, который не зависит от Гёделя), а теоремы Коэна - нет.

Извините за задержку с ответом, я немного приболел тут.
Работы перечисленных относятся к очень ограниченным формам выводимости, т.н. propositional proof complexity (очень близко по духу и вообще к цепям.)
``$P \ne NP$, Propositional Proof Complexity, and Resolution Lower Bounds for the Weak Pigeonhole Principle'', R.Raz,Proceeding of the International Congress of Mathematicians, ICM 2002, Vol III, pp. 685-693 (http://www.wisdom.weizmann.ac.il/~ranraz/publications/Pchina.ps)
или выводимость в слабых кусках арифметики: Кук с учениками ( у него на сайте есть и обзоры, и драфт книжки на эту тему), Бусс.

Если я правильно понял, что вы имеете в виду, то да. Т.е. также предполагается утверждение и с его помощью "вручную" строится модель.
Вот неплохой обзор "модельных" доказательств недоказуемости буквально в страницу, с ссылками на основные работы Фридмана
http://www.csc.liv.ac.uk/~andrey/forlogicians/forlogicians.html

Не прокомментируете ли http://bbixob.livejournal.com/50403.html ?
Мни казалось, что когда-то на ФОМ Фридман что0то такое упоминал
(канонические конструкции мат обхектов), может быть в связи с аксиомой выбора
но я не помню/

Честно говоря, к уже сказанному там мне содержательного добавить особо нечего.

По поводу Фридмана. Я помню два обсуждения:
1)Действительно, сколько "выбора" достаточно для единственности алгебраического замыкания рациональных
http://www.cs.nyu.edu/pipermail/fom/2006-May/thread.html#start
Но, в целом, с теоретико-модельной точки зрения, по-моему, не очень интересно.
2)Более пространное и интересное обсуждение о канонических конструкциях ( ну, т.е. более-менее без AC) в июне-июле 2003 начиная с записи Болдуина "categoricity and strongly minimal sets" и многочисленных комментариев к ней ( http://www.cs.nyu.edu/pipermail/fom/2003-June/date.html#start . К сожалению, дать ссылку точнее нет технической возможности )

Spasibo! Ja by ne smog najti eto obsuzhdenie sam..

W odnom iz postov est' est' ssylka na rezultat Covey (nim-numbers)

http://www.cs.nyu.edu/pipermail/fom/2006-May/010560.html


wtoroe eshe ne smotrel.

ох, столько описок в двух предложениях, что просто ужас.

Как заработать в Интернете Новичку. Без вложений и затрат. Все объясняется буквально на пальцах-ну ОЧЕНЬ просто. Идеально подходит для новичков. Конкретные схемы, приемы, методы, которые помогут Вам организовать такую бизнес структуру, которая будет работать автономно 24 часа в сутки, без Вашего участия, и приносить Вам стабильный доход.

"Заполучи!!! в свои руки настоящего денежного зверя, который будет ежедневно приносить нехилую денежную добычу на твой электронный счёт в различных кибер системах"

Скачайте БЕСПЛАТНО книгу по следующей ссылки:

http://kajfa.net/book1.zip

Приятного Вам чтения!

С уважением,
Владимир.