Парадокс доказательства

http://projectwordsworth.com/the-paradox-of-the-proof/
  • Перевод
31 августа 2012 года японский математик Cинъити Мотидзуки опубликовал в интернете четыре статьи.

Заголовки были непостижимы. Объём был пугающим: 512 страниц в сумме. Посыл был дерзким: он заявил, что доказал abc-гипотезу, знаменитую, соблазнительно лёгкую числовую теорию, которая десятилетиями заводила математиков в тупик.

Затем Мотидзуки просто ушёл. Он не отправил свою работу в Annals of Mathematics. Он не оставил сообщение ни на одном сетевом форуме, которые часто посещают математики со всего мира. Он просто опубликовал статьи и ждал.

Два дня спустя, Джордан Элленберг, профессор математики в Висконсинского университета в Мадисоне, получил почтовое оповещение от Google Scholar, сервиса, который сканирует интернет в поисках статей по указанным темам. Второго сентября Google Scholar отправил ему статьи Мотидзуки: «Это может заинтересовать вас».

«А я такой: „Да, Гугл, мне это как бы интересно!“» – вспоминает Элленберг, – «Я запостил их в Фэйсбуке и в моём блоге, с пометкой: „Между прочим, похоже, что Мотидзуки доказал abc-гипотезу“».

Интернет взорвался. В течение дней даже далёкие от математики СМИ подхватили историю. «Решена сложнейшая в мире математическая теория», – объявила Telegraph. «Возможный прорыв в abc-гипотезе», – немного скромнее писала New York Times.

На математическом форуме MathOverflow математики со всего мира стали оспаривать и обсуждать заявление Мотидзуки. Вопрос, который быстро стал самым популярным на форуме был прост: «Кто-нибудь может объяснить философию его работы и прокомментировать почему она может пролить свет на abc-гипотезу?» – спросил Энди Путман, ассистент профессора в Университете Райса. Или, если перефразировать: «Я ничего не понял. Кто-нибудь понял?»

Проблема, с которой столкнулись многие математики, сбежавшиеся к сайту Мотидзуки, была в том, что доказательство было невозможно прочесть. Первая статья под заголовком «Интер-универсальная теория Тейхмюллера 1: Построение театров Ходжа», начинается с утверждения, что цель работы в «разработке арифметической версии теории Тейхмюллера для цифровых полей ограниченных эллиптической кривой… с помощью применения теории полуграфов анабелиоидов, фробениоидов, эталь тета-функций и логарифмических оболочек».

Это похоже на тарабарщину не только для обывателя. Это было тарабарщиной и для математического сообщества.

«Смотря на неё, ты чувствуешь будто читаешь статью из будущего или далёкого космоса», – написал Элленберг в своём блоге.

«Она очень, очень странная», – говорит профессор Колумбийского университета Йохан де Йонг, работающий в близких сферах математики.

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

Как профессор Мун Дучин из университета Тафтса выразила это: «Он воистину создал свой собственный мир».

Должно пройти долгое время прежде чем кто-нибудь будет способен понять работу Мотидзуки, тем более оценить верность доказательства. В последующие месяцы статьи лежали камнем на плечах математического сообщества. Горстка людей подобралась к ним и начала изучать. Другие пытались, но быстро сдались. Некоторые полностью игнорировали их, предпочитая наблюдать издалека. Что же до виновника беспокойства, человека, который заявил, что решил одну из величайших проблем математики – от него не было ни звука.



Столетиями математики стремились к одной цели: понять как работает вселенная и описать её. Для этой цели математика сама по себе лишь инструмент — это язык, который изобрели математики, чтобы помочь описать известное и исследовать неизвестное.

История математических исследований отмечена вехами в виде теорем и гипотез. Попросту говоря, теорема — это наблюдение, которое считается истинным. Теорема Пифагора, например, говорит, что для всех прямоугольных треугольников отношение между тремя сторонами a, b и c выражается формулой a2+ b2= c2. Гипотезы это предшественники теорем — они представляют собой заявку на теорему, наблюдения, которые математики считают верными, но ещё не доказанными. Если гипотеза доказана, она становится теоремой, и когда это случается, математики празднуют и добавляют новую теорему в счёт познанной вселенной.

«Суть не в том, чтобы доказать теорему», – объясняет Элленберг. – «Суть в том, чтобы понять работу вселенной и объяснить, что же, чёрт возьми, происходит».

Элленберг моет посуду пока говорит со мной по телефону, и я могу слышать голос маленького ребёнка где-то на фоне. Элленберг страстно желает объяснить математику всему миру. Он ведёт математическую колонку для журнала Slate и работает над книгой «Как не быть неправым», которая должна помочь обычным людям применять математику в повседневной жизни.

Звук посуды замирает, когда Элленберг объясняет, что мотивирует его и других математиков. Я представляю его жестикулирующим в воздухе мыльными руками: «Мы чувствуем существование огромной тёмной области незнания, но мы все вместе толкаем вперёд, делаем шаги чтобы сдвинуть границу».

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

Она начинается с простого уравнения: a + b = c.

Переменные a, b, и c, которые дают гипотезе своё название, имеют ограничения. Они должны быть целыми числами, и a и b не должны иметь общих множителей, то есть, они не должны быть делимы на одно и то же простое число. Так, например, если бы a было 64, что равняется 26, то b не может быть никаким числом, которое делится на два. В этом случае b может быть 81, что является 34. Теперь a и b не разделяют общих множителей, и мы можем получить уравнение 64 + 81 = 145.

Несложно придумать комбинации a и b, которые удовлетворяют условиям. Можно взять большие числа, такие как 3072 + 390625 = 393697 (3,072 = 210 x 3 и 390,625 = 58, никаких пересекающихся множителей нет), или очень маленькие, такие как 3 + 125 = 128 (125 = 5 x 5 x 5).

О чём abc-гипотеза затем говорит, так это о том, что свойства a и b влияют на свойства c. Чтобы понять это наблюдение, может помочь для начала переписать эти уравнения a + b = c в версии, состоящие из простых множителей.

Наше первое уравнение, 64 + 81 = 145, эквивалентно 26+ 34= 5 x 29.

Наш второй пример, 3072 + 390625 = 393697 эквивалентен 210 x 3 + 58 = 393697 (простое число!)

Наш последний пример 3 + 125 = 128 эквивалентен 3 + 53= 27.

Первые два уравнения не похожи на третье, потому что в первых двух уравнениях у нас есть много простых множителей с левой стороны уравнения и очень мало с правой стороны уравнения. В третьем примере наоборот — с правой стороны уравнения больше простых чисел (семь) чем с левой (только четыре). Оказывается, что из всех возможных комбинаций a, b и c, третья ситуация очень редка. В сущности abc-гипотеза говорит, что когда простых множителей много с левой стороны, тогда, обычно, их будет не очень много с правой стороны уравнения.

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

«Она о чём-то очень, очень базовом, о тесной связи, которая соотносит свойства сложения и умножения чисел», – говорит Минхён Ким, профессор в Оксфордском университете. – «Если существует что-то новое, что можно открыть в этом направлении, то можно быть уверенным, что это очень важно».

Эта идея не очевидна. Хотя математики и придумали сложение и умножение, основываясь на текущем понимании математики, нет никакой причины думать, что свойства сложения чисел могут каким-то образом влиять или затрагивать их свойства умножения.

«Существует очень мало свидетельств этого», – говорит Питер Сарнак, профессор Принстонского университета, скептически относящийся к abc-гипотезе. «Я поверю только тогда, когда увижу доказательство».

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

Даже скептик Сарнак признаёт это: «Если это правда, то это будет величайшим достижением».

На самом деле оно будет таким великим, что автоматически раскроет многие легендарные математические загадки. Одной из них будет Великая теорема Ферма, известная математическая проблема, которая была предложена в 1637 году и решена совсем недавно в 1993 году Эндрю Уайлсом. Доказательство Уайлса принесло ему более 100000 немецких марок призовых денег (эквивалент примерно 50000 долларов в 1997), награда, которая была предложена почти на век раньше в 1908 году. Уайлс не решил последнюю теорему Ферма с помощью abc-гипотезы, он выбрал другой путь, но если бы гипотеза была верна, тогда доказательство теоремы было бы простым следствием.

Благодаря своей простоте abc-гипотеза хорошо известна всем математикам. Профессор Городского университета Нью-Йорка Люсьен Шпиро говорит, что «каждый профессионал по крайней мере однажды пытался» теоретизировать на тему доказательства. Но мало кто серьёзно пытался найти его. Шпиро, чья одноимённая гипотеза является предшественником abc-гипотезы, предложил доказательство в 2007 году, но в нём скоро обнаружились проблемы. С тех пор никто не осмеливался взяться за его поиски, до появления Мотидзуки.



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

Мотидзуки славился своим выдающимся умом. Родился в Токио, затем переехал в Нью-Йорк со своими родителями, Киичи и Аннэ Мотидзуки, когда ему было 5 лет. Он покинул дом для учёбы в Академии Филлипса в Эксетере, в Нью Хэмпшире. Там он экстерном закончил учёбу через два года, в 16 лет, с отличными оценками по математике, физике, американской и европейской истории и латинскому языку.

Потом Мотидзуки поступил в Принстонский университет, где снова закончил обучение раньше остальных, получил степень бакалавра в математике за три года и быстро двинулся в сторону кандидатской, которую получил в 23 года. После двух лет преподавания в Гарвардском университете он вернулся в Японию, где присоединился к исследовательскому институту математических наук в Киотском университете. В 2002 году он стал профессором в необычно молодом возрасте — 33 года. Его ранние статьи были широко признаны очень хорошими работами.

Академическая удаль это не единственная характеристика, которая отличает Мотидзуки от остальных. Его друг, оксфордский профессор Минхён Ким, говорит, что самое выдающееся качество Мотидзуки это его полное сосредоточение на работе.

«Даже среди множества моих знакомых математиков, он демонстрирует невероятное терпение и умение просто сидеть и заниматься математикой долгие, долгие часы», – говорит Ким.

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

«Большинство из нас постепенно приходят к пониманию [работ Гротендика] в течении многих лет, после нескольких периодических погружений», –сказал Ким. – «Добавьте к этому тысячи и тысячи страниц».

Но не Мотидзуки.

«Мотидзуки… просто прочитал их от начала до конца сидя за своим столом», – вспоминает Ким. – «Он начал этот процесс, когда был ещё студентом последних курсов, и за пару лет он уже закончил».

Через пару лет после возвращения в Японию Мотидзуки обратил своё внимание на abc-гипотезу. В последующие годы появились слухи о его уверенности в том, что он разгадал головоломку, а сам Мотидзуки сказал, что ожидает результатов к 2012 году. Поэтому, когда статьи появились, математическое сообщество уже ждало с нетерпением. Но потом энтузиазм пропал.

«Его другие работы – они читаемы, я могу их понять и они поразительны», – говорит Де Йонг, работающий в схожей области. Прохаживаясь по своему офису в Колумбийском университете, Де Йонг качает головой, вспоминая первое впечатление от новых статей. Они были другими. Они были нечитаемы. После работы в изоляции более десяти лет, Мотидзуки построил математический язык, который только он сам может понять. Чтобы только начать разбирать четыре статьи опубликованные в августе 2012, нужно прочитать сотни, может тысячи страниц его предыдущих работ, ни одна из которых не была проверена или рецензирована. Потребовался бы по крайней мере год, чтобы прочитать и понять всё. Де Йонг уже подумывал взять отпуск и собирался потратить год на статьи Мотидзуки, но когда он увидел высоту этой горы, он спасовал.

«Я решил, что я в жизни не смогу это сделать. Это сведёт меня с ума».

Вскоре, разочарование сменилось гневом. Немногие профессоры были готовы открыто критиковать собрата-математика, но практически каждый человек, которого я интервьюировала, сразу отмечал, что Мотидзуки не следовал стандартам сообщества. Как правило, они говорят, математики обсуждают свои находки с коллегами. Обычно они публикуют препринты на уважаемых форумах. Потом они отправляют свои работы в Annals of Mathematics, где статьи реферируются видными математиками перед публикацией. Мотидзуки противился тренду. Он был, согласно его коллегам, «неправоверным».

Но самым возмутительным был отказ Мотидзуки проводить лекции. Обычно после публикации математик проводит лекции, отправляется в различные университеты объясняя свою работу и отвечая на вопросы своих коллег. Мотидзуки отверг множество предложений.

«Заметный исследовательский университет попросил его: „Приезжайте, расскажите о своих результатах“, а он ответил: „Я не смогу сделать это за одну лекцию“», – говорит Кэти ОНил, жена Де Йонга, бывший профессор математики более известный как блоггер «Mathbabe».

«И они сказали: „Хорошо, оставайтесь на неделю“, а он отвечает: „Я не смогу сделать это за неделю“».

«Тогда они предложили: „Оставайтесь на месяц. Оставайтесь столько, сколько вам нужно“, но он всё равно сказал нет».

«Парень просто не хочет этого делать».

Ким симпатизирует разочарованным коллегам, но предлагает другое объяснение обиды: «Читать чужие работы очень мучительно. И всё… Мы просто слишком ленивы, чтобы читать их».

Ким старается защитить своего друга, он говорит, что немногословность Мотидзуки вызвана его «немного стеснительным характером» и усердием в работе: «Он очень много работает и действительно просто не хочет тратить время на самолёты, гостиницы и тому подобное».

О’Нил, тем не менее, считает Мотидзуки ответственным, говорит, что его отказ сотрудничать ставит в неудобное положение его коллег: «Ты не можешь сказать, что доказал что-то пока ты не объяснил это», – говорит она. – «Доказательство это общественная конструкция. Если сообщество не понимает, ты не сделал свою рабооту».



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

Шли месяцы, и общее молчание начало подвергать сомнению основное правило математических научных кругов. Дучин объясняет его так: «Доказательства верны или не верны. Общество выносит вердикт».

Этот фундамент является предметом гордости математиков. Сообщество работает вместе, они не соревнуются. Коллеги проверяют работы друг друга, тратят многие часы проверяя, что всё верно. Они делают это не просто из альтруизма, это необходимо: в отличии от медицины, где ты знаешь, что прав, если пациент излечился, или в технике, где ракета либо взлетает либо нет. Теоретическая математика, более известная как «чистая» математика, не имеет физического или видимого стандарта. Она целиком основывается на логике. Чтобы знать, что ты прав, необходим кто-то ещё, желательно много других людей, кто прошёл бы по твоим следам и подтвердил, что каждый шаг был верен. Доказательство в вакууме не является доказательством.

Даже неверное доказательство лучше чем его отсутствие, потому что, если идеи отличаются новизной, они ещё могут быть полезны для других проблем или могут подтолкнуть другого математика к нахождению правильного ответа. Таким образом, самый главный вопрос не в правоте Мотидзуки, гораздо важнее, выполнит ли математическое сообщество свою роль и прочитает статьи?

Перспективы туманны. Шпиро является одним из немногих, кто делал попытки понять отрывки из статьи. Он проводит еженедельные семинары с учёными из Городского университета Нью-Йорка для обсуждения статьи, но он говорит, что они ограничены «местным» анализом и ещё не понимают большой картины. Единственный кандидатом остаётся Го Ямасита, коллега Мотидзуки в Киотском университете. Согласно Киму, Мотидзуки проводит частные семинары с Ямаситой, и Ким надеется, что Ямасита затем объяснит работу. Если Ямасита не справится, то неясно, кто ещё сможет осилить задачу.

Пока всё, что может делать математическое сообщество это ждать. Пока они ждут, они рассказывают истории и вспоминают великие моменты в математике — год, когда Уайлс победил Великую теорему Ферма, как Перельман доказал гипотезу Пуанкаре. Колумбийский профессор Дориан Голдфелд рассказывает историю Курта Хегнера, учителя старшей школы в Берлине, который решил классическую проблему, предложенную Гауссом: «Никто не поверил в это. Все известные математики фыркнули и отвергли его». Статья Хегнера собирала пыль больше десяти лет пока наконец, спустя четыре года после его смерти, математики поняли, что Хегнер всё это время был прав. Ким вспоминает доказательство Великой теоремы Ферма, которое предложил Йоичи Мияока в 1988 году, которое получило много внимания от СМИ пока в нем не обнаружились серьёзные недостатки. «Ему было очень неловко», – вспоминает Ким.

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

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



Что же до Мотидзуки, кто отверг все запросы СМИ, кто так сопротивляется распространению собственной работы, остаётся лишь гадать в курсе ли он той шумихи, которую поднял.

На его сайте одна из немногих фотографий Мотидзуки, доступных в интернете, показывает человека средних лет со старомодными очками в стиле 90-ых, смотрящего вверх и куда-то в сторону, над нашими головами. Самопровозглашённый титул висит над его головой. Это не «математик», а «интер-универсальный геометр».

Что это значит? Сайт не даёт подсказок. Там лишь его статьи длиной в тысячу страниц, груды плотной математики. Его резюме скромное и формальное. Он указывает своё семейное положение как «холост (не был женат)». Ещё есть страница под названием «Мысли Cинъити Мотидзуки», на которой всего лишь 17 заметок. «Я бы хотел поделиться своим прогрессом», – он пишет в феврале 2009 года. «Позвольте рассказать о моём прогрессе», октябрь 2009. «Позвольте рассказать о моём прогрессе», апрель 2010, июнь 2011, январь 2012. Затем следует математическая речь. Сложно сказать, он возбуждён, подавлен, разочарован или воодушевлён.

Мотидзуки рассказывал о своём продвижении годами, но куда он идёт? Этот «интер-универсальный геометр», этот вероятный гений, возможно нашёл то, что перевернёт известную нам теорию чисел. Он, возможно, открыл новый путь в тёмное неизведанное математики. Но пока его шаги не отследить. Куда бы он ни шёл, он похоже идёт один.

По слухам, за псевдонимом Сатоси Накамото, создателя Bitcoin, скрывается всё тот же Мотидзуки. Ссылки на статьи Мотидзуки: 1, 2, 3, 4
Поделиться публикацией
Похожие публикации
Реклама помогает поддерживать и развивать наши сервисы

Подробнее
Реклама
Комментарии 404
  • +5
    В чем парадокс?
    • +57
      Доказательство есть, но в то же время его нет.
      • +1
        Что значит «нет»? Если я правильно понял, оно есть, но его понимает только его автор.
        • +15
          В этом и суть парадокса. Доказательство вон лежит, в открытом доступе по ссылкам выше, но пока его не признают остальные математики, оно не существует.
          • –20
            Да как так не существует? Если оно лежит в открытом доступе, то оно существует. «Не признано» — согласен. Но признание не является критерием существования. По-прежнему не вижу никакого парадокса.
            • +35
              Ну проблема в том, что пока кто-то не проверит, нельзя быть уверенным что доказательство не содержит ошибки.

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

              Другое дело непонятно как отличить такие «непонятные» доказательства от бреда, который понять в принципе невозможно. Мне кажется без введения формального языка, который могла бы проверить машина, тут не обойтись.
              • 0
                Мне кажется без введения формального языка, который могла бы проверить машина
                Вы так математиков без хлеба оставите.
                • +2


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

                  Точно также если мы повсеместно начнём верифицировать программы — ведь программисты без хлеба не останутся. Потому что писать программы тоже может только человек.
                  • 0
                    Да? А мы вот тут экзамен по IBM WebSphere Business Modeler в универе сдавали, там можно построить бизнес-процесс с помощью блоков, мышкой, а дальше автоматически сгенерировать Java или C++ классы. С полным покрытием по RUP. Только тссс :)
                    • +4
                      Кхм, это был сарказм?

                      Генерация кода — это генерация кода. Это не программирование. Это перевод с одного языка (диаграмм) на другой — Java/C++. Работа программиста состоит не в этом.

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

                      Точно также может быть когда-то большая часть ПО будет разрабатываться на языках более высокого уровня, чем C++, но программисты всё равно будут нужны.
                      • –1
                        Я знаю, как происходит разработка ПО. Оба комментария были сарказмом, я люблю этот юмор, извините.

                        Насчёт верификации теорем — я думаю это неразрешимая проблема и у самих математиков уже наверняка были исследования на эту тему.
              • +7
                Доказательство станет доказательством, когда признают его правоту. Пока же это «возможное доказательство».
                • –7
                  Окей, пусть это пока «возможное доказательство». Автор опубликовал возможное доказательство. Где парадокс?
                  • +17
                    Ну ок. Тогда это «доказательство Шредингера» (по аналогии с котом): пока кто-то не докажет или не опровергнет его, неизвестно, доказательство это или нет. При желании подобную ситуацию можно назвать «парадоксом».
                    • 0
                      При желании все что угодно можно назвать парадоксом. Об этом и речь, что желание называть парадоксом очевидные вещи несколько обескураживает
                    • +11
                      это как заявить, что привидения существуют на самом деле и являются следствием влияния моноцентрических пси-барионных полей на Галардов центр височной доли мозга и привести 500 страниц расчетов и графиков. Но что такое моноцентрические барионные поля и Галардов центр, никто кроме автора утверждения не знает, а он сознаваться не хочет. Это не значит, что это его выдумка, т.к. он вполне может быть и прав, пока не доказано обратное, но и прямым доказательством это считать нельзя
                      • +21
                        Ненене, не совсем. Исправлю сравнение: автор написал, что такое моноцентрические барионные поля, но в другой книжке на 700 страниц. А что такое галардов центр он объясняет еще в одной книжке на 900 страниц. Причем в этих книжках есть понятия, которые описаны еще в каких-то книжках. И т.д. И даже самые-самые первые и основные из этих книжек способны понять человек 100 в мире, специалисты именно в данной области математики.
                        Вот на что это больше похоже.
                        Для сравнения — когда проверяли труды Уйалса ( те, которые доказали теорему Ферма ), специально наняли 7 математиков, которые около 2х лет только этим и занимались — тщательно изучали его доказательство, строчка за строчкой. И Уайлс активно помогал, они ему постоянно звонили зайдя в тупик, и он разъяснял непонятные моменты, а перед этим, конечно, обрисовал общую картину.
                        А вот японец для своей, еще более сложной работы, этого делать не хочет — надеюсь, пока.

                        • +3
                          Судя по описанию, он вполне может оказаться одним из тех гениев, которым до лампочки общественное признание. Доказал, понял сам, а остальное его не касается. Надеюсь, что это не так.
                          • +24
                            Вместо того, чтобы тратить время на объяснение, он может ещё что-нибудь глобальное доказать. Время гения слишком ценно, а жизнь коротка. Ну, а потомки за 100 лет потом разберутся, что к чему.
                            • +6
                              Без популяризации это время будет потрачено впустую. Через n-лет кто-то также решит эту проблему и его доказательство будет более понятным или же этот кто-то просто поможет остальным его понять. И уже на основе его работы будут основыватся другие. А эта останется занятным казусом, если не будет просто забыта.
                              Знания и опыт — величайшие сокровища человечества. Но если уникальное знание будет только у человека-двух — скорее всего, оно будет утеряно.
                              • +5
                                Иногда сам путь доказательства бывает не менее ценнее самой гипотезы.

                                Даже если взять этот пример, то для того, чтобы доказать abc-гипотезу были изобретены совершенно новые математические инструменты, которые сами по себе уже являются открытием и которые могут быть полезны в других областях математики. Поэтому было бы необдуманно называть объяснение решения гипотезы бесполезным решением. Хотя, автор сам решает, как поступать.
                                • 0
                                  это, простите, пока что пустое бахвальство. Он пока не гений, а человек, написавший 1000 никому непонятных страниц.

                                  Нет ничего хорошего и похвального в том, что бы отмалчиваться и стоять в стороне от сообщества.
                                  • 0
                                    Он пойдет на контакт с математической общественностью в декабре 2015 года.
                              • +1
                                Причем все эти книжки написал он сам. Если посмотреть списки литературы приведенных четырех статей Мотидзуки, то там большую половину составляют другие опубликованные в журналах работы автора, обладающие гигантским объемом, иной раз за 100 страниц.

                                Это действительно огромный труд для сообщества — верифицировать суммарно порядка 1000 страниц содержательного текста, находящегося в сложной взаимосвязанности.

                                Нельзя сказать, что вызов необорим — скажем, классификация конечных простых групп — куда более объемный результат. Однако, подозреваю, классификацию было легче разбить на составные кирпичики и проверять по отдельности; она создавалась множеством ученых в течении нескольких десятилетий.
                            • +3
                              Доказательство предоставлено и лежит в открытом доступе, но сообщество не может его понять, вследствие чего не может уверенно сказать — правильно оно или нет.
                              По-моему, Мотидзуки мыслит совершенно иными образами, недоступными для нашего понимания.
                              • 0
                                Ким симпатизирует разочарованным коллегам, но предлагает другое объяснение обиды: «Читать чужие работы очень мучительно. И всё… Мы просто слишком ленивы, чтобы читать их».

                                по моему тут гораздо ближе к истине. я помню как разбирал 10 страниц чужого кода на асме без комментариев. я ясно представляю задачу разобрать таких 1000 страниц…
                                • +3
                                  Мне кажется, многие не дочитали даже этот пост на хабре :)
                                  • 0
                                    не знаю… мне от чего-то хочется верить в лучшее, в том числе и в мыслительные способности человека и в самодисциплину. Не верю я что кроме Мотидзуки ни кто этот труд не осилит и не превзойдет.
                                    Печаль только от того, что это не я и не сейчас :)
                                    • 0
                                      Мотидзуки всю свою жизнь, возможно, собрал в этой работе. Что бы ее прочесть, возможно, нужна жизнь… Осилит и превзойдет кто-нибудь в будущем, какой-нибудь парень с нейроимплантом в затылке.
                                      • 0
                                        Не обязательно — следующий сможет передавать знания потомкам в более доступной форме, так что этот процесс понимания можно будет разбить на несколько жизней.
                                  • 0
                                    да, почти то же самое ))
                                • НЛО прилетело и опубликовало эту надпись здесь
                                  • 0
                                    По количеству минусов и плюсов у соответствующих комментариев я уже понял, что хабрасообщество устраивает такая псевдологика. Пусть будет парадокс, я уже отказался от спора (но не от своей точки зрения).
                                    • –2
                                      тебе подарили машину но колеса в коробке, угадай ?: не шреденгера машину ли тебе подарили ?!
                                      блин, ребят ну что за бред, 99% не выпендриваясь согласитесь — мы никогда не узнаем чем закончится эта история. зачем мозг рвать?
                                      плюсани засранец если ты в оставшемся проценте!
                                • +1
                                  Оно не может использоваться как инструмент для «исследования неизвестного», говоря выражением из данной статьи.
                                  Считайте, что сумрачный японский гений изобрел ракету и выложил её чертежи в открытый доступ — но никто не может разобраться в схеме и построить её (либо на её основе сделать что-то попроще). И сам изобретатель не желает в этом помочь.
                                  А пока не разобрались в особенностях схемы — нельзя сказать: а взлетит ли она?
                                  • +1
                                    О, а вот тут уже начинается серьёзная философия. Есть доказательство-статья, а есть доказательство-идея. Статья существует, но её идея ещё не признана, и пока этого не случится получается глупая ситуация: у нас есть супер-пупер важная гипотеза, доказательство которой автоматом раскрывает не только Великую теорему Ферма, но и гипотезу Шпиро, частично гипотезу Войта, не говоря уже просто о серьёзном сдвиге в понимании чисел. Но при этом все воротят нос и говорят, что оно слишком сложное и им нужна помощь.
                                    • 0
                                      Суть статьи весьма понятна. Непонятно только где парадокс.

                                      Дом построен, но не сдан госкомиссии. Дом есть, но его одновременно нет. Парадокс!
                                      • +3
                                        Кроме парадокса как логического противоречия есть парадокс в смысле парадоксальная ситуация, но было бы неуклюже делать заголовок «Парадоксальная ситуация вокруг доказательства, которое очень-очень важное, но непонятно написано, и никто его не признаёт». В вашем примере парадоксальным было бы то, что дом есть, а жить в нём нельзя.
                                        • +5
                                          видимо, я слишком требователен к употреблению слов типа «парадокс», «эпицентр» и т.п. Когда их применяют для повышения эмоциональной окраски, пренебрегая их точным значениям. Пусть будет парадокс…
                                          • +2
                                            Ну хватит. Что значит «пренебрегая точными значениями»? Слово «парадокс» имеет два значения, и оба из них с точки зрения лингвистики одинаково точные. Только одно значения из области логики, а другое из обыденной речи. И вот именно это, второе значение, вы почему-то в упор не признаёте.
                                            • +4
                                              Может быть вы дадите себе труд (небольшой) прочитать то что написано по вашей ссылке и чуть больший труд подумать. Мне сложно представить, что для такого в целом общества как здесь непроверенность доказательства является парадоксом. Еще «парадоксы»:

                                              Спроектировали машину, но еще не успели наладить производтство. Машина есть, но ее нет. Парадокс!
                                              Код написан, но не запущен, не протестирован и не проверен. Программа есть, но ее нет. Парадокс!
                                              Телевизор стоит в комнате, но выключен. Изображение есть, но его нет. Парадокс!
                                              У меня за спиной стоит холодильник. Я его не вижу. Он есть, но его нет. Парадокс!
                                              Доказательство написано, но еще не проверено. Его есть, но его нет. Парадокс!

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

                                                Вы упрекнули мне в том, что я якобы не прочитал словарную статью, на которую дал ссылку. У меня сложилось такое же мнение относительно вас.
                                                Итак, читаем статью: «Заимствование из французского, где paradoxe восходит к греческому paradoxos, состоящему из двух основ para – „против“, doxos – „слава“. Буквальное значение „против того, что принято, устоялось“. Запомнили.

                                                Доказательство написано, но еще не проверено. Его есть, но его нет. Парадокс!

                                                Да именно так. Наличие доказательства, которое написано, но которое никто не может проверить — это „против того, что принято, устоялось“, так как обычно не составляет труда проверить написанное доказательство.

                                                Вот ещё в тему статья с вики: Парадокс (значения).
                                                • 0
                                                  Удивительно! но комментарий не существует, пока я его не отправлю. Вроде бы комментарий есть, но его нет. Парадокс :) кругом одни парадоксы :)

                                                  Действительно, это очень-очень удивительно, что пока научная работа не проверена научным сообществом и им не «одобрена», то пользоваться этой работой можно на свой страх и риск. Удивительные очевидные парадоксы!

                                                  Еще раз повторю: есть два «состояния» доказательства:
                                                  1. Оно написано, но не проверено
                                                  2. Оно написано и уже проверено

                                                  Нет никакого парадокса в существовании этих двух состояний. Что такое проверка доказательства? Это принятие его как «достоверного» внутри научного (а позже — и за его пределами) сообщества. Это такой же необходимый шаг, как нажатие кнопки «Написать» под формой комментария. Если я не нажму кнопку «Написать», то этот комментарий продолжит свое существование, но не сохранится в базу данных хабра, и пропадет вместе с закрытием моего браузера. Но не надо делать из этого парадокс!

                                                  Знаете что меня удивляет больше всего? То что члены сообщества добровольно записывают себя в число недалёких людей, которыми вобще-то не являются. Парадокс существует только для тех, кто не может постичь причины возникновения этого парадокса. Вам же не кажется парадоксальным отражение в зеркале? Вы там есть, но вас там нет. Потому что вы понимаете природу того, что видите. Точно так же и с этим доказательством: оно существует, оно написано на 512 страницах. Но оно пока не может считаться признанным, и если кто-то решит использовать его выводы, то должен будет просто поверить, что оно правильное и укладывается в те аксиомы, на которые оно опиралось. Но это же, ёмаё, элементарные вещи, доступные даже первокласснику! Какой еще парадокс вы здесь узрели?
                                                  • 0
                                                    Возможно, парадокс в том, что доказательству уже скоро год, а его «все еще нет».
                                    • 0
                                      Эти файлы станут доказательством только после того, как их правильность подтвердит научное сообщество. Научное сообщество так же может сказать, что в доказательстве есть ошибка (и тогда доказательства не будет). Без такого решения это просто 500+ страниц математического текста, который может быть является доказательством.
                                • +2
                                  Почти тот же кот Шредингера, только никто не может открыть «коробку», чтобы убедиться в одном из вариантов.
                                  • +1
                                    (do-безумный-бред «Кстати да. Может быть вообще, кот Шрёдингера — это одно из проявлений такого вот поведения. То есть, кот не то, чтобы в странном состоянии находится, просто у Вселенной, ограниченной коробкой и котом не хватает производительности, чтобы вывести то, в каком состоянии он должен находится? А потом приходит наблюдатель и добавляет вычислительной мощности и хопа, решение принимается»)
                              • +34
                                Мало что понял, но ясно, что за этим скрывается что-то потрясающее. Пролистав статьи, осознал свою ничтожность.
                                • +41
                                  Завидую Вам, я осознал свою ничтожность просто прочитав эту статью.
                                • +102
                                  Отличный перевод. Получил настоящее наслаждение от прочтения.
                                  • +13
                                    Присоединяюсь.
                                    Есть что-то фантастическое в манере перевода — будто читаешь художественную литературу на тему технологий.
                                    • +1
                                      При прочтении вспоминается советская короткометражка про доказательство теоремы ферма.
                                      • +3
                                        Особенно когда завязка кончается как "… от него не было ни звука." И просто нельзя удержаться, чтобы не кликнуть «Читать дальше», чтобы узнать, что же было дальше.
                                      • +2
                                        Согласен. Местами шероховато, но, всё равно, перевод на редкость хороший.
                                        • 0
                                          Наоборот, очень дословный, местами как машинный.
                                        • +12
                                          Вот ещё хорошая короткометражка по теме: «Математик и черт»
                                          • 0
                                            Кстати, снята по рассказу Артура Порджеса «Саймон Флегг и Дьявол».
                                          • +22
                                            Может Ферма тоже имел ввиду 4 статьи на 512 страниц, говоря «Я нашел этому поистине чудесное доказательство, но поля книги слишком узки для него.»?
                                            • +2
                                              Ферма жил давно, у него не было очень многих математических знаний, которые есть сейчас у почти каждого студента-математика. Так что не думаю, что у него было что-то подобное.
                                              • +1
                                                По-моему, классическая версия заключается в том, что у Ферма было короткое, красивое, элегантное — и неправильное доказательство.
                                              • +11
                                                Читал когда-то, что Ферма имел в виду другую теорему. В его времена не было устоявшейся системы записи формул. И Ферма, как подтверждают другие его заметки, менял местами основание и показатель степени, по сравнению с привычными нам.
                                                Теорема с перевернутыми основанием и показателями имеет место, и действительно легко доказывается.
                                                К сожалению, я не нашел скана оригинальной рукописи Ферма. Но все же, склонен верить в ее самозарождение :)
                                                • +1
                                                  Теорема с перевернутыми основанием и показателями (n^x+n^y=n^z неразрешимо при n>=3) слишком легко доказывается чтобы доказательство не влезло на поля :)
                                                  • +1
                                                    Доказательство было слишком коротким, чтобы его можно было разглядеть на полях…
                                                    • 0
                                                      Любопытно. Заменой переменных a=z-x, b=y-x я свёл уравнение к n^a-n^b=1, но как обосновать, что любые степени числа n>2 отстоят друг от друга не менее, чем на 1?
                                                      • 0
                                                        Хотя тут решение проще. Для чётных n в левой части — чётное число,
                                                        для нечётных n=2k+1
                                                        в левой части — тоже чётное число: (2k+1)^a-(2k+1)^b раскрывая скобки по биному Ньютона, понятно что от каждой скобки нечётной останется только 1^a-1^b

                                                        Таким образом, слева всегда чётное, справа — единица.
                                                        • 0
                                                          Пардон за некропостинг, но почему «Для чётных n в левой части — чётное число»? Ведь четность числа определяется только для целых чисел, а так как x, y, z могут быть отрицательными (по условию задачи они должны быть только целыми и ненулевыми), то в левой части уравнения будет получаться дробное число.
                                                        • +1
                                                          Eсли b=0, то n^a=2, а этого не бывает (при n>2), а если a>b>0, то левая часть делится на n, а правая — нет.
                                                • +6
                                                  А чем обусловлен выбор хаба «DIY или Сделай Сам»?
                                                  • +34
                                                    Докажи или опровергни гипотезу сам? Могу убрать)
                                                    • +14
                                                      Прочитал статьи, докажи сам?
                                                      • +6
                                                        прочитай сам доказательство! :)
                                                        • +1
                                                          Особенно хорошо звучит, если читать DIY как die :)
                                                        • +20
                                                          Когда читаю о таких случаях, всегда возникает вопрос: почему доказательства не формализуют? В компьютерном смысле слова. Чтобы доказательства писались не (не только) на естественном языке, а а на каком-то машинно-понимаемом (типа Coq). Ведь тогда по крайней мере вопрос о том «есть ли ошибка в доказательстве?» был бы снят, так как корректность доказательства могла бы понять машина. Проблема сложности доказательства, так же как проблема сложности кода, который пишут иные программисты — осталась бы, но это было бы хоть что-то. 95% доказательств можно было бы отсеять по причине их некорректности, и только корректные пришлось бы разбирать математическим сообществом.

                                                          Так почему же так не делают?
                                                          Принципиально невозможно? Думаю нет, уже доказанные вещи можно вполне заложить в верифицирующую систему как аксиомы. А ещё лучше перевести их доказательства на формальный язык.
                                                          Долго? Так ведь математик, как и программист, больше времени тратит на размышление, и рассмотрение ложных вариантов чем на написание финального доказательства. Поэтому имея уже готовое доказательство, формализовать его не составило бы труда.
                                                          Может быть по настоящему крутые математики слишком узко специализированы и неспособны пользоваться компьютером? Сомневаюсь.
                                                          • +10
                                                            Вы, видимо, не математик. Вы когда-нибудь читали сложные математические доказательства, хотя бы за второй курс математического факультета какого-нибудь нормального ВУЗа? Усилий на то, что Вы предложили, уйдет столько, что это просто не рентабельно.
                                                            • +5
                                                              Ну ВМК окончил, но математиком себя не считаю, скорее программистом.

                                                              Доказательства читал, и даже пытался понимать, и сам что-то доказывал. В итоге остался очень неудовлетворён каким-то «интуитивным» пониманием доказательств. Когда читаешь доказательство и теряешь способность проверить, верен ли переход, так как доказательство корректности перехода автору видится очевидным. А когда сам доказываешь — делаешь какой-то переход, а потом, внезапно, оказывается что он некорректен. Мне кажется с формальным языком такого бы не было.

                                                              С формальным языком Coq проходил туториал около месяца, доказывал простейшие теоремки (типа четности суммы двух нечетных чисел), но потом началась сессия и эту деятельность пришлось свернуть. Но всё-таки в чем проблема? Ведь как и в программировании можно какие-то частые переходы свернуть в заранее написанные процедуры и их применять. Декомпозиция же, повторное использование, разделяй и властвуй, разве в математике такое невозможно?
                                                              • +2
                                                                Слишком много нужно сделать, чтобы реализовать требуемую программу. Проще научить медведя шнурки завязывать. К тому же, в некоторой аксиоматике может существовать утверждение, которое нельзя ни доказать, ни опровергнуть. Так что программа все равно будет несовершенна.
                                                                • +6
                                                                  Я так и не смог осознать упомянутую ниже теорему Гёделя о неполноте, но может вы, как человек причастный к математике, разъясните на пальцах?

                                                                  Утверждается что если формальная арифметика непротиворечива, то в ней существует невыводимая и неопровержимая формула.

                                                                  Во-первых даже если она существует, то существует ли она среди практически полезных формул? Это ведь то же самое что говорить о бесполезности верификации программ, ссылаясь на неразрешимость проблемы останова, в то время как все практически полезные программы останавливаются.

                                                                  Во-вторых если это действительно проблема, то как она решается в текущем подходе математики? Пишутся доказательства на неформальном языке? Но тогда каков критерий верности доказательства? Я могу посмотреть на него — и сказать «доказательство верно», другой посмотрит — и скажет «доказательство неверно», какой-то вопрос веры а не науки получается уже.
                                                                  • 0
                                                                    Тут все довольно сложно. Да, просто существуют в различных аксиоматиках недоказуемые и неопровергаемые утверждения. В большинстве случаев это не несет в себе каких-то проблем, ибо доказательства многих вещей строятся на уже проверенных математических аппаратах. Однако, имея эту теорему, уже нельзя утверждать что какую-то конкретную проблему можно точно решить. Повторюсь, это проявляется если глубоко копать. Например, математическая логика очень важна в понимании и создании искусственного интеллекта.
                                                                    Как бороться? Никак. Теорема-то доказана.
                                                                    Если непонятно. Найденное недоказуемое утверждение не будет выглядеть верным для одного человека и неверным для другого. Оно просто недоказуемо. Для всех.
                                                                    • +3
                                                                      Ну в таком случае — если математика не имеет путей обхода теоремы о неполноте — то эта теорема совершенно ортогональна моему предложению формальной верификации. Потому что в этом плане формальная верификация новой проблемы не вносит, как были недоказуемые неопровергаемые теоремы, так и останутся.
                                                                      • 0
                                                                        «Существует общее заблуждение, согласно которому теорема Гёделя якобы утверждает существование „недоказуемых математических утверждений“ и областей „платонического мира“ математических истин, принципиально не доступных для нас. Это очень далеко от вывода, который мы должны сделать из теоремы Гёделя. В действительности Гёдель утверждает, что какие бы правила доказательства мы ни сформулировали заранее, предполодив их заслуживающими доверия (т.е. не способными привести нас к ложному заключению) и не слишком ограничетельными, мы в результате получим новый способ доступа к некоторым математическим истинам, которые невозможно вывести в рамках данных правил».
                                                                        Пенроуз Р. Путь к реальности, или законы, управляющие Вселенной. Полный путеводитель (2007)

                                                                        Насколько понятно из слов Пенроуза (далее по тексту книги), основная формулировка теоремы Гёделя сводится к следующему: существуют так называемые «истинные П1-высказывания», которые нельзя получить из правил некоторой формальной системы F (при этом система F предполагается заслуживающей доверия). Примерами таких высказываний может служить «последняя теорема Ферма» или бинарная проблема Гольдбаха (тернарная гипотеза Гольдбаха была доказана в этом году, в мае опубликовано доказательство), согласно которой любое чётное число большее 2, можно представить в виде суммы двух простых чисел.
                                                                        • +1
                                                                          Простите, лолшто?

                                                                          Во-первых, ВТФ уже много лет как доказана. Во-вторых, то, что проблема Гольдбаха не решена, не делает её нерешаемой.
                                                                          • 0
                                                                            Где я сказал, что теорема Ферма не доказана? Где я сказал, что бинарная проблема Гольдбаха нерешаема?
                                                                            • 0
                                                                              А что вы здесь сказали, если не это?
                                                                              существуют так называемые «истинные П1-высказывания», которые нельзя получить из правил некоторой формальной системы F (при этом система F предполагается заслуживающей доверия). Примерами таких высказываний может служить «последняя теорема Ферма» или бинарная проблема Гольдбаха.
                                                                              • 0
                                                                                Ну, во-первых, это слова Р. Пенроуза (совсем немного изменений, но суть 100% сохранена во всех смыслах). Во-вторых, то, что П1-высказывания нельзя получить из правил формальной системы F, заслуживающей доверия, не означает, что их нельзя доказать, но, мне кажется, это означает, что их не получится описать и доказать только на основе формального подхода (хотя здесь я могу быть не прав).
                                                                                • +1
                                                                                  суть 100% сохранена во всех смыслах

                                                                                  Верится с большим трудом. Точнее, не верится вообще. Предположу, что Пенроуз писал, что ВТФ и проблема Гольдбаха могут оказаться недоказуемы.
                                                                                  • +1
                                                                                    Что значит «верится» или «не верится». Я же источник указал.
                                                                                    Во-первых, книга написана в 2007 г., а, следовательно, Пенроуз знал о том, что ВТФ доказана (собственно, он это и подтвердил).
                                                                                    Во-вторых, вот эта вырезка

                                                                                    Пенроуз Р. Путь к реальности, или законы, управляющие Вселенной. Полный путеводитель (2007)
                                                                                    • 0
                                                                                      Не очень понятно, что он называет «истинными П1 высказываниями». Если, допустим, бинарная гипотеза Гольдбаха недоказуема, то она не является ни истинной, ни ложной. Она недоказуема — и только (хотя доказать её недоказуемость мы тоже не сможем).
                                                                                      Как из этого утверждения получить «новый способ доступа к некоторым математическим истинам», непонятно вообще. Либо ввести новые аксиомы (что математики делают регулярно), либо предложить «новую логику», но тогда у нас будет совсем другая математика :) Что, конечно, очень интересно само по себе.
                                                                                      • 0
                                                                                        Как я и предполагал, вы всё переврали. ВТФ приводится как пример П1-высказывания, но не как пример истинного недоказуемого П1-высказывания.
                                                                                        • 0
                                                                                          Итак, я сказал
                                                                                          Насколько понятно из слов Пенроуза (далее по тексту книги), основная формулировка теоремы Гёделя сводится к следующему: существуют так называемые «истинные П1-высказывания», которые нельзя получить из правил некоторой формальной системы F (при этом система F предполагается заслуживающей доверия). Примерами таких высказываний может служить «последняя теорема Ферма» или бинарная проблема Гольдбаха (тернарная гипотеза Гольдбаха была доказана в этом году, в мае опубликовано доказательство), согласно которой любое чётное число большее 2, можно представить в виде суммы двух простых чисел.
                                                                                          Вы высказали предположения, что я утерял суть высказывание Пенроуза, которое я позднее привел в виде отрывка. Теперь вы явно утверждаете, что я утерял суть, пересказывая содержание данного отрывка. А теперь процитируйте, пожалуйста, фразу, в которой эта суть утеряна и не соответствует содержанию приведённого отрывка. Давайте разберёмся, кто здесь верблюд.
                                                                                          • +9
                                                                                            Верблюд вы, и я это докажу. Следите за руками. Ваша цитата:
                                                                                            существуют так называемые «истинные П1-высказывания», которые нельзя получить из правил некоторой формальной системы F (при этом система F предполагается заслуживающей доверия). Примерами таких высказываний может служить «последняя теорема Ферма» или бинарная проблема Гольдбаха

                                                                                            Из неё следует, что ВТФ является примером истинного П1-высказывания, которое нельзя получить из правил системы F.

                                                                                            Цитата Пенроуза:
                                                                                            Другим ещё более известным примером может служить «последняя теорема Ферма», доказанная в конце ХХ века Эндрю Уайлзом. Ещё одной (пока не решённой) проблемой является известная «гипотеза Гольдбаха», согласно которой любое чётное число, большее 2, можно представить в виде суммы двух простых чисел. Утверждения такого рода специалисты по математической логике называют П1-высказываниями.

                                                                                            Из неё следует только то, что ВТФ является примером П1-высказывания, но Пенроуз не утверждает, что её нельзя вывести из F.
                                                                                            • +14
                                                                                              Согласен, я верблюд.
                                                                                    • 0
                                                                                      Тут одно из двух. Либо Пенроуз говорит, что тезис Чёрча-Тьюринга неверен, т.е. множество задач, которые могут быть решены человеком, шире, чем множество алгоритмически разрешимых задач, либо что-то очень странное:
                                                                                      какие бы правила доказательства мы ни сформулировали заранее, предположив их заслуживающими доверия (т.е. не способными привести нас к ложному заключению) и не слишком ограничительными, мы в результате получим новый способ доступа к некоторым математическим истинам, которые невозможно вывести в рамках данных правил

                                                                                      Потому что «математические истины» в рамках какой-нибудь теории — это как раз то, что можно получить с помощью заданных правил доказательств (математической логики) из набора аксиом этой теории. Можно вводить новые аксиомы (и получится другая теория), но добавлять новые правила вывода (если они не следуют из известных) математика не позволяет.
                                                                                      • +1
                                                                                        Ну. Вообще, Пенроуз активно не верит в то, что искусственный интеллект можно создать и объясняет это тем, что человек может решать алгоритмически неразрешимые задачи. У него даже две книги об этом есть.

                                                                                        Но в данном случае он говорит именно о том, что разные системы аксиом позволяют получать разные утверждения об одних и тех же объектах. Он потом там о геометриях различных рассуждает.
                                                                                        • 0
                                                                                          Да, есть такое, поэтому, возможно, есть вероятность некоторого искажения сути под влиянием его взглядов на проблему создания сильного ИИ. Но Пенроуз дядька умный всё же, наверное, таких глупых ошибок не сделал бы.
                                                                        • +36
                                                                          Для понимания теоремы Гёделя очень советую прочесть книгу Д. Хофштадтера «Гёдель, Эшер, Бах — эта бесконечная гирлянда», там идея «странной петли», которая используется в доказательстве, пояснена на множестве простых примеров. Очень грубо и упрощенно теорему Гёделя о неполноте можно интерпретировать так: любой язык, достаточно мощный для того, чтобы быть собственным метаязыком (формальная арифметика — это язык именно такой мощности) либо не полон (содержит недоказуемые, т.е. не выводимые за конечное число шагов с помощью конечного числа правил вывода из конечного числа аксиом, истинные утверждения) либо противоречив (содержит доказательство как какой-либо гипотезы А, так и её отрицания not A).
                                                                          Проблема именно в том, что язык становится для самого себя метаязыком, и на нем можно сформулировать автореферентную (ссылающуюся на саму себя) строчку вида G = «G — не теорема». Именно такая строчка и будет гёделевой для указанного языка. Парадоксальность утверждения «Это утверждение ложно» заметили еще древние греки, но его наличие не машает нам пользоваться естественным языком. Также и теорема Гёделя не сильно мешает использованию формальных систем.
                                                                          • +8
                                                                            Прекрасно, снимаю шляпу. Я хоть и знал что это, но так доступно и хорошо описать бы не смог.
                                                                            • 0
                                                                              а на мой взгляд, это очередной сепулькарий на заданную тему…
                                                                              • +3
                                                                                Можно пояснить лучше, если аналогия непонятна.

                                                                                Пусть имеется формальная система Т, в которой можно выразить все утверждения формальной арифметики.
                                                                                Если занумеровать каждую аксиому и каждое правило вывода, то сам процесс вывода какой либо теоремы (т.е. последовательного применения правил вывода к аксиомам и уже выведенным теоремам) можно рассматривать как манипуляцию с числами, т.е. сам вывод можно описать в терминах формальной арифметики.
                                                                                Вот здесь и начинается проблема, т.к. можно построить автореферентное высказывание вида G = «G не выводима в формальной системе Т».
                                                                                Если это высказывание выводимо, то его вывод является выводом не только G, но и высказывания not G = «G выводима в формальной системе Т», что делает формальную систему Т противоречивой. Если же вывод утверждения G не существует, то G — невыводимое в системе Т истинное утверждение (истинно оно потому, что оно утверждает свою невыводимость, и это действительно так), поэтому система Т — не полная.
                                                                                На самом деле, теорему Гёделя можно доказывать не только построением «парадокса лжеца» в формальной системе, как это было сделано самим Гёделем, но и любым другим парадоксом, основанным на автореференции, например, парадоксом Берри.
                                                                                Более того, существуют доказательства, не использующие автореференцию вообще, и основанные, к примеру, на теории вычислимости, но на пальцах я их пояснить уже не смогу.
                                                                                • 0
                                                                                  Лучше не стало.
                                                                                  Вы по-прежнему в объяснениях используете понятия, требующие пояснений, при закапывании в которые велик шанс прийти к началу объяснений или уйти в бесконечность. И пропускаете шаги, по принципу "Отсюда, очевидно, следует"… И ещё и ошибки при этом совершаете… (в частности, с чего вдруг утверждение про выводимость утверждения G отнесено к утверждениям в формальной арифметики?)

                                                                                  Мне больше вариант Клайна подходит. Он же в той книге, кстати, тоже пытался описать способ появления и доказательства теоремы Геделя через сведение утверждений к числам, но тоже пропустил как минимум пару важных для понимания шагов…
                                                                                  • 0
                                                                                    Выводимость можно описать как отношение формальной арифметики, и если формальная система Т может выражать отношения формальной арифметики, то она может выражать и выводимость. Да, отношение «высказывание S выводимо в T» посложнее, чем a+b=c, но принципиальной разницы между ними нет.
                                                                                    Прошу вас, прочтите Хофштадтера, там он вводит формальную систему (названную им Топографческой Теорией Чисел), в которой все манипуляции в ходе доказательства теоремы Гёделя можно отследить, просто считая палочки на бумаге.
                                                                                    Очень трудно описать гёделизацию простыми словами, но в английской вики у сообщества почти получилось.
                                                                                    Если доказательства на словах вас не устраивают, можете отследить работу системы доказательства теорем Nqthm, которую использовал Шанкар для доказательства теоремы Гёделя еще в 1986 году.
                                                                                    • 0
                                                                                      Я бы предложил глянуть на Godel’s Incompleteness Theorem in Coq
                                                                              • НЛО прилетело и опубликовало эту надпись здесь
                                                                              • +1
                                                                                существует ли она среди практически полезных формул?


                                                                                Возможно, что среди тех утверждений (формул), которые недоказуемы по Геделю, сейчас нет «полезных», т.е. применимых в физике и пр. Но также возможно, что польза в будущем будет найдена, как нашлась польза от неевклидивой геометрии.

                                                                                Вот, например, пишут про «Континуум-гипотезу»:

                                                                                В 1963 г. П. Дж. Коэн из Станфордского университета, опираясь на работу Курта Гёделя и математиков из Института высших исследований, показал, что, хотя эта гипотеза не противоречит аксиомам общепринятой теории множеств, она вместе с тем и не следует из них.
                                                                                Фактически роль континуум-гипотезы в теории множеств такая же, как роль евклидовского постулата параллельности в геометрии. При допущении истинности или ложности гипотезы континуума можно построить различные версии теории множеств точно так же, как при допущении истинности или ложности аксиомы параллельности можно строить евклидову или неевклидовы геометрии.
                                                                                • 0
                                                                                  Думаю, данная цитата что-то может прояснить:

                                                                                  Морис Клайн «Математика. Утрата определенности.» Глава XIV, Куда идет математика?

                                                                                  … как показал Гёдель, в рамках наложенных Гильбертом ограничений любая достаточно мощная формальная система содержит неразрешимые утверждения, т.е. утверждения, которые, базируясь на аксиомах нельзя ни доказать, ни опровергнуть;

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

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

                                                                                  Процесс последовательного расширения исходной формальной системы можно было бы продолжать бесконечно.

                                                                                  Логицисты, формалисты и представители теоретико-множественного направления полагаются на аксиоматические основания. В первые десятилетия XX в. именно аксиоматика превозносилась как наиболее подходящий фундамент для построения математики.

                                                                                  Но теорема Гёделя утверждает, что ни одна система аксиом не охватывает всех истин, содержащихся в любой математической структуре, а теорема Левенгейма — Сколема показывает, что каждая система аксиом включает больше, чем предполагалось.

                                                                                • +2
                                                                                  Так уже куча таких программ реализована. Тут же нет задачи доказать, что высказывание на одном языке эквивалентно высказыванию на другом (точнее есть, но она не такая общая, как в верификации). Тут задача в том, чтобы машина проверила доказательство, которое человек описывает на специальном языке. Язык этот (исчисление конструкций), вроде, достаточно мощный. Машине надо лишь проверить только корректность каждого шага в доказательстве, а это достаточно просто, потому что, если она не может вывести какой-нибудь предикат, то она просто говорит пользователю: не могу проверить, дополни доказательство. Кроме того, эти proof-помощники позволяют утверждения объявлять аксиомами.

                                                                                  Кстати, японцы активно пытаются внедрять этот подход с формализацией доказательств. Я пару раз видел статьи, которые были просто программами для proof-помощника.
                                                                                  • 0
                                                                                    японцы же?
                                                                                    жаль, что японец Мотидзуки с ними не дружит настолько, чтобы сходить разок и их путём…
                                                                                  • 0
                                                                                    Мне кажется, что реализовать требуемую систему не слишком сложно. Сложно реализовать эту систему с поиском доказательства, но если математик нашел док-во, то занесение его в систему эквивалентно написанию программы на императивном языке по алгоритму. Формальная проверка каждого этапа должна быть не сложной (я не математик). Грубо говоря, есть аксиомы, они формализованы. Есть правила вывода, их тоже не слишком сложно формализовать. Есть теоремы, для каждой теоремы можно вручную указать цепочку вывода (еще раз, нам не нужен автоматический вывод). Для проверки просто придется перегнать все 1000+ страниц статей этого японца в код. Это бы не было проблемой, если бы он сразу писал код по мере получения результатов. Проблема в том, что нужна такая система, формальное доказательство работоспособности этой системы и внедрение этой системы в комьюнити.
                                                                                • –1
                                                                                  Усилий на то, что Вы предложили, уйдет столько, что это просто не рентабельно.

                                                                                  Воеводский с вами не согласен
                                                                                • 0
                                                                                  Любые доказательства строятся на допущениях (аксиомах), а аксиомы в каждой предметной области — свои. Каждая область сама себе решает, что считается истинным и не нуждающимся в доказательстве.
                                                                                  • +1
                                                                                    А вот тут тоже сложности не вижу.

                                                                                    Претендент на доказательство вводит «общепризнанные в данной области» аксиомы, а также утверждение теоремы в верифицирующую систему.
                                                                                    Далее система верифицирует тело доказательства.

                                                                                    Сообществу остается лишь проверить что «общепризнанные аксиомы» действительно общепризнаны, а также что утверждение теоремы им интересно. Тело же доказательства (которое внутри может содержать какие-то вспомогательные теоремы с их доказательствами) читать чтобы оценить его правильность — не надо.
                                                                                    • –3
                                                                                      Тогда как вам такой аргумент. Современные компьютеры не всегда хорошо работают с банальными дробями, не говоря уже о более сложных конструкциях. Для такой системы понадобился бы суперкомпьютер, который потом ещё непонятно как пришлось бы отлаживать. Существуют специализированные железки, которые работают с рациональными числами, но не на таком масштабе. Так что да, это наверняка возможно при достаточном понимании математики и развитии информатики, железа и ПО, но сложно.
                                                                                      • +4
                                                                                        Ещё раз напомню, что я не предлагаю компьютеру придумывать доказательство — это практически невозможно.
                                                                                        Я предлагаю ему лишь проверять доказательство — это мне кажется возможным и вычислительно не сложным. При условии что доказательство состоит из серии шагов, где каждое последующее утверждение практически очевидным образом следует из предыдущих. Для этого компьютеру даже не обязательно рассматривать всё доказательство целиком, достаточно рассматривать каждый логический переход по отдельности, всё очень локализовано.

                                                                                        Если математик при рассмотрении доказательства на бумаге не «работает» с рациональными числами, в том плане что не перемножает их численно и не складывает — то и компьютеру при проверке доказательства — не придется. Проверка же заключается в подстановке в теорему каких-то конкретных значений и проверке истинности доказательства для них, а в проверке правомерности общих логических переходов.
                                                                                        • +2
                                                                                          Боюсь что количество абстракций в математике настолько велико, что для того чтобы их формализовать и описать на машинно понятном языке потребуются настолько огромные затраты времени, труда, ресурсов, и в конечном итоге не факт что объема доступных на данный момент вычислительных мощностей хватит для того чтобы справится со всем этим массивом данных.
                                                                                          Как пример возьмите доказательство простейшей теоремы Пифагора, и задумайтесь о создание системы верификации ее доказательства, боюсь что количество сущностей с которым вам придется оперировать зашкалит за сотню.
                                                                                          • +2
                                                                                            Вообще-то многие доказательства формализованы. perso.ens-lyon.fr/jeanmarie.madiot/coq100/ теоремы Пифагора тоже. А что до количества абстракций в математике… Это тоже проблема. Многие абстракции по сути описывают одно и то же.
                                                                                            • 0
                                                                                              Насколько я понял, это формализация теорем, а не их доказательств, и верификацию теоремы на предмет правильности лишь на основе этих строчек произвести не получится.
                                                                                              • 0
                                                                                                Там, вроде, есть доказательства в contrib/… исходников. Хотя, у меня не было времени разбираться с ними. Поэтому не знаю, закончены они или нет.
                                                                                                • 0
                                                                                                  Это формализация, которая (в силу изоморфизма Карри-Говарда) является верификацией. Проверка доказательства — задача куда как более простая, чем оного доказательства поиск.
                                                                                            • +1
                                                                                              Проверка же заключается не в подстановке в теорему каких-то конкретных значений
                                                                                              кажется, вы «не» пропустили
                                                                                              • +1
                                                                                                Да, конечно, именно так.
                                                                                            • 0
                                                                                              > Современные компьютеры не всегда хорошо работают с банальными дробями
                                                                                              В каком смысле? В чем проблема?
                                                                                              • –1
                                                                                                Ну попробуйте записать одну треть в переменную. Нельзя же просто взять и написать где-нибудь в коде: x = 1/3. Хранимое в памяти значение будет отличаться. Чтобы обойти это нужно использовать костыли, в то время как для человека такая операция вообще не представляет сложности.
                                                                                                • +1
                                                                                                  Ну, например, http://ru.wikipedia.org/wiki/Символьные_вычисления. А ещё в лиспе по умолчанию есть тип рациональных чисел, который дроби хранит как дроби, а не в десятичной записи с округлением.
                                                                                                  • +1
                                                                                                    Prelude> import Data.Ratio
                                                                                                    Prelude Data.Ratio> 1 % 3
                                                                                                    1 % 3
                                                                                                    Prelude Data.Ratio> 1 % 3 + 2 % 7
                                                                                                    13 % 21
                                                                                                    Prelude Data.Ratio>
                                                                                                    
                                                                                                    • +1
                                                                                                      Для человека операции с простыми дробями — это тоже своего рода костыль (а точнее надстройка над целочисленной арифметикой). Кстати, многие дети понимают суть простых дробей намного позже, чем овладевают умением совершать операции над ними.
                                                                                                      Кстати, очень многие вещи не хранятся «просто в переменных», например те же строки, или переменные типа «датавремя». Для работы над ними надстроены в языках программирования соответствующие перегрузки операторов, встроенные функции, методы классов и т.д. Просто мы к этому привыкли и не замечаем.
                                                                                                      Тоже самое и простыми дробями. Если нужно хранить дроби как дроби — с ними можно работать и строго математически, но для этого потребуется использовать не стандартные типы данных, а пользовательские структуры и для операций над этими структурами использовать специфические функции/методы.
                                                                                                      • 0
                                                                                                        Ну разумеется можно хранить каким нибудь хитрым образом, я не спорю. Но архитектура компьютеров изначально не предусматривала работы с дробями и прочими математическими конструкциями. Нет же такой машинной команды как вычисление корня или дифференцирование.
                                                                                                        • 0
                                                                                                          Вычисление корня — есть, но в мат. сопроцессоре. Но т.к. он давно уже является стандартным модулем процессора, можно считать, что такая машинная команда есть.
                                                                                                          А вообще, если посмотреть, чем мы на компьютерах занимаемся, то не для чего из этого машинной команды нет. Не тем мы, значит, на компьютерах занимаемся, не для того они.
                                                                                                          • 0
                                                                                                            Вычисление корня многочлена? Пока такой нет, разве что на чём-нибудь специализированном…
                                                                                                            • 0
                                                                                                              Корня многочлена — конечно нет. Я об арифметическом корне писал.
                                                                                                  • +1
                                                                                                    Называть дроби «банальными» — весьма смелый трюк.
                                                                                                    Особенно в свете того, что запись дробей очень зависит от выбранной системы счисления, и они бывают бесконечными, и могут содержать любые виды чисел, позволяющих операцию деления.

                                                                                                    Логика в этом отношении куда проще — она работает лишь с утверждениями. Булева алгебра на компьютерах реализована в полной мере.
                                                                                              • 0
                                                                                                Тоже задавался таким вопросом. Насколько я понял, вся классическая математика построена на теории множеств, а Coq — на теории типов. А это не одно и то же. Поправьте, если я не прав.
                                                                                                • +1
                                                                                                  Я тоже слабо понимаю, на да — не одно и то же. Coq был лишь для примера. Ясно что если теория множеств формально описана, то и для неё можно написать (или уже написан) верификатор.
                                                                                                  • 0
                                                                                                    Насколько я понял, вся классическая математика построена на теории множеств, а Coq — на теории типов. А это не одно и то же.
                                                                                                    Это действительно не одно и то же, поскольку теории типов изоморфны исчислениям (изоморфизм Карри-Говарда), а не теории множеств. Впрочем, что происходит в исчислении (индуктивных) конструкций под капотом в Coq, я слабо представляю, так что разъяснение знатока не повредило бы.
                                                                                                  • 0
                                                                                                    Я вообще слабо понимаю в математике, но может причина в ней: ru.wikipedia.org/wiki/Теорема_Гёделя_о_неполноте?
                                                                                                    • +4
                                                                                                      Нет, точно не в ней. Грубо говоря, эта теорема говорит о том, что не все истинные утверждения доказуемы в формальной арифметике. Но если есть доказательство, то формализовать его можно.

                                                                                                      Я и сам задавался вопросом, почему нельзя задать машинопонятный язык (вместо имеющегося «полуформального»). Похоже, что это не делается из-за возрастающей сложности, неудобства инструментов и имеющихся научных традиций. Механизмы (соответствующая логическая теория или в некоторых случаях даже прикладные программы) существуют, но, видимо, не столь удобны. К тому же для этого пришлось бы вносить огромное количество имеющейся информации в базы… Учитывая сложность подобной работы, вряд ли кто-то за нее возьмется, во всяком случае в ближайшее время.
                                                                                                      • 0
                                                                                                        Кстати, формализация похожего плана формально допустима и не только для математики (в примитивном случае можно воспользоваться хотя бы тем же исчислением/секвенциальным исчислением предикатов). Все это проваливается по вышеописанным причинам, но в теории такие штуки помогли бы решить проблему верификации, а так же устранили проблему «неоткрытого общественного знания», т.е. ситуации, когда известны утверждения «А влечет В» и «В влечет С», но неизвестно утверждение «А влечет С» (и прочие вариации на эту тему).
                                                                                                        • 0
                                                                                                          А можно поподробнее? Или хотя бы ссылки на это самое секвенциальное исчисление.
                                                                                                          • 0
                                                                                                            Без проблем, но мне кажется, что в математической логике существуют более подходящие инструменты, чем секвенциальное исчисление предикатов. Есть что-то на вики, но я не ручаюсь за качество материала.
                                                                                                            На базовом уровне это рассматривается в любых учебниках по матлогике, вот например:

                                                                                                            Ершов, Палютин — «математическая логика», изд. второе.
                                                                                                            Эдельман — «матматическая логика»
                                                                                                            • 0
                                                                                                              Но у Эдельмана не очень наглядно представлен вопрос именно секвенций… Грубо говоря, с помощью них можно работать с предикатами синтаксически, а не семантически. У нас это входило в базовый курс матлогики в университете, поэтому затрудняюсь порекомендовать что-либо другое из литературы.
                                                                                                              • 0
                                                                                                                Более подходящие — это какие?
                                                                                                                • 0
                                                                                                                  Логика высших порядков (например, логика второго порядка расширяет исчисление предикатов такими штуками, как работа кванторов с предикатами) и теория типов. Язык Coq, кстати, построен на частном случае лямбда-исчислений — на исчислении конструкций.

                                                                                                                  Но мои знания в них очень поверхностны и я понятия не имею, какой математический аппарат стоит за ними, потому не могу ничего порекомендовать из литературы.
                                                                                                                  • 0
                                                                                                                    Эх. Печалька :( Как-то у нас эта тема вообще почти никак не разбирается в математике.
                                                                                                        • 0
                                                                                                          Мне всегда не нравилось, что на эту теорему указывают, когда не понимают сути происходящего. Но в данном контексте, мне кажется, вы очень точно указали на проблему.
                                                                                                          • 0
                                                                                                            Это разные проблемы. Проблема неполноты — существование недоказуемых истинных утверждений. Она не влияет на проблему формальной проверки доказательства.
                                                                                                            • –1
                                                                                                              «недоказуемых истинных утверждений». Немного не так. Просто «недоказуемых утверждений».
                                                                                                              • 0
                                                                                                                На самом деле проблема и того шире, в данном случае я просто выражался «на пальцах» и не стал оговаривать вопрос аксиоматики.
                                                                                                        • –13
                                                                                                          Странное(но понимаемое и не разделяемое) желание алгоритмизировать процесс проверки доказательств теорем. Почему бы не пойти дальше и не алгоритмизировать проверку на «красоту» и «правильность» различных произведений искусства вроде картин, скульптур, стихотворений, музыки.
                                                                                                          Не может иметь это смысла.
                                                                                                          • +6
                                                                                                            Хотелось бы пояснений. Чем принципиально плоха возможность автоматической проверки? Почему это не может иметь смысла?

                                                                                                            В оценке произведений искусства неотделимо присутствует субъективная оценка, здесь же ее не может быть — доказательство может быть или верно, или нет. Доказательство может быть верным, для объектов искусства же подобный термин не определен. К тому же подобная проверка не исключает проверки человеком, для обучения просто необходимо разбираться в доказательствах и методах доказательств.
                                                                                                            • –6
                                                                                                              Потому что задача сводится к построению системы, которая умеет думать. При оценке нового математического доказательства, нужно понимать применимость тех или иных математических методов или приемов, используемых в доказательстве, а не формальное наличие алгоритмических ошибок.
                                                                                                              • +3
                                                                                                                Я все равно не понимаю Вас. Причем здесь алгоритмические ошибки? Все методы, которые были использованы, будут ровно таким же образом формализованы (принципиальной разницы, кроме сложности исполнения, между имеющейся на сегодня формальной записью и подобной машинопонятной записью нет). Если метод неприменим, мы просто не получим необходимого логического следствия.
                                                                                                                • –5
                                                                                                                  А кто знает какое следствие является логически необходимым? Простой пример: Есть факт A. Есть два метода(утверждения, аксиомы, приема, формулы и т.д. применимых для А): M1 и M2 (на самом деле сколь угодно). И вот автор применяя M1 к А получает следствие S1: S1 = M1(A). Аналогично S2=M2(A). Выбирая M1 и M2 можно получить взаимно противоречивые или просто разные следствия S1 и S2 при полностью формально правильном применении M1 и M2, что можно алгоритмически проверить. Но как алгоритмически проверить правильность выбора M1 или M2? Сколько методов не формализуй остается проблема правильности их выбора. Собственно это и есть самая большая проблема в оценке правильности математических доказательств.

                                                                                                                  • +5
                                                                                                                    Если у нас есть система, в которой можно из истинных утверждений формально вывести два взаимопротиворечивых утверждения, данная система называется противоречивой, и в ней можно формально доказать все что угодно. Противоречивые системы — плохие системы, нам не имеет смысла с ними работать.

                                                                                                                    Или Вы имели в виду проверку метода на корректность, т.е. проблему применимости? Здесь эта проблема выглядит несколько иначе, чем у машин Тьюринга. При введении метода необходимо изначально пояснить, на каких данных он работает, и обосновать, почему он работает, иначе данный метод применять мы не имеем права.
                                                                                                                    • –3
                                                                                                                      При оценке нового математического доказательства, нужно понимать применимость тех или иных математических методов или приемов

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

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

                                                                                                                      • +3
                                                                                                                        Любая подобная программа будет работать с уже выбранными автором методами и пытаться искать «ошибки» в уже сформированном доказательстве.

                                                                                                                        Для проверки доказательства нам ничего больше и не нужно. Вот только методы не «выбраны автором», а заранее предопределены математической логикой. И набором «общепризнанных» теорем (чтобы не пришлось доказывать всё с самых основ). Всё, что может автор — это сказать «берём такую-то теорему, подставляем вместо свободных переменных некоторые формулы — получаем новую теорему. Если её условие оказалось в списке доказанных утверждений, то и вывод можно поместить в тот же список».
                                                                                                                        В книге «Гедель, Эшер, Бах» приводится пример полностью формализованного доказательства одной из теорем. Правда, там доказывалась всего лишь коммутативность сложения. Доказательство заняло около трёх страниц.
                                                                                                                        • –4
                                                                                                                          Вот только методы не «выбраны автором», а заранее предопределены математической логикой.

                                                                                                                          Методы не могут быть заранее предопределены:) Существуют множества, в том числе и еще неизвестные, доказательств одних и тех же утверждений.

                                                                                                                          набором «общепризнанных» теорем

                                                                                                                          Все сводится к созданию этого «набора», но проблема в том, что этот набор по-определению уже будет неполон в силу искусственности своего происхождения.

                                                                                                                          приводится пример полностью формализованного доказательства одной из теорем

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