Геймдизайнер-телепат
0,1
рейтинг
17 июня 2013 в 11:06

Разработка → Парадокс доказательства перевод

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
Перевод: Caroline Chen
Даниил Басманов @BasmanovDaniil
карма
190,2
рейтинг 0,1
Геймдизайнер-телепат
Реклама помогает поддерживать и развивать наши сервисы

Подробнее
Реклама

Самое читаемое Разработка

Комментарии (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
                      Вот только методы не «выбраны автором», а заранее предопределены математической логикой.

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

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

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

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

                      Речи о том, что формализовать существующие доказательства нельзя — не было. Речь о том, что в общем случае, алгоритмизировать доказательство произвольных суждений пока что невозможно, а соответственно любая работа в этом направлении пока что лишена смысла в силу.
                      • +2
                        Как раз речь изначально была не о доказательстве произвольных суждений, а о проверке доказательства.
                        • –2
                          А в чем разница?)
                          • +2
                            Программе не нужно создавать свое доказательство. Нужно лишь проверить уже заданное формально доказательство.
                            • –4
                              А в чем ценность, если «заданное формально доказательство» неверно? Ведь выбор неверных исходных данных, гипотез, приемов, следствий при логической непротиворечивости цепочки вывода даст недостоверный результат.
                              • +2
                                В возможности автоматической проверки, является ли оно верным. Все выбранные приемы и теоремы должны быть предварительно определены, ибо это математика.
                                • –4
                                  Все выбранные приемы и теоремы должны быть предварительно определены, ибо это математика.

                                  Не могут быть в принципе — ибо это математика. Если бы все они были бы определены — все существующие утверждения были бы уже доказаны или опровергнуты.
                                  • 0
                                    Слово «выбранные» забыли. Мы выбрали набор теорем, на который ссылаемся.
                                    • –1
                                      Не важно:) Выбранные тоже вначале надо доказать или вручную или «автоматически» и мы возвращаемся к сути проблемы, а именно вмешательства человека в процесс доказывания.
                                      • +2
                                        А причем здесь это? Мы проверяем уже записанное человеком доказательство, какая проблема? Нам от машины нужна только проверка.
                              • 0
                                Неверно, значит неверно. И тогда вопрос с конкретным доказательством, приведённым этим конкретным математиком, можно закрыть. А можно попытаться всё-таки разобраться, чего он напридумывал, и как это называется в общепринятом языке.
                      • 0
                        Речь о том, что в общем случае, алгоритмизировать доказательство произвольных суждений пока что невозможно

                        С этим никто и не спорит. Но в нашем случае, цель — проверить уже написанное доказательство, в котором, если оно полное, все используемые теоремы доказаны, а все цепочки вывода — приведены в явном виде. И нам не нужно угадывать, какое бы следствие вывести из теоремы A — за нас это сделал автор. Надо только проверить, что он в этом выводе не ошибся.
                        • –4
                          Так проблема же не в том, что «нужно угадывать, какое бы следствие вывести из теоремы», а в том, а нужно ли это следствие вообще.
                  • +3
                    Я так и не понял, что в вашем понимании значит «обосновать правильность выбора каждого метода».

                    Что есть «правильность выбора»? Мы имеет метод, для которого доказана работа на данных класса А. Если этот метод используем в теореме на данных не класса А, то он неприменим. Если на данных класса А, то он применим.

                    Если проверяемое доказательство уже задано в машину, мы всего лишь проверяем корректность всех логических переходов. Причем здесь произвольные суждения?
                    • –1
                      что в вашем понимании значит «обосновать правильность выбора каждого метода»

                      То, что любое доказательство, это совокупность различных приемов. Вот пример: school14-v.ucoz.ru/publ/1-1-0-2
                      Возможно, существуют и другие. От выбора метода на любом этапе зависят дальнейшие результаты. Выбор правильного метода — дает правильные результаты. Неприменимого — недостоверные.

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

                      Метод M — неприменим в конкретном доказательстве утверждения, но для M — доказана работа на данных класса А.
                      Применение М в рассуждениях даст недостоверный результат.

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


                      Одна только «корректность всех логических переходов» не гарантирует достоверность доказательства.
                      Необходимы так же достоверность исходных данных и логическая обоснованность самих переходов.
                      • +2
                        Так Вы и не объяснили, что за «правильность метода».

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

                        «Достоверность исходных данных» — что есть в вашем понимании достоверность и причем тут она мне тоже неясно. Все используемые в теореме утверждения должны быть предварительно доказаны. Все методы — обоснованы. Доказательство — формализовано.

                        Работа математиков при проверке корректности работы в этом плане тоже совершенно техническая, не творческая. За сим я откланяюсь, мне неинтересно разбираться в вашей терминологии.
                        • –1
                          Так вы и не объяснили, что за «правильность метода».

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

                          «Достоверность исходных данных» — что есть в вашем понимании достоверность и причем тут она мне тоже неясно.

                          Достоверность — самый обычный термин. В своем значении он и употребляется. Любые строгие утверждения могут строится исключительно на достоверных данных.

                          Все методы — обоснованы.

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

                          мне неинтересно разбираться в вашей терминологии.

                          Терминология тут, право, не причем. Она самая обычная и разбираться в ней нет необходимости:)
                          • +1
                            Термин неприменим для той ситуации с точки зрения математики, потому и странный.

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

                            Скажем, если у нас есть обоснованный агорифм нахождения наибольшего общего делителя, на наутральных числах он будет работать для них всегда, в любом месте доказательства, в любое время дня и ночи, для любого человека. Его обоснование формируется в виде теоремы, доказательство которой проверяется аналогичным же образом.
                            • 0
                              *под «Мы только проверяем уже имеющееся доказательство» я имел в виду данную ситуацию. Разумеется, у математиков есть и иные занятия.
                            • –2
                              проверяем уже имеющееся доказательство, это работа чисто техническая

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

                              Вам дают доказательство утверждения, построенное на своей новой уникальной математической теории. Приводят в рамках этой теории доказательство. Вы отдаете его своей чудо-программе и проверяете(еще непонятно как, т.к. надо ее не только правильно понять в итоге, но и прежде правильно формализовать для программы). Программа говорит — ОК (Errors — 0, Warnings — 14 567)
                              Доказательство утверждения в рамках теории успешное.

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

                              На мой взгляд, текст такой программы должен быть предельно прост:
                              {
                              print(42)
                              }
                              • +4
                                Вы вообще занимались математикой?
                                Про введение новых теорий я ничего не говорил, предполагается использование классических теорий. Если формализация доказательства невозможна, то это не доказательство.

                                Далее, у нас две теории. Если имеется их взаимная противоречивость, то, очевидно, в рамках более глобальной теории, иначе терминология «противоречие с другими теориями» является бессмыслицей в математике (Вы же не будете утверждать, что геометрии Лобачевского и Эвклида противоречат друг другу? Это просто разные формальные системы).

                                Если глобальная теория оказалась противоречивой, то она либо не имеет отношения, скажем, к формальной арифметике (в ней противоречивость доказать невозможно), либо есть утверждения, которые на самом деле не были доказаны.
                                • 0
                                  Забыл, еще есть вариант, что базовая формализация теории была противоречивой. Противоречивые аксиомы, например.
                                • –1
                                  Про введение новых теорий я ничего не говорил, предполагается использование классических теорий.

                                  Вы и обратного не говорили. И каких это классических теорий предполагается и кем? Если разговор скатывается в какие-то частные случаи — не вижу смысла его поддерживать. Мне уже предлагали здесь «новую логику». С моей стороны выражение «в общем случае» было почти в каждом ответе.

                                  Далее, у нас две теории.

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

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

                                          Это оригинальный вопрос, на который я ответил, что не вижу в этом смысла.

                                          И в частности потому, что в общем случае, там где подобные средства будут необходимы, очень вероятно, что

                                          ошибки лежат за рамками доказательства теоремы.


                                          Соотнося трудозатраты на разработку подобного продукта, его сложность, и практический выхлоп я до сих пор не услышал ни одного аргумента, чтобы поменять своего мнения:)
                                          • 0
                                            Вот теперь я услышал ответ на вопрос, хотя непонятно, зачем Вы изначально упомянули произведения искусства.

                                            Банальная экономия времени и денег, тем более системы а-ля Coq уже существуют. В итоге станет выгоднее создать систему с достаточным функционалом, чем оплачивать труд рецензентов и терять время выдающихся математиков.
                                            • +1
                                              Вряд ли это в реальности возможно. Возможно, наличие такого инструмента сократило бы время на доказывание, скажем теоремы о классификации простых конечных групп.

                                              Но ведь в науке не только важен результат. Но и сам путь к нему. Даже неверное доказательство может открыть пути для более выдающихся результатов.

                                              На хабре понятно желание программистов автоматизировать все и вся. Но со временем и до них дойдет, что некоторые вещи лучше оставить как есть. Для математиков, в частности, уже существует достаточное количество нужных им инструментов. И самые ценные для них это все-таки листок бумаги и ручка.
                                              • 0
                                                Госпожа Черепаха, перелогиньтесь пожалуйста
                                                • 0
                                                  Это Вы, простите, к кому сейчас обращаетесь?:)
                                                  • +1
                                                    Пока Воеводский описывает на Coq унивалентные основания математики на Хабрахабрике не могут доказать вторую теорему Гёделя на бумаге :-)
              • +7
                Произвольный предикат M1(A), который ниоткуда не следует, означает введение новой аксиомы. С чего вдруг «вброшена» новая аксиома?

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

                Проблема для пишущих будет в том, что нельзя будет делать так.

                Приходит Лившиц к Ландау и говорит:
                — Лев Давыдович, я в трамвае 40 страниц выкладок потерял!
                — Ничего, напишем «Откуда, очевидно, следует»
                • 0
                  Вы неправильно интерпретировали запись M1(A). Это не предикат, в общем случае. Это некоторый способ или прием, который применяется к некоторому набору фактов А, чтобы получить другой набор фактов S1 (скорее некоторый набор предикатов). Одну и ту же теорему можно доказать множеством совершенно разных способов используя разные приемы. Результата это не меняет. Но выбрав неправильный прием, можно получить уже другой результат. Как алгоритмически в общем случае определять применимость использования того или иного приема совершенно непонятно. Более того, как оценивать применимость совершенно нового и неизвестного ранее математического приема или способа?
                  • 0
                    >Это некоторый способ или прием, который применяется к некоторому набору фактов А, чтобы получить другой набор фактов S1 (скорее некоторый набор предикатов).

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

                    (any (x) Металл (x) => Металлопроводен (x)) ^ Металл (Медь) => Металлопроводен(Медь)

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

                    Например

                    perso.ens-lyon.fr/jeanmarie.madiot/coq100/
                    nevidal.org/sad.ru.html

                    >Более того, как оценивать применимость совершенно нового и неизвестного ранее математического приема или способа?

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

                    • 0
                      ведь изучением способов получать одни суждения из других занимается логика

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

                      Ну а почему нет, если существующих логик недостаточно

                      Ну в качестве эксперимента можно делать все что угодно:) Я же про это ничего не могу сказать и не знаю как это соотносится с объективной реальностью:) Эли это строго детерминированный алгоритм — это круто.
                      • 0
                        >Получать одни суждения из других это не проблемная часть математических доказательств.

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

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

                        Вот саму цепь составить — это во многом искусство, конечно.
          • 0
            Не так. Задача «думать» (самостоятельно искать пути от аксиом к доказываемой теореме, причём так, что бы заняло меньше бесконечного количества времени) — слишком большая. Программу — формализацию доказательства теоремы можно снабдить хинтами, благодаря которому верификатор затратит небольшое количество времени. Расстановка таких хинтов — творческий процесс, проверка — чисто механический.
        • 0
          Для произведений искусства есть золотое сечение. На сколько я понимаю, оно должно присутствовать в изобразительных произведениях, скульптуре, архитектуре, музыке. Если его нет, то произведение искусства, скорее всего, отстойное. Т.е. это универсальная, объективная оценка.

          Конечно есть и субъективная составляющая. Но она есть и в науке. Доказательство или какая-нибудь теория тоже может субъективно (не)нравиться.

          Ещё есть какая-то смысловая или прагматичная составляющая. И произведение искусства, и научная теория могут быть гармоничными/правильными, но совершенно бессмысленными.

          Вообще тема автоматической проверки, критериев истинности научного знания очень топтаная в философии науки:

          Есть позитивисты, которые считают, что единственный критерий истинности — это опыт. Для них эта теорема — какая-то бессмыслица, оторванная от физической реальности.

          Есть неопозитивисты, которые как-раз попробовали бы проверить истинность доказательства как предлагаете вы — в плоскости формального языка.

          Есть постпозитивисты, которые уделяют большее внимание роли научного сообщества и т.п. Типа если никто не может опровергнуть доказательство, значит его можно пока считать истинным. Если его никто не хочет опровергать, то скорее всего это какой-то бред, который может и правильный, но никому не нужен. Как-то так :)
    • +1
      Думаю, не делают, потому что пока такие доказательства — редкость, и в целом текущие доказательства можно «осилить». А так хорошо было бы принимать работы в чем-нибудь типа

      nevidal.org/sad.ru.html

      Если не хватает этой системы автоматизации дедукции, можно язык специальный разработать, на базе haskell :) И на нем писать вообще ВСЕ научные работы в естественных науках. Плюсы огромны — общая база знаний, поиск нужной работы, автоматическое построение доказательств, исключение плагиата и так далее.

      А рецензентам-то насколько проще будет — сразу смотришь на вывод, который гарантированно обладает новизной и следует из посылок.
      • +1
        А потом загрузить туда все знания человечества, и писать утверждения, например, «однополые браки это плохо», а система будет выдавать строго доказанный ответ: «истина» либо «ложь».
        • +2
          42
        • +1
          В данном случае будет облом на формализации смысла слова «плохо»
    • 0
      Потому что доказательства математических теорем базируются на нашем умении представлять (фантазировать) множеста.
      Компьютер не умеет выдумывать множества, и невозможно написать алгоритм, который может формализовать придумывание множеств.
      • 0
        Некоторые множества можно перебирать и, таким образом, придумывать. К примеру, можно написать алгоритм придумывания элементов множества всех строк (или фраз, соответствующих определённой грамматике). Другое дело, что ресурсы ограничены.

        Никто не предлагает сделать человеко-заменителя (ИР). Достаточно лишь механически проверить непротиворечивую выводимость каждого конкретного шага доказательства из фиксированного набора аксиом, неопределяемых понятий и правил вывода). Где нужно расставить хинты для выбора верификатором способов переборов, что бы верификация проходила в небольшое время.
      • –1
        • 0
          Я как-то не уловил связь между «отличает кошку от собаки» и «умеет придумывать множества».
          • +1
            Не отличает кошку от собаки, а на основе 10 миллионов случайных изображений из роликов на ютубе нейронная сеть сама выделила встречающиеся объекты на фотографиях, например кошек и стала отвечать на наличие данного объекта на фотографии. При этом фотографии с кошками никак не помечались при обучении.
            То есть нейронная сеть выделила абстрактное множество кошек. Это безусловно еще очень примитивный результат, но уже показывает, что компьютеры фактически могут абстрагироваться.
            • 0
              Эээ. Вот хаусдорфоры пространства — абстрактные множества. А множество кошек — ещё какое конкретное.
              • 0
                Какое же оно конкретное, если каждая кошка обладает уникальным генотипом и фенотипом, а некоторые кошки вообще существуют только в рисованном виде?
                • 0
                  Конкретный = существующий в реальном мире
                  Абстрактный = существующий только в нашем воображении.

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

      После гугления у меня возникло мнение, что страницы такой «википедии» должны быть написаны на симбиозе математического (декларативного) языка и языка императивных комментариев на около-естественном языке (на упрощенной разновидности английского). Что бы утверждения на математическом языке верифицировали не только конечные узлы-гипотезы, но и комментарии по конкретным фразам. Т.е. комментарии, в общем-то, должны быть избыточными для доказательства (но недостаточными для оного сами по себе), но благодаря ним должна сохраниться возможность ориентироваться в доказательствах.

      Думаю, что если никто не займёт эту нишу, то в течение ближайших 5 лет я мог бы создать ризонер-верификатор подобного языка… Единственно, у меня сложилось впечатление, что профессиональным математикам это не интересно, соответственно, мне тем более тяжело выделить своё свободное время. Видел в сети только сборник доказательств на ML — этого мало.
      • +1
        Почитайте про проект sciencewise.info Семантическая сеть на базе arxiv.org

        Как раз семантическая википедия для научных статей. Написана на Django. Руководители проекта рускоязычные, если интересуетесь, то можете попробовать присоединиться.
        • 0
          Это, наверное, не совсем то… Это механизм генерации связей между понятиями (как я понял), а не способ формализации знаний. Или я ошибаюсь?
          • 0
            Я не сильно знаком с проектом. Я просто знаю людей, которые с ним работают. Так что точно вам не смогу сказать, но по моему вы правы, это именно связь между научными статьями и как следствие понятиями. Возможно на базе sciencewise.info можно было бы сделать и формализацию знаний, т.к. инструментов там много уже создано.
      • 0
        Я тоже хотел. Для начала хотел перенести в формальную систему те теоремы что изучал в университете, когда понял что к пятому курсу начал их забывать. Но потом руки так и не дошли.
        • 0
          «Просто перенести» довольно много начинали. Проблема в том, что формальные языки математических доказательств практически не читаемы — слишком формальны они по сравнению с естественным языком. На естественном языке (пусть и с кванторами и специальными обозначениями) — дохлый номер описывать. Так что нужно для начала придумать как описывать достаточно кратко, что бы человек мог понять, но не все детали расписывались — либо, как я написал, хотя бы придумывать, как аннотировать машинный язык доказательства понятным человеку языком, но так, что бы не нужно было думать: «а не придумал ли комментатор лишнего».
          • 0
            Ну тут мне кажется также как с программным кодом.

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

            В том числе и кванторами можно, код всё-таки для человека а не для машины. Вот пример:
            forall n m : nat, le n m -> le (S n) (S m)
            


            И проблема комментариев та же, что и в программном коде. Комментарии могут устаревать, и не соответствовать коду.

            Верифицировать их мне честно говоря не кажется хорошей идеей.

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

            Ну и точно также, как в программировании кроме программного кода мы имеем всякую документацию, диаграммы, алгоритмы и тому подобные вещи, которые нужны не для компилятора, а для людей — так и в доказательствах можно дать на пару страниц интуитивные соображения, идеи, диаграммы и т.п., а ниже полный код на формальном языке. Кто поймёт идею по неформальному описанию — хорошо, кто не поймёт — пусть идёт разбираться в коде.
            • +1
              Естественно, при прочих равных лучше разбить код на разные леммы. Но проблема в том, что в отличие от кода (реализующего игры, бизнес-процессы и т.п.), математика — очень абстрактная, часто не имеющая «физического смысла»… И работать с кодом, состоящим из «леммы1, леммы2,… леммы 4234, объединяющей леммы 42 и т.п.» — очень сложно.

              Собственно, идея с комментариями пришла ко мне, когда я участвовал в холиварах: комментировать или нет. Во-первых, мне показалось, что код нужно комментировать так, что бы осветить аспекты программы, плохо выражаемые на данном языке. К примеру, блок из кучи императивных mov/jmp на ассемблере имеет смысл прокомментировать декларацией того, что этот код должен делать в предметной области (открывать файл, мигать светодиодиками и т.п.). Или, наоборот, код на прологе или лиспе часто имеет смысл прокомментировать: как конкретно обходится та или иная рекурсия на используемой платформе.

              Во-вторых, в качестве решения устаревания кода мне пришла идея включить комментарии в сам язык — сделав таким образом гибридный императивно-декларативный язык. Т.е. комментарии могут быть значимым кодом — и, к примеру, если с учётом синонимов/фразеологизмов (устоявшихся языковых паттернов) комментарий соответствует коду на 50%, то пропускать этот код через интерпретатор без ошибки.

              К слову, идея смеси декларативного языка с императивным не нова (только цели другие): к примеру, SQL`ем описать запросы к БД часто невозможно без того, что бы база не начала тупить, перебирая то, что не надо. Для того, что бы этого избежать любая вменяемая СУБД имеет механизм хинтов — позволяющих скорректировать план запросов для данного запроса. Получается, что декларативный SQL — это всего лишь человеко-понятный комментарий к программе, использующей глубокое знание деталей платформы (которая, в свою очередь использует SQL как основу).

              Ещё никто не мешает там, где это удобно, использовать один язык, а в других местах — другой. Один императивный, другой декларативный (или какой-нибудь аспектный, не важно).
              • 0
                > леммы1, леммы2,… леммы 4234, объединяющей леммы 42 и т.п.
                Вопрос об именовании лемм выходит за рамки верификации. Ведь при текущем положении дел математики как-то ссылаются на леммы, приведенные несколькими страницами ранее, то есть дают им какие-то имена, пусть и численные.

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

                > Во-вторых, в качестве решения устаревания кода мне пришла идея включить комментарии в сам язык — сделав таким образом гибридный императивно-декларативный язык. Т.е. комментарии могут быть значимым кодом — и, к примеру, если с учётом синонимов/фразеологизмов (устоявшихся языковых паттернов) комментарий соответствует коду на 50%, то пропускать этот код через интерпретатор без ошибки.
                Вот это уже не нравится. Рассуждения про 50% и т.п. вносят нестрогость в эту проверку. На мой взгляд либо верификатор умеет читать эти комментарии полноценно — тогда почему бы не выкинуть основной человеконепонятный код и не писать всё доказательство такими комментариями, либо не умеет (если комментарии добавляют интуитивного понимания, которого верификатор не имеет) — тогда смиримся что они только для людей.

                > К слову, идея смеси декларативного языка с императивным не нова: к примеру, SQL`ем описать запросы к БД часто невозможно без того, что бы база не начала тупить, перебирая то, что не надо. Для того, что бы этого избежать любая вменяемая СУБД имеет механизм хинтов — позволяющих скорректировать план запросов для данного запроса. Получается, что декларативный SQL — это всего лишь человеко-понятный комментарий к программе, использующей глубокое знание деталей платформы (которая, в свою очередь использует SQL как основу).
                Интересный пример. Но здесь это имеет смысл из-за скорости вычислений. В аналогичном случае в верификаторе ничего не мешает написать утверждение на языке высокого уровня, которое транслятор переведёт на язык низкого уровня, пусть и неэффективно, эффективность тут не нужна.

                Может быть моё сомнение по поводу включения комментариев в язык можно сформулировать так: проверить соответствие между кодом и комментарием не проще чем сгенерировать код по комментарию.

                Другое дело что можно писать.
                Утверждение1.
                Утверждение2.
                Отсюда очевидным образом следует утверждение3 (в скобках куча кода)
                


                То есть для человека утверждение3 действительно следует очевидным образом, но для верификатора в скобках это доказано более детально. Причем код в скобках можно от человека спрятать за ссылкой «подробнее». Но это уже непринципиальные детали, связанные с тем что верификатор маломощен. Иначе он мог бы (раз человеку очевидно) вывести то что написано в скобках самостоятельно методом перебора.
    • 0
      Вообще-то этой проблемой занимается сейчас много людей, Воеводский, например, продвигает свою гомотопическую теорию типов homotopytypetheory.org/
    • НЛО прилетело и опубликовало эту надпись здесь
    • +1
      Потому что настоящие открытия в математики могут вообще не вписываться в формальный язык, который вы придумаете.
  • +1
    Статьи не компьютерной программой были написаны? Судя по тому что математики не смогли в них разобраться, очень похоже.

    Хотя в доказательстве Перельмана тоже разобрались единицы, и прятался он от коллег-математиков не хуже
    • +2
      Нет, просто тело в том, что во всём мире наберётся полсотни человек, которые разбираются в этой области математики. И у них, разумеется, есть свои проблемы, помимо чтения чужих архиважных доказательств. Может на следующей конференции они соберутся и наконец разберутся что к чему.
    • 0
      Статьи, написанные компьютерной программой, распознаются очень легко, если хоть чуть-чуть шарить в этой области.
  • +1
    Вроде ж об этом писали на хабре — Японский математик доказал АВС-гипотезу
    • +10
      ИМХО, данная статья интересней и развернутей.
  • +19
    Это похоже на тарабарщину не только для обывателя. Это было тарабарщиной и для математического сообщества.
    Это не вся правда. Дело в том, что среди приведенной литературы, Мотидзуки ссылается на свои собственные работы, т.е. кроме 500 страниц доказательства abc-гипотезы, нужно сначала освоить несколько сот страниц других его работ.
    Если провести аналогию для программиста: это если бы он создал свой собственный язык программирования, нет скорее свою библиотеку, а за тем на ней разработал все остальное.
    Если дальше развить эту аналогию, как пример для C/C++, человек разработал (пусть под себя) «другую» stdlib, далее используя ее доказал гипотезу — с его точки зрения единственно правильное решение, ведь стандартная stdlib не достаточно гибка, не удобна, да и вообще не позволяет ему развернуться как следует. Для понимающих, это как после java/c# и ко, пересесть ну например на erlang (не в обиду разработчикам java/c#).
    Что абсолютно не понятно, с моей точки зрения, это нежелание всего «математического» мира, всех этих выдающихся «Перельманов», «Уайльсов» и т.д. «изучить» эту библиотеку, чтобы понять доказательство этой важнейшей гипотезы.
    Другая аналогия — вот вы выложили в интернете крутющую библиотеку, которую заметим, вы писали в свое свободное время. Но она ну например для ada. И теперь все ее хотят, но для C++, и вам говорят — мы не понимаем как оно работает, а перепишите ка это для C++ и кроме того не используйте своих библиотек, а юзайте исключительно stdlib.
    Мне все, что происходит с Мотидзуки и его доказательством, видится как то так.
    • +4
      Отличие в том, что в случае программирования можно проверить, работает ли библиотека — даже не заглядывая в код, просто запустив и пользуясь. А убедившись что код работает, можно уже портировать на другие языки если хочется.

      А единственная ценность доказательства — это его «код» — потому что не разобравшись в нём нельзя быть уверенным что оно истинно, и пользоваться его утверждением. А раз так — пока доказательство никто не понимает — оно не несёт никакой ценности. И нет уверенности что если кто-то потратит кучу времени на разбор этого доказательства — не окажется что в нём ошибка и время потрачено зря.
      • +2
        Отличие в том, что в случае программирования можно проверить, работает ли библиотека — даже не заглядывая в код, просто запустив и пользуясь.


        Можно копнуть дальше, изобретена не только библиотека но и архитектура железа, на котором все это вертится.
        • +1
          Ну тогда по крайней мере автор может в качестве демонстрации решить какую-то считавшуюся неразрешимой вычислительную задачу на своём железе. Тогда к нему будет проявлен интерес, но не ранее того.
          • +1
            Дык может он втихоря биткойны майнит на калькуляторе тысячами ;)
      • 0
        … пока доказательство никто не понимает — оно не несёт никакой ценности.
        Вот и вас логика какая-то потребительски однобокая.
        А убедившись что код работает, можно уже портировать на другие языки если хочется.
        А если нет ады под рукой?
        И нет уверенности что если кто-то потратит кучу времени на разбор этого доказательства — не окажется что в нём ошибка и время потрачено зря.
        Не зря, т.к. вы постигли мышление выдающегося математика (или выучили его библиотеку).
        • +1
          > Не зря, т.к. вы постигли мышление выдающегося математика (или выучили его библиотеку).

          Эту будет иметь смысл только если математик действительно выдающийся (а не безумен), а также если те, кто будут разбирать его рукопись менее выдающиеся. Иначе их время можно было бы потратить с большей пользой.
          • +5
            Согласен отчасти: с одной стороны, достаточно много его работ признаны математическим сообществом. Напомню мы говорим о человеке, ставшим в 23 года доктором, а в 33 профессором.
            С другой стороны, для того что бы понять не безумен ли он, нужно понять его выкладки ..., а это имеет смысл только если он не безумен. Согласитесь, это замкнутый круг получается.
            • 0
              ага.
              и предлагаемый софт даёт из него выход.
              • 0
                Какой простите софт? Где и кем предлагаемый?
                • 0
                  простите. Тут: habrahabr.ru/post/183374/#comment_6378020
                  • 0
                    В математике такого порядка я скорее дилетант, чем профи. В программировании же, скорее наоборот. Тем не менее думается мне, что создать что-то предложеное там не является возможным, как минимум по нескольким причинам:
                    — количество абстракций просто гигантское;
                    — множество понятий просто нельзя формализовать, можно формализовать только например действия над этими понятиями либо только результат определенного действия;
                    — некоторые уже существующие доказательства (например доказательство от обратного) невероятно сложно описать какими либо абстракциями алгоритмически;
                    — еще сложнее представить его в такой абстрактной форме, что бы алгоритм софта (какой бы умный он не был) однозначно ответил да/нет/константа/множество и т.д. — иногда математика оперирует оценочными суждениями;
                    — все это вообще не реально, если мы имеем дело с экспандирующими абстракциями (что-нибудь вида произведения двух и более «матричных» или даже «бесконечных» абстракций);
                    Чтобы не быть голословным, пример:
                    Есть какая-то (неточная) мат. абстракция LA, которая может быть реализована только лямбдой (в программистском смысле). В доказательстве используется интеграл от этой лямбды или еще хуже произведение с другой мат. абстракцией LB, тоже представленой только лямбдой. Так вот, моей дилетантской математики достаточно чтобы представить в голове или на бумаге свойства такого интеграла или произведения. Но я как программист не имею ни малейшего понятия как представить результат алгоритмически — даже что это за конструкция (как должна быть формализована в программе) не представляю.
                    Я только за, если кто сможет ..., но пока помоему, без вариантов.
                    Для тех кто в танке, просьба не делать голословных заявлений, а описать алгоритмически ну например какую нибудь элементарную функцию (по Лиувилю) а потом применить эту абстракцию для доказательства ну например следующего следствия теоремы Лиувилля: интеграл от e^{x^2} не является элементарной функцией.
                    • 0
                      Да еще чего забыл: у такого мета-языка (буде его кто-либо осилит) будет огромнейшая семантическая составляющая, со всеми вытекающеми. Ну или если короче, сложный будет очень и для освоения и для написания «сценариев» доказательства. Я уж молчу про читабельность по сравнению с сухим «языком» мат. формул. То что в результате получится в исходниках, сам «писатель» врядли осилит через пару месяцев.
                      Так вот, доказательство теоремы от Мотидзуки на английском и «математическом» то языках никто не может (не хочет) понять, а вы собираетесь в эту кучу еще какой-то мета-язык запихнуть? Или вы считаете, что он самодостаточен, т.е. ошибки на этом языке исключены по определению? — накидал кучу исходников — оно сказало теорема доказана и все?
                      Смею вас разочаровать, такого не бывает. За свою карьеру программером, я много повидал исходников, кстати написанных в том числе и гениями (по моим скромным понятиям) — так вот абстрактный код в вакууме (об ошибках говоря) бывает трех типов:
                      — код содержит явные ошибки;
                      — ошибки в коде еще не выявлены;
                      — ошибки есть но пока не происходят на текущих данных (зависят от каких-либо входных параметров в том числе от положения звезд на небе).
                      Какими бы тест-кейсами код не покрывался, какой бы ревью не делался, сколь долго тестеры не гоняли бы этот код. И чем абстрактнее или формальнее язык программирования, тем чаще можно словить баг. А здесь у нас вообще абстрактно-формально-описательный язык в абсолюте (в степени X факториал), который оперирует даже не объектами, классами и выражениями, а абстрактными моделями и функциональными описаниями.
                      Я вам больше скажу — тот кто будет вынужден писать на этом — пострадает почище того, кто этот «язык» будет реализовывать.
                      Почему-то эту сторону вопроса никто из поборников «универсального математического компилятора» вообще не рассматривал. А надо было бы…
                      • +1
                        Существуют языки, отсутствие ошибок в которых формально доказано. Математически. И если такой язык скажет, что доказательство верно — оно действительно верно, в рамках математики, которой доказано что верен язык (интерпретатор языка). Если же интерпретатор говорит, что док-во неверно, он сообщает также, какой переход неправилен. Математику нужно лишь проверить, соответствует ли код, написанный для этого перехода, самому переходу в док-ве. При этом переход достаточно элементарен — на том уровне абстракций, на котором он применяется (а ля «согласно теореме Х», при этом у теоремы простые условие и вывод, но сложное док-во). Если переход закодирован неверно, математик его исправляет и возобновляет проверку, в противном случае док-во содержит ошибку.
      • НЛО прилетело и опубликовало эту надпись здесь
    • +1
      Я подозреваю что у всего математического мира нежелание проверять из-за того, что по аналогии с языками программирования, людям привыкшим к C#/Java для понимания доказательства придется предварительно изучить Brainfuck
    • +2
      Что абсолютно не понятно, с моей точки зрения, это нежелание всего «математического» мира, всех этих выдающихся «Перельманов», «Уайльсов» и т.д. «изучить» эту библиотеку, чтобы понять доказательство этой важнейшей гипотезы.


      Это-то как раз понятно. Никто не оплатит эту работу. Ну поймёт кто-то эту работу, и что? Математикам же платят за количество публикаций (во всём мире), а не за понимание (и это гигантская печалька).
    • +2
      Спасибо за локализацию статьи :)
    • –1
      И такие вещи существуют в программировании. Взять, например, язык K и написанную на нем kdb.

      Синтаксис K:

      "Hello world!"

      / The following expression sorts a list of strings by their lengths:
      
      x@>#:'x

      / tables
      
      n: 1000
      names: `bob `ted `carol `alice
      emp.salary: 20000 + n _draw 10000
      emp.name: names[n _draw #names]
      emp.manager: names[n _draw #names]
      
      `show $ `emp
      
      / modify salary to be twice the salary
      
      emp.salary: 2*emp.salary
      
      / create a chart
      
      emp.salary..c:`chart
      `show $ `emp.salary
      • 0
        Это вы к чему вообще? Язык «программирования» K видел, ну и-и?
        Я вообще-то просто аналогию проводил. Безпредметно.
        Кстати, если это к другой ветке, где обсуждается «универсальный математический доказатель». И вы язык «К» собираетесь в этом качестве прицепить — не стоит. Это примерно, то же что пытатся для решения математических задач использовать 1C-бухгалтерию вместо например матлаб.
        • 0
          Вы написали: «Если провести аналогию для программиста: это если бы он создал свой собственный язык программирования, нет скорее свою библиотеку, а за тем на ней разработал все остальное»

          K и kdb — как раз пример такого случая.
  • –55
    Ещё раз убедился в том, что математика является гуманитарной наукой.
    • +5
      Как Вы определяете термин «гуманитарная наука»?
    • +56
      Только гуманитарий мог такое сморозить.
      • –6
        Физ-мат, аспирантура, аналитические решения внутренних задач гидродинамики при ламинарном и стационарном режимах, решение бигармонического уравнения Навье-Стокса методом малых возмущений, цепочки Боголюбова,… — такое у меня образование. Более того, я искренне понимаю Ваши поспешные минусы к фразе о математике.
        • +11
          В таком случае, вы просто не понимаете смысла слова "гуманитарный".
      • +6
        Строго говоря, математика даже не является наукой. Это формальная система правил, которыми руководствуется человек в своих построениях. Математика — явление человеческой природы, один из языков человека.

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

        Курите философию науки, господа.
        • +3
          Не люблю такие холивары, потому что нереально кого-либо переубедить. Но я все таки отвечу.

          Литература, философия — это не науки. Это вот точно просто порождение человеческой мысли. Если подумать, то ясно, что без человека философии бы не возникло. Если б на планете появились мыслящие кристаллы, думали бы они по-другому и нашей философии бы точно не было. А вот математика от человека точно не зависит. Она одинакова в любой точке Вселенной. Как и физика, как и химия. Да, математика — свод правил. Но они взялись из нашего мира, а не из человеческого воображения. Так что называть математику гуманитарной наукой неправильно. Я бы сказал, что ставить рядом слова «наука» и «гуманитарная» вообще неправильно, но это уже отдельный разговор.

          Дальше спорить не вижу смысла.
          • –1
            . А вот математика от человека точно не зависит.

            Ошибка в этом.
            Звезды или галактики объективно существуют без наблюдателя. Числа и прочие математические понятия — не существуют. Они абстрактны. Даже при всей их неизменности.
            • +2
              Звезды или галактики объективно существуют без наблюдателя.

              Кстати не факт.

              Тем не менее, математика описывает некие законы, как правильно было подмечено — не зависящие от человека, пусть и субъективно (в рамках некой человеческой логики). Другой вопрос — насколько хорошо мы описываем их? Наши абстракции возможно и не существуют, но то, к чему мы подбираемся с помощью них — вполне реально
              А если брать пример с кристаллами, то да, философия у них скорее всего была бы другой. И математика тоже другой, но тут речь идет скорее о реализации, а не о целях и конечных результатах. Так что математику «кристаллов» (да простит меня Император за эту ересь) вполне можно было бы назвать другим «языком» математики. К тому же есть вероятность, что и человеческая математика еще существенно изменится со временем.
            • 0
              Звёзды и галактики существуют только в предположении, что законы природы везде одинаковы. Если убрать это предположение, то мы можем лишь сказать, что из сферы, окружающей нас, на наш разум воздействуют чем-то похожим на свет от свечи.
          • +6
            А насчет гуманитарных наук. Та же социология вполне удовлетворяет критериям настоящей науки, при этом оставаясь гуманитарной (т.к. существует только в контексте человека). Другое дело, что она чуть менее чем полностью захвачена идиотами, но это не мешает в ней ставить эксперименты и вести настоящие исследования.
        • +2
          Что это значит? Математика — наука. Если попросят привести пример науки, и вы скажете «Математика», то будете правы на 100%. В энциклопедии Британника математика определяется как наука. Конечно, вы можете иметь альтернативный взгляд на смысл понятий «наука» и «математика», однако в том виде, в котором пытаетесь представить их вы, они явно противоречат общепринятым. По меньшей мере, то, о чём вы говорите, скорее соответствует разделу философии под названием «логика», чем понятию «математика».

          Не гуманитаризируйте на техническом ресурсе, не надо патетичненьких фраз вроде «математика — язык человека» или «математика — царица наук».
          • –1
            Мой взгляд на понятие математики — это общепринятый взгляд серьезных ученых-естественников, да и самих математиков, интересующихся предметом дальше своего носа.

            А ваш взгляд — это ололо-кококо студента-недоучки, который знает только то, что он должен ненавидеть гуманитариев.
            Даже ваша фраза про язык вас выдает с головой. У этого слова есть строгое формальное определение, о котором вы, разумеется, не слышали.

            Для большинства людей математика является наукой, что и отражено в определении британики. Они так привыкли и им так вдолбили в школе. Хотите уподобляться большинству — стоит начать сидеть в одноклассниках и смотреть Дом-2.
            • +1
              Каких учёных? Каких математиков? Где пруфы на научные работы? На книги, цитаты? Вы знаете, что допустили как минимум две логические ошибки разных типов (аргумент к социальной безуспешности, аппеляция к анонимному авторитету), о которых вы, разумеется, даже не слышали?
              • +1
                wwintspace.net/n-427.html

                Рекомендую ознакомиться со статьей целиком. Это лишь малый отрывок.

                Никто не знает, сохранят ли грядущие века и тысячелетия сегодняшнее деление наук на естественные и гуманитарные. Но даже и сегодня безоговорочное отнесение математики к естественным наукам вызывает серьезные возражения. Ее родство с естественными науками, прежде всего — с физикой, очевидно, и нередко приходится слышать, что математика является частью физики, поскольку описывает свойства внешнего, физического мира. Но с тем же успехом ее можно считать частью психологии, поскольку изучаемые в ней абстракции суть явления нашего мышления, а значит, должны проходить по ведомству психологии. Не менее очевидна и логическая, приближающаяся к философской, природа математики. Скажем, знаменитую теорему Гёделя о неполноте, гласящую, что какие бы способы доказывания ни установить, всегда найдется истинное, но не доказуемое утверждение — причем даже среди утверждений о натуральных числах, — эту теорему можно считать теоремой теории познания.
                Владимир Андреевич Успенский, доктор физико-математических наук, заведующий кафедрой математической логики и теории алгоритмов мехмата МГУ, Земля (Sol III).

                • –1
                  Там многовато проблематики и воды, но отдельные моменты вполне точно отражают сомнения самих математиков по поводы природы того, что они изучают.
                • +6
                  Когда учили нас, то математику относили не к естественным и не к гуманитарным наукам, а к точным.
                  Потому что есть существенные отличия и от естественных (изучается порождение человеческого разума, а не природный объект), и от гуманитарных (есть понятие эксперимента, позволяющее объективно разделить утверждения на истинные и ложные).
                • +2
                  Ну, во-первых, нужно отметить, что
                  Авторами «Британники» являются ведущие мировые эксперты, среди которых десятки лауреатов Нобелевской премии. В разное время статьи для «Британники» писали Зигмунд Фрейд, Альберт Эйнштейн, Мария Кюри, Генри Форд, Лев Троцкий. Современная версия «Британники» создана при участии около 4000 авторов и редакторов.
                  (взято из вики)

                  Поэтому, если ссылаться на авторитеты, то получим две противоборствующие стороны: «математика — наука» и «математика — не наука» (а лучше уточнить: «математика — естественная наука» и «математика — гуманитарная наука», потому что, насколько я понял из статьи, В.А. Успенский говорит об отнесении «науки математики» к гуманитарной ветке, а не о лишении математики статуса науки, что, с другой стороны, хотите сделать вы:
                  Строго говоря, математика даже не является наукой.
                  Во-вторых, с рассуждениями В.А. Успенского я тоже не согласен. То, что математика отошла от «сухой цифири» (хотя весьма глупым выглядит попытка доказать это путем упоминания о парадоксе близнецов, который не является чисто математической проблемой (а тем более глупо говорить о парадоксе близнецов как о проблеме, ждущей решения), или о «попытках (математиков) познания бесконечного, которые значительно расширяют горизонты мышления») — не повод переносить её в разряд гуманитарных дисциплин. А почему бы туда не перенести физику? Физики (особенно квантовые) сейчас рассуждают о немыслимых вещах, куда дальше уходя от «тупо цифири». Опять же, то, что математика «расширяет навыки мышления», улучшает «строгость мышления и воображение» — это просто свойство математики (и, скажем, того же программирования тоже) — не повод сделать её гуманитарной. А может сделаем информатику гуманитарной дисциплиной? Ведь у нас тут абстракции разные, знаете ли.

                  Потом, В.А. Успенский называет «вторым и более глубоким фактором» то, что
                  занятия математикой и сопряженное с ними систематическое использование точной терминологии определенным образом сказываются на психологии, по крайней мере в части восприятия слов
                  На хабре была не одна статья о профессиональной деформации программистов — так что, может всё же сделаем информатику гуманитарной дисциплиной, ведь программирование сопряжено с использованием точной терминологии, что определённым образом складывается на психологии (кстати, почему на психологии, а не на психике?). Или физику?

                  Ну и третий фактор, который упоминается статье уже смещён до безобразия. Ображение к этимологии и толкованию слов для… для чего? Это вообще аргументом можно назвать? В англ. языке есть слово fail, которому нет прямого аналога в русском — так что теперь? А может отсутствие в (исконно?) русском языке толкования слова «ложь» в том смысле, в котором это делают в математике, наоборот отдаляет математику от блока гуманитарных наук. Разве нет?

                  В общем лучи негодования В.А. Успенскому за его статью. Не примите меня за технофашиста, но статья в самом деле «гуманитарная с ног до головы», с безобразной, маразматичной, аргументацией. Зачем автор опять затрагивает эту якобы проблему «физиков и лириков» («технарей и гуманитариев»), да сколько можно! Это моё ИМХО, естестественно.
                  • 0
                    *смешон
            • +2
              Вы сейчас воспроизводите мнение группы Бурбаки. Многие наши математики не разделяет ее. Хорошо известно выражение Арнольда, что математика — экспериментальная наука.
              • 0
                Я отношусь к естественникам и не встречал еще кого-либо среди коллег, кто разделял это определение. Т.к. различия между математическим «экспериментом» и натурным достаточно очевидны.
                • +1
                  Считайте, что одного человека вы знаете — это я.

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

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

                  То в математике это сводится к формализацию формулировок, завязанных на логических построениях.
                  • –1
                    Это сейчас схема такая. Раньше было по-другому — кто кого переспорит на площади, тот и прав. Возможно, через некоторое время схема снова изменится, и истинность теорем будет решаться на заседаниях Думы голосованием. Или наоборот, найдётся теория, для которой и нынешняя матлогика, и теория множеств будут следствиями (в рамках правил вывода — или того, что их заменит — уже этой теории). И это не сделает математику ни естественной, ни, тем более, гуманитарной наукой. «Математика — это язык».
                    • 0
                      Вы не правы, причем не правы во всем. Да еще и передергиваете с думой.
                      1) В математике никогда не было того, что вы говорите. Вы явно путаете с философией и риторикой.
                      2) Доказательства эволюционировали, что в физике, что в математике. Достаточно вспомнить Аристотеля и то, как он доказывал то, что для движения нужна сила.
                      3) Эти новые рамки будут созданы на основе решения парадоксов и проблем, вызванных старой системой. Так теория множеств возникла на основе развитии рядов и геометрии, так и интуиционизм и теория Цермело-Френкеля возникли на основе парадоксов теории множеств, ровно как действительные число ввели из-за развития геометрии, ровно как комплексные числа из-за появления формулы Кардано.
                      • +1
                        1) Наверное, путаю. Но была ли до Евклида и Аристотеля математика отделена от философии?
                        2) Действительно. В математике — из-за уточнения набора аксиом той или иной теории. В физике? Наверное, можно законы рассматривать, как разновидность аксиом, а объекты «реального мира» — как объекты этой теории. Но получится не более, чем математическая модель соответствующего кусочка мира. И задачей физики будет проверить соответствие этой модели наблюдаемому миру, а задачей математики — говорить, какие теоремы будут работать и как они будут проявляться в «наблюдаемых» терминах. У математиков будут «доказательства», а у физиков — «подтверждения».
                        3) Вот упоминание интуиционизма здесь действительно интересно. Интуиционизм и конструктивизм предлагают использование другой логики, т.е. из одного и того же набора аксиом получаются разные наборы теорем. Можно сказать, что это разные математики.
                        А насчет «парадоксов и проблем»… как насчёт континуум-гипотезы и аксиомы выбора? В реальном мире континуум-гипотеза не нужна вообще, ни она, ни её отрицание ничего особенного не дают. А от аксиомы выбора вообще одни неприятности, вроде парадокса Банаха-Тарского. Тем не менее, математики её почему-то очень любят :)
                        • 0
                          1) Да, более чем. Справедливости ради надо отметить, что платоновская философия аппелировала к математики, но не более
                          2) Вы сейчас отождествляете мир как таковой с материальной его частью, но это не так.
                          3) Нет, не разные. Фундаментальная математика формирует разные подходы к решению задач. Но их набор остается одинаковым. Возникающие противоречия составляют обойму тех парадоксов, которые необходимо решать и которые в будущем приведут к развитию новых теорий.

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

                          К примеру, обычному электрику или программисту из гугла глубоко наплевать на то является ли электрон неделимой частицой или нет. Также не волнует вопрос о количестве видов нейтрино или о распаде протона. Ну и т.д.
                          • 0
                            Я вообще не считаю, что математика имеет отношение к реальному миру (если реальный мир вообще существует). Она занимается абстрактными понятиями, некоторые из которых физика и другие науки используют для своих моделей.
                            Насколько математика универсальна — не знаю. Например, может ли существовать математика без натуральных чисел или без теории множеств. Или теория множеств быть совсем не такой, как у нас (и вообще не иметь модели в «нашей» математике). Скорее всего, это всё возможно.
                            «Набор подходов остаётся одинаковым»? Наверное, смотря насколько обобщать. «Доказывать от противного» — это подход? В «нашей» математике он работает, а, например, в конструктивизме нет. Или «подходами» вы называете правила вывода? Или общий принцип «есть аксиомы, и есть теоремы»? Или вообще «утверждения могут быть истинными, а могут быть ложными»? Я пока не слышал о математических теориях, в которых эти принципы бы нарушались. Но это не значит, что «у кристаллов» они обязаны быть.
          • 0
            Помнится, Фейнман не считал математику наукой, т.к. её «нельзя» проверить экспериментально.
            Даже на замечательной связи, объединяющей физику с математикой, мы не задержимся. (Математика, с нашей точки зрения, не наука в том смысле, что она не относится к естественным наукам. Ведь мерило ее справедливости отнюдь не опыт.) Кстати, не все то, что не наука, уж обязательно плохо. Любовь, например, тоже не наука. Словом, когда какую-то вещь называют не наукой, это не значит, что с нею что-то неладно: просто не наука она, и всё.

            Признаться, я с этим не согласен. Да и проверить её очень даже можно: взять, к примеру, геометрию. Берём относительно плоскую поверхность, рисуем круг радиуса R, измеряем площадь. Математика предсказывает, что она будет примерно равна 22/7 R^2. Рисуем концентрический круг радиуса 2R и измеряем его площадь. Математика предсказывает, что площадь увеличится ровно в четыре раза.
            Если бы эти соотношения не выполнялись, современная математика была бы совсем иной, ведь по преданию математика родилась как раз из практической необходимости измерять землю в Египте.
            • +3
              не наука в том смысле, что она не относится к естественным наукам
              То бишь Фейнман не относит математику к естественным наукам, а не к наукам вообще. Если выделить категории «точных, естественных и инженерных наук», то математика попадает в «точные».
        • 0
          Спор о верности любого утверждения вида «А — это Б», где А и Б — некоторые слова естественного языка, на мой взгляд лишены всякого смысла. Естественный язык отличается от формального тем, что в нём значение слов держится лишь на негласном предположении, что собеседники подразумевают одно и то же понятие. В общем случае два человека могут иметь разные точки зрения о значении слова «наука», и нет чёткого критерия, по которому одно из них можно однозначно выбрать верным. При некоторых значениях слова «наука», фраза «математика — наука» верна, при некоторых нет. Принцип большинства, отсылка к авторитету — это всё логические заблуждения.
  • +4
    Статья читается с такой интригой! Прямо детектив какой-то. Очень интересно, большое спасибо.
  • +17