Comments 405
В чем парадокс?
Доказательство есть, но в то же время его нет.
Что значит «нет»? Если я правильно понял, оно есть, но его понимает только его автор.
В этом и суть парадокса. Доказательство вон лежит, в открытом доступе по ссылкам выше, но пока его не признают остальные математики, оно не существует.
Да как так не существует? Если оно лежит в открытом доступе, то оно существует. «Не признано» — согласен. Но признание не является критерием существования. По-прежнему не вижу никакого парадокса.
Ну проблема в том, что пока кто-то не проверит, нельзя быть уверенным что доказательство не содержит ошибки.
И принято было, что либо сообщество проверяет доказательство и говорит «у вас тут ошибка в 30 строке», либо подтверждает его истинность. А тут не могут сделать ни того ни другого.
Другое дело непонятно как отличить такие «непонятные» доказательства от бреда, который понять в принципе невозможно. Мне кажется без введения формального языка, который могла бы проверить машина, тут не обойтись.
И принято было, что либо сообщество проверяет доказательство и говорит «у вас тут ошибка в 30 строке», либо подтверждает его истинность. А тут не могут сделать ни того ни другого.
Другое дело непонятно как отличить такие «непонятные» доказательства от бреда, который понять в принципе невозможно. Мне кажется без введения формального языка, который могла бы проверить машина, тут не обойтись.
Мне кажется без введения формального языка, который могла бы проверить машинаВы так математиков без хлеба оставите.
Математикам вполне останется творческая работа по придумыванию доказательств (в этом люди думаю долго, если не всегда, будут впереди машин), а также по объяснению идей проверенных доказательств друг другу.
Точно также если мы повсеместно начнём верифицировать программы — ведь программисты без хлеба не останутся. Потому что писать программы тоже может только человек.
Да? А мы вот тут экзамен по IBM WebSphere Business Modeler в универе сдавали, там можно построить бизнес-процесс с помощью блоков, мышкой, а дальше автоматически сгенерировать Java или C++ классы. С полным покрытием по RUP. Только тссс :)
Кхм, это был сарказм?
Генерация кода — это генерация кода. Это не программирование. Это перевод с одного языка (диаграмм) на другой — Java/C++. Работа программиста состоит не в этом.
Когда появился компилятор C, который мог генерировать код в машинных кодах из высокоуровневого кода на C — программисты же не потеряли работу. Часть начала писать на C, часть — продолжила писать на ассемблере те критические участки, которые компилятор генерирует неоптимально, часть — стала разрабатывать компилятор.
Точно также может быть когда-то большая часть ПО будет разрабатываться на языках более высокого уровня, чем C++, но программисты всё равно будут нужны.
Генерация кода — это генерация кода. Это не программирование. Это перевод с одного языка (диаграмм) на другой — Java/C++. Работа программиста состоит не в этом.
Когда появился компилятор C, который мог генерировать код в машинных кодах из высокоуровневого кода на C — программисты же не потеряли работу. Часть начала писать на C, часть — продолжила писать на ассемблере те критические участки, которые компилятор генерирует неоптимально, часть — стала разрабатывать компилятор.
Точно также может быть когда-то большая часть ПО будет разрабатываться на языках более высокого уровня, чем C++, но программисты всё равно будут нужны.
Доказательство станет доказательством, когда признают его правоту. Пока же это «возможное доказательство».
Окей, пусть это пока «возможное доказательство». Автор опубликовал возможное доказательство. Где парадокс?
Ну ок. Тогда это «доказательство Шредингера» (по аналогии с котом): пока кто-то не докажет или не опровергнет его, неизвестно, доказательство это или нет. При желании подобную ситуацию можно назвать «парадоксом».
При желании все что угодно можно назвать парадоксом. Об этом и речь, что желание называть парадоксом очевидные вещи несколько обескураживает
это как заявить, что привидения существуют на самом деле и являются следствием влияния моноцентрических пси-барионных полей на Галардов центр височной доли мозга и привести 500 страниц расчетов и графиков. Но что такое моноцентрические барионные поля и Галардов центр, никто кроме автора утверждения не знает, а он сознаваться не хочет. Это не значит, что это его выдумка, т.к. он вполне может быть и прав, пока не доказано обратное, но и прямым доказательством это считать нельзя
Ненене, не совсем. Исправлю сравнение: автор написал, что такое моноцентрические барионные поля, но в другой книжке на 700 страниц. А что такое галардов центр он объясняет еще в одной книжке на 900 страниц. Причем в этих книжках есть понятия, которые описаны еще в каких-то книжках. И т.д. И даже самые-самые первые и основные из этих книжек способны понять человек 100 в мире, специалисты именно в данной области математики.
Вот на что это больше похоже.
Для сравнения — когда проверяли труды Уйалса ( те, которые доказали теорему Ферма ), специально наняли 7 математиков, которые около 2х лет только этим и занимались — тщательно изучали его доказательство, строчка за строчкой. И Уайлс активно помогал, они ему постоянно звонили зайдя в тупик, и он разъяснял непонятные моменты, а перед этим, конечно, обрисовал общую картину.
А вот японец для своей, еще более сложной работы, этого делать не хочет — надеюсь, пока.
Вот на что это больше похоже.
Для сравнения — когда проверяли труды Уйалса ( те, которые доказали теорему Ферма ), специально наняли 7 математиков, которые около 2х лет только этим и занимались — тщательно изучали его доказательство, строчка за строчкой. И Уайлс активно помогал, они ему постоянно звонили зайдя в тупик, и он разъяснял непонятные моменты, а перед этим, конечно, обрисовал общую картину.
А вот японец для своей, еще более сложной работы, этого делать не хочет — надеюсь, пока.
Судя по описанию, он вполне может оказаться одним из тех гениев, которым до лампочки общественное признание. Доказал, понял сам, а остальное его не касается. Надеюсь, что это не так.
Вместо того, чтобы тратить время на объяснение, он может ещё что-нибудь глобальное доказать. Время гения слишком ценно, а жизнь коротка. Ну, а потомки за 100 лет потом разберутся, что к чему.
Без популяризации это время будет потрачено впустую. Через n-лет кто-то также решит эту проблему и его доказательство будет более понятным или же этот кто-то просто поможет остальным его понять. И уже на основе его работы будут основыватся другие. А эта останется занятным казусом, если не будет просто забыта.
Знания и опыт — величайшие сокровища человечества. Но если уникальное знание будет только у человека-двух — скорее всего, оно будет утеряно.
Знания и опыт — величайшие сокровища человечества. Но если уникальное знание будет только у человека-двух — скорее всего, оно будет утеряно.
Иногда сам путь доказательства бывает не менее ценнее самой гипотезы.
Даже если взять этот пример, то для того, чтобы доказать abc-гипотезу были изобретены совершенно новые математические инструменты, которые сами по себе уже являются открытием и которые могут быть полезны в других областях математики. Поэтому было бы необдуманно называть объяснение решения гипотезы бесполезным решением. Хотя, автор сам решает, как поступать.
Даже если взять этот пример, то для того, чтобы доказать abc-гипотезу были изобретены совершенно новые математические инструменты, которые сами по себе уже являются открытием и которые могут быть полезны в других областях математики. Поэтому было бы необдуманно называть объяснение решения гипотезы бесполезным решением. Хотя, автор сам решает, как поступать.
это, простите, пока что пустое бахвальство. Он пока не гений, а человек, написавший 1000 никому непонятных страниц.
Нет ничего хорошего и похвального в том, что бы отмалчиваться и стоять в стороне от сообщества.
Нет ничего хорошего и похвального в том, что бы отмалчиваться и стоять в стороне от сообщества.
Причем все эти книжки написал он сам. Если посмотреть списки литературы приведенных четырех статей Мотидзуки, то там большую половину составляют другие опубликованные в журналах работы автора, обладающие гигантским объемом, иной раз за 100 страниц.
Это действительно огромный труд для сообщества — верифицировать суммарно порядка 1000 страниц содержательного текста, находящегося в сложной взаимосвязанности.
Нельзя сказать, что вызов необорим — скажем, классификация конечных простых групп — куда более объемный результат. Однако, подозреваю, классификацию было легче разбить на составные кирпичики и проверять по отдельности; она создавалась множеством ученых в течении нескольких десятилетий.
Это действительно огромный труд для сообщества — верифицировать суммарно порядка 1000 страниц содержательного текста, находящегося в сложной взаимосвязанности.
Нельзя сказать, что вызов необорим — скажем, классификация конечных простых групп — куда более объемный результат. Однако, подозреваю, классификацию было легче разбить на составные кирпичики и проверять по отдельности; она создавалась множеством ученых в течении нескольких десятилетий.
Доказательство предоставлено и лежит в открытом доступе, но сообщество не может его понять, вследствие чего не может уверенно сказать — правильно оно или нет.
По-моему, Мотидзуки мыслит совершенно иными образами, недоступными для нашего понимания.
По-моему, Мотидзуки мыслит совершенно иными образами, недоступными для нашего понимания.
Ким симпатизирует разочарованным коллегам, но предлагает другое объяснение обиды: «Читать чужие работы очень мучительно. И всё… Мы просто слишком ленивы, чтобы читать их».
по моему тут гораздо ближе к истине. я помню как разбирал 10 страниц чужого кода на асме без комментариев. я ясно представляю задачу разобрать таких 1000 страниц…
по моему тут гораздо ближе к истине. я помню как разбирал 10 страниц чужого кода на асме без комментариев. я ясно представляю задачу разобрать таких 1000 страниц…
Мне кажется, многие не дочитали даже этот пост на хабре :)
не знаю… мне от чего-то хочется верить в лучшее, в том числе и в мыслительные способности человека и в самодисциплину. Не верю я что кроме Мотидзуки ни кто этот труд не осилит и не превзойдет.
Печаль только от того, что это не я и не сейчас :)
Печаль только от того, что это не я и не сейчас :)
да, почти то же самое ))
По количеству минусов и плюсов у соответствующих комментариев я уже понял, что хабрасообщество устраивает такая псевдологика. Пусть будет парадокс, я уже отказался от спора (но не от своей точки зрения).
тебе подарили машину но колеса в коробке, угадай ?: не шреденгера машину ли тебе подарили ?!
блин, ребят ну что за бред, 99% не выпендриваясь согласитесь — мы никогда не узнаем чем закончится эта история. зачем мозг рвать?
плюсани засранец если ты в оставшемся проценте!
блин, ребят ну что за бред, 99% не выпендриваясь согласитесь — мы никогда не узнаем чем закончится эта история. зачем мозг рвать?
плюсани засранец если ты в оставшемся проценте!
Оно не может использоваться как инструмент для «исследования неизвестного», говоря выражением из данной статьи.
Считайте, что сумрачный японский гений изобрел ракету и выложил её чертежи в открытый доступ — но никто не может разобраться в схеме и построить её (либо на её основе сделать что-то попроще). И сам изобретатель не желает в этом помочь.
А пока не разобрались в особенностях схемы — нельзя сказать: а взлетит ли она?
Считайте, что сумрачный японский гений изобрел ракету и выложил её чертежи в открытый доступ — но никто не может разобраться в схеме и построить её (либо на её основе сделать что-то попроще). И сам изобретатель не желает в этом помочь.
А пока не разобрались в особенностях схемы — нельзя сказать: а взлетит ли она?
О, а вот тут уже начинается серьёзная философия. Есть доказательство-статья, а есть доказательство-идея. Статья существует, но её идея ещё не признана, и пока этого не случится получается глупая ситуация: у нас есть супер-пупер важная гипотеза, доказательство которой автоматом раскрывает не только Великую теорему Ферма, но и гипотезу Шпиро, частично гипотезу Войта, не говоря уже просто о серьёзном сдвиге в понимании чисел. Но при этом все воротят нос и говорят, что оно слишком сложное и им нужна помощь.
Суть статьи весьма понятна. Непонятно только где парадокс.
Дом построен, но не сдан госкомиссии. Дом есть, но его одновременно нет. Парадокс!
Дом построен, но не сдан госкомиссии. Дом есть, но его одновременно нет. Парадокс!
Кроме парадокса как логического противоречия есть парадокс в смысле парадоксальная ситуация, но было бы неуклюже делать заголовок «Парадоксальная ситуация вокруг доказательства, которое очень-очень важное, но непонятно написано, и никто его не признаёт». В вашем примере парадоксальным было бы то, что дом есть, а жить в нём нельзя.
видимо, я слишком требователен к употреблению слов типа «парадокс», «эпицентр» и т.п. Когда их применяют для повышения эмоциональной окраски, пренебрегая их точным значениям. Пусть будет парадокс…
Ну хватит. Что значит «пренебрегая точными значениями»? Слово «парадокс» имеет два значения, и оба из них с точки зрения лингвистики одинаково точные. Только одно значения из области логики, а другое из обыденной речи. И вот именно это, второе значение, вы почему-то в упор не признаёте.
Может быть вы дадите себе труд (небольшой) прочитать то что написано по вашей ссылке и чуть больший труд подумать. Мне сложно представить, что для такого в целом общества как здесь непроверенность доказательства является парадоксом. Еще «парадоксы»:
Спроектировали машину, но еще не успели наладить производтство. Машина есть, но ее нет. Парадокс!
Код написан, но не запущен, не протестирован и не проверен. Программа есть, но ее нет. Парадокс!
Телевизор стоит в комнате, но выключен. Изображение есть, но его нет. Парадокс!
У меня за спиной стоит холодильник. Я его не вижу. Он есть, но его нет. Парадокс!
Доказательство написано, но еще не проверено. Его есть, но его нет. Парадокс!
Спроектировали машину, но еще не успели наладить производтство. Машина есть, но ее нет. Парадокс!
Код написан, но не запущен, не протестирован и не проверен. Программа есть, но ее нет. Парадокс!
Телевизор стоит в комнате, но выключен. Изображение есть, но его нет. Парадокс!
У меня за спиной стоит холодильник. Я его не вижу. Он есть, но его нет. Парадокс!
Доказательство написано, но еще не проверено. Его есть, но его нет. Парадокс!
То, что вам сложно представить одно из значений слова «парадокс» не отменяет того, что это самое значение существует и является абсолютно корректным.
Вы упрекнули мне в том, что я якобы не прочитал словарную статью, на которую дал ссылку. У меня сложилось такое же мнение относительно вас.
Итак, читаем статью: «Заимствование из французского, где paradoxe восходит к греческому paradoxos, состоящему из двух основ para – „против“, doxos – „слава“. Буквальное значение „против того, что принято, устоялось“. Запомнили.
Да именно так. Наличие доказательства, которое написано, но которое никто не может проверить — это „против того, что принято, устоялось“, так как обычно не составляет труда проверить написанное доказательство.
Вот ещё в тему статья с вики: Парадокс (значения).
Вы упрекнули мне в том, что я якобы не прочитал словарную статью, на которую дал ссылку. У меня сложилось такое же мнение относительно вас.
Итак, читаем статью: «Заимствование из французского, где paradoxe восходит к греческому paradoxos, состоящему из двух основ para – „против“, doxos – „слава“. Буквальное значение „против того, что принято, устоялось“. Запомнили.
Доказательство написано, но еще не проверено. Его есть, но его нет. Парадокс!
Да именно так. Наличие доказательства, которое написано, но которое никто не может проверить — это „против того, что принято, устоялось“, так как обычно не составляет труда проверить написанное доказательство.
Вот ещё в тему статья с вики: Парадокс (значения).
Удивительно! но комментарий не существует, пока я его не отправлю. Вроде бы комментарий есть, но его нет. Парадокс :) кругом одни парадоксы :)
Действительно, это очень-очень удивительно, что пока научная работа не проверена научным сообществом и им не «одобрена», то пользоваться этой работой можно на свой страх и риск. Удивительные очевидные парадоксы!
Еще раз повторю: есть два «состояния» доказательства:
1. Оно написано, но не проверено
2. Оно написано и уже проверено
Нет никакого парадокса в существовании этих двух состояний. Что такое проверка доказательства? Это принятие его как «достоверного» внутри научного (а позже — и за его пределами) сообщества. Это такой же необходимый шаг, как нажатие кнопки «Написать» под формой комментария. Если я не нажму кнопку «Написать», то этот комментарий продолжит свое существование, но не сохранится в базу данных хабра, и пропадет вместе с закрытием моего браузера. Но не надо делать из этого парадокс!
Знаете что меня удивляет больше всего? То что члены сообщества добровольно записывают себя в число недалёких людей, которыми вобще-то не являются. Парадокс существует только для тех, кто не может постичь причины возникновения этого парадокса. Вам же не кажется парадоксальным отражение в зеркале? Вы там есть, но вас там нет. Потому что вы понимаете природу того, что видите. Точно так же и с этим доказательством: оно существует, оно написано на 512 страницах. Но оно пока не может считаться признанным, и если кто-то решит использовать его выводы, то должен будет просто поверить, что оно правильное и укладывается в те аксиомы, на которые оно опиралось. Но это же, ёмаё, элементарные вещи, доступные даже первокласснику! Какой еще парадокс вы здесь узрели?
Действительно, это очень-очень удивительно, что пока научная работа не проверена научным сообществом и им не «одобрена», то пользоваться этой работой можно на свой страх и риск. Удивительные очевидные парадоксы!
Еще раз повторю: есть два «состояния» доказательства:
1. Оно написано, но не проверено
2. Оно написано и уже проверено
Нет никакого парадокса в существовании этих двух состояний. Что такое проверка доказательства? Это принятие его как «достоверного» внутри научного (а позже — и за его пределами) сообщества. Это такой же необходимый шаг, как нажатие кнопки «Написать» под формой комментария. Если я не нажму кнопку «Написать», то этот комментарий продолжит свое существование, но не сохранится в базу данных хабра, и пропадет вместе с закрытием моего браузера. Но не надо делать из этого парадокс!
Знаете что меня удивляет больше всего? То что члены сообщества добровольно записывают себя в число недалёких людей, которыми вобще-то не являются. Парадокс существует только для тех, кто не может постичь причины возникновения этого парадокса. Вам же не кажется парадоксальным отражение в зеркале? Вы там есть, но вас там нет. Потому что вы понимаете природу того, что видите. Точно так же и с этим доказательством: оно существует, оно написано на 512 страницах. Но оно пока не может считаться признанным, и если кто-то решит использовать его выводы, то должен будет просто поверить, что оно правильное и укладывается в те аксиомы, на которые оно опиралось. Но это же, ёмаё, элементарные вещи, доступные даже первокласснику! Какой еще парадокс вы здесь узрели?
Эти файлы станут доказательством только после того, как их правильность подтвердит научное сообщество. Научное сообщество так же может сказать, что в доказательстве есть ошибка (и тогда доказательства не будет). Без такого решения это просто 500+ страниц математического текста, который может быть является доказательством.
Почти тот же кот Шредингера, только никто не может открыть «коробку», чтобы убедиться в одном из вариантов.
(do-безумный-бред «Кстати да. Может быть вообще, кот Шрёдингера — это одно из проявлений такого вот поведения. То есть, кот не то, чтобы в странном состоянии находится, просто у Вселенной, ограниченной коробкой и котом не хватает производительности, чтобы вывести то, в каком состоянии он должен находится? А потом приходит наблюдатель и добавляет вычислительной мощности и хопа, решение принимается»)
Мало что понял, но ясно, что за этим скрывается что-то потрясающее. Пролистав статьи, осознал свою ничтожность.
Отличный перевод. Получил настоящее наслаждение от прочтения.
Вот ещё хорошая короткометражка по теме: «Математик и черт»
Может Ферма тоже имел ввиду 4 статьи на 512 страниц, говоря «Я нашел этому поистине чудесное доказательство, но поля книги слишком узки для него.»?
Ферма жил давно, у него не было очень многих математических знаний, которые есть сейчас у почти каждого студента-математика. Так что не думаю, что у него было что-то подобное.
Читал когда-то, что Ферма имел в виду другую теорему. В его времена не было устоявшейся системы записи формул. И Ферма, как подтверждают другие его заметки, менял местами основание и показатель степени, по сравнению с привычными нам.
Теорема с перевернутыми основанием и показателями имеет место, и действительно легко доказывается.
К сожалению, я не нашел скана оригинальной рукописи Ферма. Но все же, склонен верить в ее самозарождение :)
Теорема с перевернутыми основанием и показателями имеет место, и действительно легко доказывается.
К сожалению, я не нашел скана оригинальной рукописи Ферма. Но все же, склонен верить в ее самозарождение :)
Теорема с перевернутыми основанием и показателями (n^x+n^y=n^z неразрешимо при n>=3) слишком легко доказывается чтобы доказательство не влезло на поля :)
Доказательство было слишком коротким, чтобы его можно было разглядеть на полях…
Любопытно. Заменой переменных a=z-x, b=y-x я свёл уравнение к n^a-n^b=1, но как обосновать, что любые степени числа n>2 отстоят друг от друга не менее, чем на 1?
Хотя тут решение проще. Для чётных n в левой части — чётное число,
для нечётных n=2k+1
в левой части — тоже чётное число: (2k+1)^a-(2k+1)^b раскрывая скобки по биному Ньютона, понятно что от каждой скобки нечётной останется только 1^a-1^b
Таким образом, слева всегда чётное, справа — единица.
для нечётных n=2k+1
в левой части — тоже чётное число: (2k+1)^a-(2k+1)^b раскрывая скобки по биному Ньютона, понятно что от каждой скобки нечётной останется только 1^a-1^b
Таким образом, слева всегда чётное, справа — единица.
Пардон за некропостинг, но почему «Для чётных n в левой части — чётное число»? Ведь четность числа определяется только для целых чисел, а так как
x, y, z могут быть отрицательными (по условию задачи они должны быть только целыми и ненулевыми), то в левой части уравнения будет получаться дробное число.Eсли b=0, то n^a=2, а этого не бывает (при n>2), а если a>b>0, то левая часть делится на n, а правая — нет.
А чем обусловлен выбор хаба «DIY или Сделай Сам»?
Когда читаю о таких случаях, всегда возникает вопрос: почему доказательства не формализуют? В компьютерном смысле слова. Чтобы доказательства писались не (не только) на естественном языке, а а на каком-то машинно-понимаемом (типа Coq). Ведь тогда по крайней мере вопрос о том «есть ли ошибка в доказательстве?» был бы снят, так как корректность доказательства могла бы понять машина. Проблема сложности доказательства, так же как проблема сложности кода, который пишут иные программисты — осталась бы, но это было бы хоть что-то. 95% доказательств можно было бы отсеять по причине их некорректности, и только корректные пришлось бы разбирать математическим сообществом.
Так почему же так не делают?
Принципиально невозможно? Думаю нет, уже доказанные вещи можно вполне заложить в верифицирующую систему как аксиомы. А ещё лучше перевести их доказательства на формальный язык.
Долго? Так ведь математик, как и программист, больше времени тратит на размышление, и рассмотрение ложных вариантов чем на написание финального доказательства. Поэтому имея уже готовое доказательство, формализовать его не составило бы труда.
Может быть по настоящему крутые математики слишком узко специализированы и неспособны пользоваться компьютером? Сомневаюсь.
Так почему же так не делают?
Принципиально невозможно? Думаю нет, уже доказанные вещи можно вполне заложить в верифицирующую систему как аксиомы. А ещё лучше перевести их доказательства на формальный язык.
Долго? Так ведь математик, как и программист, больше времени тратит на размышление, и рассмотрение ложных вариантов чем на написание финального доказательства. Поэтому имея уже готовое доказательство, формализовать его не составило бы труда.
Может быть по настоящему крутые математики слишком узко специализированы и неспособны пользоваться компьютером? Сомневаюсь.
Вы, видимо, не математик. Вы когда-нибудь читали сложные математические доказательства, хотя бы за второй курс математического факультета какого-нибудь нормального ВУЗа? Усилий на то, что Вы предложили, уйдет столько, что это просто не рентабельно.
Ну ВМК окончил, но математиком себя не считаю, скорее программистом.
Доказательства читал, и даже пытался понимать, и сам что-то доказывал. В итоге остался очень неудовлетворён каким-то «интуитивным» пониманием доказательств. Когда читаешь доказательство и теряешь способность проверить, верен ли переход, так как доказательство корректности перехода автору видится очевидным. А когда сам доказываешь — делаешь какой-то переход, а потом, внезапно, оказывается что он некорректен. Мне кажется с формальным языком такого бы не было.
С формальным языком Coq проходил туториал около месяца, доказывал простейшие теоремки (типа четности суммы двух нечетных чисел), но потом началась сессия и эту деятельность пришлось свернуть. Но всё-таки в чем проблема? Ведь как и в программировании можно какие-то частые переходы свернуть в заранее написанные процедуры и их применять. Декомпозиция же, повторное использование, разделяй и властвуй, разве в математике такое невозможно?
Доказательства читал, и даже пытался понимать, и сам что-то доказывал. В итоге остался очень неудовлетворён каким-то «интуитивным» пониманием доказательств. Когда читаешь доказательство и теряешь способность проверить, верен ли переход, так как доказательство корректности перехода автору видится очевидным. А когда сам доказываешь — делаешь какой-то переход, а потом, внезапно, оказывается что он некорректен. Мне кажется с формальным языком такого бы не было.
С формальным языком Coq проходил туториал около месяца, доказывал простейшие теоремки (типа четности суммы двух нечетных чисел), но потом началась сессия и эту деятельность пришлось свернуть. Но всё-таки в чем проблема? Ведь как и в программировании можно какие-то частые переходы свернуть в заранее написанные процедуры и их применять. Декомпозиция же, повторное использование, разделяй и властвуй, разве в математике такое невозможно?
Слишком много нужно сделать, чтобы реализовать требуемую программу. Проще научить медведя шнурки завязывать. К тому же, в некоторой аксиоматике может существовать утверждение, которое нельзя ни доказать, ни опровергнуть. Так что программа все равно будет несовершенна.
Я так и не смог осознать упомянутую ниже теорему Гёделя о неполноте, но может вы, как человек причастный к математике, разъясните на пальцах?
Утверждается что если формальная арифметика непротиворечива, то в ней существует невыводимая и неопровержимая формула.
Во-первых даже если она существует, то существует ли она среди практически полезных формул? Это ведь то же самое что говорить о бесполезности верификации программ, ссылаясь на неразрешимость проблемы останова, в то время как все практически полезные программы останавливаются.
Во-вторых если это действительно проблема, то как она решается в текущем подходе математики? Пишутся доказательства на неформальном языке? Но тогда каков критерий верности доказательства? Я могу посмотреть на него — и сказать «доказательство верно», другой посмотрит — и скажет «доказательство неверно», какой-то вопрос веры а не науки получается уже.
Утверждается что если формальная арифметика непротиворечива, то в ней существует невыводимая и неопровержимая формула.
Во-первых даже если она существует, то существует ли она среди практически полезных формул? Это ведь то же самое что говорить о бесполезности верификации программ, ссылаясь на неразрешимость проблемы останова, в то время как все практически полезные программы останавливаются.
Во-вторых если это действительно проблема, то как она решается в текущем подходе математики? Пишутся доказательства на неформальном языке? Но тогда каков критерий верности доказательства? Я могу посмотреть на него — и сказать «доказательство верно», другой посмотрит — и скажет «доказательство неверно», какой-то вопрос веры а не науки получается уже.
Тут все довольно сложно. Да, просто существуют в различных аксиоматиках недоказуемые и неопровергаемые утверждения. В большинстве случаев это не несет в себе каких-то проблем, ибо доказательства многих вещей строятся на уже проверенных математических аппаратах. Однако, имея эту теорему, уже нельзя утверждать что какую-то конкретную проблему можно точно решить. Повторюсь, это проявляется если глубоко копать. Например, математическая логика очень важна в понимании и создании искусственного интеллекта.
Как бороться? Никак. Теорема-то доказана.
Если непонятно. Найденное недоказуемое утверждение не будет выглядеть верным для одного человека и неверным для другого. Оно просто недоказуемо. Для всех.
Как бороться? Никак. Теорема-то доказана.
Если непонятно. Найденное недоказуемое утверждение не будет выглядеть верным для одного человека и неверным для другого. Оно просто недоказуемо. Для всех.
Ну в таком случае — если математика не имеет путей обхода теоремы о неполноте — то эта теорема совершенно ортогональна моему предложению формальной верификации. Потому что в этом плане формальная верификация новой проблемы не вносит, как были недоказуемые неопровергаемые теоремы, так и останутся.
«Существует общее заблуждение, согласно которому теорема Гёделя якобы утверждает существование „недоказуемых математических утверждений“ и областей „платонического мира“ математических истин, принципиально не доступных для нас. Это очень далеко от вывода, который мы должны сделать из теоремы Гёделя. В действительности Гёдель утверждает, что какие бы правила доказательства мы ни сформулировали заранее, предполодив их заслуживающими доверия (т.е. не способными привести нас к ложному заключению) и не слишком ограничетельными, мы в результате получим новый способ доступа к некоторым математическим истинам, которые невозможно вывести в рамках данных правил».
Пенроуз Р. Путь к реальности, или законы, управляющие Вселенной. Полный путеводитель (2007)
Насколько понятно из слов Пенроуза (далее по тексту книги), основная формулировка теоремы Гёделя сводится к следующему: существуют так называемые «истинные П1-высказывания», которые нельзя получить из правил некоторой формальной системы F (при этом система F предполагается заслуживающей доверия). Примерами таких высказываний может служить «последняя теорема Ферма» или бинарная проблема Гольдбаха (тернарная гипотеза Гольдбаха была доказана в этом году, в мае опубликовано доказательство), согласно которой любое чётное число большее 2, можно представить в виде суммы двух простых чисел.
Пенроуз Р. Путь к реальности, или законы, управляющие Вселенной. Полный путеводитель (2007)
Насколько понятно из слов Пенроуза (далее по тексту книги), основная формулировка теоремы Гёделя сводится к следующему: существуют так называемые «истинные П1-высказывания», которые нельзя получить из правил некоторой формальной системы F (при этом система F предполагается заслуживающей доверия). Примерами таких высказываний может служить «последняя теорема Ферма» или бинарная проблема Гольдбаха (тернарная гипотеза Гольдбаха была доказана в этом году, в мае опубликовано доказательство), согласно которой любое чётное число большее 2, можно представить в виде суммы двух простых чисел.
Простите, лолшто?
Во-первых, ВТФ уже много лет как доказана. Во-вторых, то, что проблема Гольдбаха не решена, не делает её нерешаемой.
Во-первых, ВТФ уже много лет как доказана. Во-вторых, то, что проблема Гольдбаха не решена, не делает её нерешаемой.
Где я сказал, что теорема Ферма не доказана? Где я сказал, что бинарная проблема Гольдбаха нерешаема?
А что вы здесь сказали, если не это?
существуют так называемые «истинные П1-высказывания», которые нельзя получить из правил некоторой формальной системы F (при этом система F предполагается заслуживающей доверия). Примерами таких высказываний может служить «последняя теорема Ферма» или бинарная проблема Гольдбаха.
Ну, во-первых, это слова Р. Пенроуза (совсем немного изменений, но суть 100% сохранена во всех смыслах). Во-вторых, то, что П1-высказывания нельзя получить из правил формальной системы F, заслуживающей доверия, не означает, что их нельзя доказать, но, мне кажется, это означает, что их не получится описать и доказать только на основе формального подхода (хотя здесь я могу быть не прав).
суть 100% сохранена во всех смыслах
Верится с большим трудом. Точнее, не верится вообще. Предположу, что Пенроуз писал, что ВТФ и проблема Гольдбаха могут оказаться недоказуемы.
Что значит «верится» или «не верится». Я же источник указал.
Во-первых, книга написана в 2007 г., а, следовательно, Пенроуз знал о том, что ВТФ доказана (собственно, он это и подтвердил).
Во-вторых, вот эта вырезка
Пенроуз Р. Путь к реальности, или законы, управляющие Вселенной. Полный путеводитель (2007)
Во-первых, книга написана в 2007 г., а, следовательно, Пенроуз знал о том, что ВТФ доказана (собственно, он это и подтвердил).
Во-вторых, вот эта вырезка
Пенроуз Р. Путь к реальности, или законы, управляющие Вселенной. Полный путеводитель (2007)
Не очень понятно, что он называет «истинными П1 высказываниями». Если, допустим, бинарная гипотеза Гольдбаха недоказуема, то она не является ни истинной, ни ложной. Она недоказуема — и только (хотя доказать её недоказуемость мы тоже не сможем).
Как из этого утверждения получить «новый способ доступа к некоторым математическим истинам», непонятно вообще. Либо ввести новые аксиомы (что математики делают регулярно), либо предложить «новую логику», но тогда у нас будет совсем другая математика :) Что, конечно, очень интересно само по себе.
Как из этого утверждения получить «новый способ доступа к некоторым математическим истинам», непонятно вообще. Либо ввести новые аксиомы (что математики делают регулярно), либо предложить «новую логику», но тогда у нас будет совсем другая математика :) Что, конечно, очень интересно само по себе.
Как я и предполагал, вы всё переврали. ВТФ приводится как пример П1-высказывания, но не как пример истинного недоказуемого П1-высказывания.
Итак, я сказал
Насколько понятно из слов Пенроуза (далее по тексту книги), основная формулировка теоремы Гёделя сводится к следующему: существуют так называемые «истинные П1-высказывания», которые нельзя получить из правил некоторой формальной системы F (при этом система F предполагается заслуживающей доверия). Примерами таких высказываний может служить «последняя теорема Ферма» или бинарная проблема Гольдбаха (тернарная гипотеза Гольдбаха была доказана в этом году, в мае опубликовано доказательство), согласно которой любое чётное число большее 2, можно представить в виде суммы двух простых чисел.Вы высказали предположения, что я утерял суть высказывание Пенроуза, которое я позднее привел в виде отрывка. Теперь вы явно утверждаете, что я утерял суть, пересказывая содержание данного отрывка. А теперь процитируйте, пожалуйста, фразу, в которой эта суть утеряна и не соответствует содержанию приведённого отрывка. Давайте разберёмся, кто здесь верблюд.
Верблюд вы, и я это докажу. Следите за руками. Ваша цитата:
Из неё следует, что ВТФ является примером истинного П1-высказывания, которое нельзя получить из правил системы F.
Цитата Пенроуза:
Из неё следует только то, что ВТФ является примером П1-высказывания, но Пенроуз не утверждает, что её нельзя вывести из F.
существуют так называемые «истинные П1-высказывания», которые нельзя получить из правил некоторой формальной системы F (при этом система F предполагается заслуживающей доверия). Примерами таких высказываний может служить «последняя теорема Ферма» или бинарная проблема Гольдбаха
Из неё следует, что ВТФ является примером истинного П1-высказывания, которое нельзя получить из правил системы F.
Цитата Пенроуза:
Другим ещё более известным примером может служить «последняя теорема Ферма», доказанная в конце ХХ века Эндрю Уайлзом. Ещё одной (пока не решённой) проблемой является известная «гипотеза Гольдбаха», согласно которой любое чётное число, большее 2, можно представить в виде суммы двух простых чисел. Утверждения такого рода специалисты по математической логике называют П1-высказываниями.
Из неё следует только то, что ВТФ является примером П1-высказывания, но Пенроуз не утверждает, что её нельзя вывести из F.
Тут одно из двух. Либо Пенроуз говорит, что тезис Чёрча-Тьюринга неверен, т.е. множество задач, которые могут быть решены человеком, шире, чем множество алгоритмически разрешимых задач, либо что-то очень странное:
Потому что «математические истины» в рамках какой-нибудь теории — это как раз то, что можно получить с помощью заданных правил доказательств (математической логики) из набора аксиом этой теории. Можно вводить новые аксиомы (и получится другая теория), но добавлять новые правила вывода (если они не следуют из известных) математика не позволяет.
какие бы правила доказательства мы ни сформулировали заранее, предположив их заслуживающими доверия (т.е. не способными привести нас к ложному заключению) и не слишком ограничительными, мы в результате получим новый способ доступа к некоторым математическим истинам, которые невозможно вывести в рамках данных правил
Потому что «математические истины» в рамках какой-нибудь теории — это как раз то, что можно получить с помощью заданных правил доказательств (математической логики) из набора аксиом этой теории. Можно вводить новые аксиомы (и получится другая теория), но добавлять новые правила вывода (если они не следуют из известных) математика не позволяет.
Ну. Вообще, Пенроуз активно не верит в то, что искусственный интеллект можно создать и объясняет это тем, что человек может решать алгоритмически неразрешимые задачи. У него даже две книги об этом есть.
Но в данном случае он говорит именно о том, что разные системы аксиом позволяют получать разные утверждения об одних и тех же объектах. Он потом там о геометриях различных рассуждает.
Но в данном случае он говорит именно о том, что разные системы аксиом позволяют получать разные утверждения об одних и тех же объектах. Он потом там о геометриях различных рассуждает.
Для понимания теоремы Гёделя очень советую прочесть книгу Д. Хофштадтера «Гёдель, Эшер, Бах — эта бесконечная гирлянда», там идея «странной петли», которая используется в доказательстве, пояснена на множестве простых примеров. Очень грубо и упрощенно теорему Гёделя о неполноте можно интерпретировать так: любой язык, достаточно мощный для того, чтобы быть собственным метаязыком (формальная арифметика — это язык именно такой мощности) либо не полон (содержит недоказуемые, т.е. не выводимые за конечное число шагов с помощью конечного числа правил вывода из конечного числа аксиом, истинные утверждения) либо противоречив (содержит доказательство как какой-либо гипотезы А, так и её отрицания not A).
Проблема именно в том, что язык становится для самого себя метаязыком, и на нем можно сформулировать автореферентную (ссылающуюся на саму себя) строчку вида G = «G — не теорема». Именно такая строчка и будет гёделевой для указанного языка. Парадоксальность утверждения «Это утверждение ложно» заметили еще древние греки, но его наличие не машает нам пользоваться естественным языком. Также и теорема Гёделя не сильно мешает использованию формальных систем.
Проблема именно в том, что язык становится для самого себя метаязыком, и на нем можно сформулировать автореферентную (ссылающуюся на саму себя) строчку вида G = «G — не теорема». Именно такая строчка и будет гёделевой для указанного языка. Парадоксальность утверждения «Это утверждение ложно» заметили еще древние греки, но его наличие не машает нам пользоваться естественным языком. Также и теорема Гёделя не сильно мешает использованию формальных систем.
Прекрасно, снимаю шляпу. Я хоть и знал что это, но так доступно и хорошо описать бы не смог.
а на мой взгляд, это очередной сепулькарий на заданную тему…
Можно пояснить лучше, если аналогия непонятна.
Пусть имеется формальная система Т, в которой можно выразить все утверждения формальной арифметики.
Если занумеровать каждую аксиому и каждое правило вывода, то сам процесс вывода какой либо теоремы (т.е. последовательного применения правил вывода к аксиомам и уже выведенным теоремам) можно рассматривать как манипуляцию с числами, т.е. сам вывод можно описать в терминах формальной арифметики.
Вот здесь и начинается проблема, т.к. можно построить автореферентное высказывание вида G = «G не выводима в формальной системе Т».
Если это высказывание выводимо, то его вывод является выводом не только G, но и высказывания not G = «G выводима в формальной системе Т», что делает формальную систему Т противоречивой. Если же вывод утверждения G не существует, то G — невыводимое в системе Т истинное утверждение (истинно оно потому, что оно утверждает свою невыводимость, и это действительно так), поэтому система Т — не полная.
На самом деле, теорему Гёделя можно доказывать не только построением «парадокса лжеца» в формальной системе, как это было сделано самим Гёделем, но и любым другим парадоксом, основанным на автореференции, например, парадоксом Берри.
Более того, существуют доказательства, не использующие автореференцию вообще, и основанные, к примеру, на теории вычислимости, но на пальцах я их пояснить уже не смогу.
Пусть имеется формальная система Т, в которой можно выразить все утверждения формальной арифметики.
Если занумеровать каждую аксиому и каждое правило вывода, то сам процесс вывода какой либо теоремы (т.е. последовательного применения правил вывода к аксиомам и уже выведенным теоремам) можно рассматривать как манипуляцию с числами, т.е. сам вывод можно описать в терминах формальной арифметики.
Вот здесь и начинается проблема, т.к. можно построить автореферентное высказывание вида G = «G не выводима в формальной системе Т».
Если это высказывание выводимо, то его вывод является выводом не только G, но и высказывания not G = «G выводима в формальной системе Т», что делает формальную систему Т противоречивой. Если же вывод утверждения G не существует, то G — невыводимое в системе Т истинное утверждение (истинно оно потому, что оно утверждает свою невыводимость, и это действительно так), поэтому система Т — не полная.
На самом деле, теорему Гёделя можно доказывать не только построением «парадокса лжеца» в формальной системе, как это было сделано самим Гёделем, но и любым другим парадоксом, основанным на автореференции, например, парадоксом Берри.
Более того, существуют доказательства, не использующие автореференцию вообще, и основанные, к примеру, на теории вычислимости, но на пальцах я их пояснить уже не смогу.
Лучше не стало.
Вы по-прежнему в объяснениях используете понятия, требующие пояснений, при закапывании в которые велик шанс прийти к началу объяснений или уйти в бесконечность. И пропускаете шаги, по принципу "Отсюда, очевидно, следует"… И ещё и ошибки при этом совершаете… (в частности, с чего вдруг утверждение про выводимость утверждения G отнесено к утверждениям в формальной арифметики?)
Мне больше вариант Клайна подходит. Он же в той книге, кстати, тоже пытался описать способ появления и доказательства теоремы Геделя через сведение утверждений к числам, но тоже пропустил как минимум пару важных для понимания шагов…
Вы по-прежнему в объяснениях используете понятия, требующие пояснений, при закапывании в которые велик шанс прийти к началу объяснений или уйти в бесконечность. И пропускаете шаги, по принципу "Отсюда, очевидно, следует"… И ещё и ошибки при этом совершаете… (в частности, с чего вдруг утверждение про выводимость утверждения G отнесено к утверждениям в формальной арифметики?)
Мне больше вариант Клайна подходит. Он же в той книге, кстати, тоже пытался описать способ появления и доказательства теоремы Геделя через сведение утверждений к числам, но тоже пропустил как минимум пару важных для понимания шагов…
Выводимость можно описать как отношение формальной арифметики, и если формальная система Т может выражать отношения формальной арифметики, то она может выражать и выводимость. Да, отношение «высказывание S выводимо в T» посложнее, чем a+b=c, но принципиальной разницы между ними нет.
Прошу вас, прочтите Хофштадтера, там он вводит формальную систему (названную им Топографческой Теорией Чисел), в которой все манипуляции в ходе доказательства теоремы Гёделя можно отследить, просто считая палочки на бумаге.
Очень трудно описать гёделизацию простыми словами, но в английской вики у сообщества почти получилось.
Если доказательства на словах вас не устраивают, можете отследить работу системы доказательства теорем Nqthm, которую использовал Шанкар для доказательства теоремы Гёделя еще в 1986 году.
Прошу вас, прочтите Хофштадтера, там он вводит формальную систему (названную им Топографческой Теорией Чисел), в которой все манипуляции в ходе доказательства теоремы Гёделя можно отследить, просто считая палочки на бумаге.
Очень трудно описать гёделизацию простыми словами, но в английской вики у сообщества почти получилось.
Если доказательства на словах вас не устраивают, можете отследить работу системы доказательства теорем Nqthm, которую использовал Шанкар для доказательства теоремы Гёделя еще в 1986 году.
существует ли она среди практически полезных формул?
Возможно, что среди тех утверждений (формул), которые недоказуемы по Геделю, сейчас нет «полезных», т.е. применимых в физике и пр. Но также возможно, что польза в будущем будет найдена, как нашлась польза от неевклидивой геометрии.
Вот, например, пишут про «Континуум-гипотезу»:
В 1963 г. П. Дж. Коэн из Станфордского университета, опираясь на работу Курта Гёделя и математиков из Института высших исследований, показал, что, хотя эта гипотеза не противоречит аксиомам общепринятой теории множеств, она вместе с тем и не следует из них.
Фактически роль континуум-гипотезы в теории множеств такая же, как роль евклидовского постулата параллельности в геометрии. При допущении истинности или ложности гипотезы континуума можно построить различные версии теории множеств точно так же, как при допущении истинности или ложности аксиомы параллельности можно строить евклидову или неевклидовы геометрии.
Думаю, данная цитата что-то может прояснить:
Морис Клайн «Математика. Утрата определенности.» Глава XIV, Куда идет математика?
… как показал Гёдель, в рамках наложенных Гильбертом ограничений любая достаточно мощная формальная система содержит неразрешимые утверждения, т.е. утверждения, которые, базируясь на аксиомах нельзя ни доказать, ни опровергнуть;
но это значит, что подобные утверждения (или их отрицания) можно принять в качестве дополнительных аксиом.
Однако и после присоединения новой аксиомы расширенная система, согласно теореме Гёделя, все еще должна содержать неразрешимые утверждения. Приняв их за новые дополнительные аксиомы, мы могли бы вторично расширить формальную систему и т.д.
Процесс последовательного расширения исходной формальной системы можно было бы продолжать бесконечно.
Логицисты, формалисты и представители теоретико-множественного направления полагаются на аксиоматические основания. В первые десятилетия XX в. именно аксиоматика превозносилась как наиболее подходящий фундамент для построения математики.
Но теорема Гёделя утверждает, что ни одна система аксиом не охватывает всех истин, содержащихся в любой математической структуре, а теорема Левенгейма — Сколема показывает, что каждая система аксиом включает больше, чем предполагалось.
Так уже куча таких программ реализована. Тут же нет задачи доказать, что высказывание на одном языке эквивалентно высказыванию на другом (точнее есть, но она не такая общая, как в верификации). Тут задача в том, чтобы машина проверила доказательство, которое человек описывает на специальном языке. Язык этот (исчисление конструкций), вроде, достаточно мощный. Машине надо лишь проверить только корректность каждого шага в доказательстве, а это достаточно просто, потому что, если она не может вывести какой-нибудь предикат, то она просто говорит пользователю: не могу проверить, дополни доказательство. Кроме того, эти proof-помощники позволяют утверждения объявлять аксиомами.
Кстати, японцы активно пытаются внедрять этот подход с формализацией доказательств. Я пару раз видел статьи, которые были просто программами для proof-помощника.
Кстати, японцы активно пытаются внедрять этот подход с формализацией доказательств. Я пару раз видел статьи, которые были просто программами для proof-помощника.
Мне кажется, что реализовать требуемую систему не слишком сложно. Сложно реализовать эту систему с поиском доказательства, но если математик нашел док-во, то занесение его в систему эквивалентно написанию программы на императивном языке по алгоритму. Формальная проверка каждого этапа должна быть не сложной (я не математик). Грубо говоря, есть аксиомы, они формализованы. Есть правила вывода, их тоже не слишком сложно формализовать. Есть теоремы, для каждой теоремы можно вручную указать цепочку вывода (еще раз, нам не нужен автоматический вывод). Для проверки просто придется перегнать все 1000+ страниц статей этого японца в код. Это бы не было проблемой, если бы он сразу писал код по мере получения результатов. Проблема в том, что нужна такая система, формальное доказательство работоспособности этой системы и внедрение этой системы в комьюнити.
Усилий на то, что Вы предложили, уйдет столько, что это просто не рентабельно.
Воеводский с вами не согласен
Любые доказательства строятся на допущениях (аксиомах), а аксиомы в каждой предметной области — свои. Каждая область сама себе решает, что считается истинным и не нуждающимся в доказательстве.
А вот тут тоже сложности не вижу.
Претендент на доказательство вводит «общепризнанные в данной области» аксиомы, а также утверждение теоремы в верифицирующую систему.
Далее система верифицирует тело доказательства.
Сообществу остается лишь проверить что «общепризнанные аксиомы» действительно общепризнаны, а также что утверждение теоремы им интересно. Тело же доказательства (которое внутри может содержать какие-то вспомогательные теоремы с их доказательствами) читать чтобы оценить его правильность — не надо.
Претендент на доказательство вводит «общепризнанные в данной области» аксиомы, а также утверждение теоремы в верифицирующую систему.
Далее система верифицирует тело доказательства.
Сообществу остается лишь проверить что «общепризнанные аксиомы» действительно общепризнаны, а также что утверждение теоремы им интересно. Тело же доказательства (которое внутри может содержать какие-то вспомогательные теоремы с их доказательствами) читать чтобы оценить его правильность — не надо.
Тогда как вам такой аргумент. Современные компьютеры не всегда хорошо работают с банальными дробями, не говоря уже о более сложных конструкциях. Для такой системы понадобился бы суперкомпьютер, который потом ещё непонятно как пришлось бы отлаживать. Существуют специализированные железки, которые работают с рациональными числами, но не на таком масштабе. Так что да, это наверняка возможно при достаточном понимании математики и развитии информатики, железа и ПО, но сложно.
Ещё раз напомню, что я не предлагаю компьютеру придумывать доказательство — это практически невозможно.
Я предлагаю ему лишь проверять доказательство — это мне кажется возможным и вычислительно не сложным. При условии что доказательство состоит из серии шагов, где каждое последующее утверждение практически очевидным образом следует из предыдущих. Для этого компьютеру даже не обязательно рассматривать всё доказательство целиком, достаточно рассматривать каждый логический переход по отдельности, всё очень локализовано.
Если математик при рассмотрении доказательства на бумаге не «работает» с рациональными числами, в том плане что не перемножает их численно и не складывает — то и компьютеру при проверке доказательства — не придется. Проверка же заключается в подстановке в теорему каких-то конкретных значений и проверке истинности доказательства для них, а в проверке правомерности общих логических переходов.
Я предлагаю ему лишь проверять доказательство — это мне кажется возможным и вычислительно не сложным. При условии что доказательство состоит из серии шагов, где каждое последующее утверждение практически очевидным образом следует из предыдущих. Для этого компьютеру даже не обязательно рассматривать всё доказательство целиком, достаточно рассматривать каждый логический переход по отдельности, всё очень локализовано.
Если математик при рассмотрении доказательства на бумаге не «работает» с рациональными числами, в том плане что не перемножает их численно и не складывает — то и компьютеру при проверке доказательства — не придется. Проверка же заключается в подстановке в теорему каких-то конкретных значений и проверке истинности доказательства для них, а в проверке правомерности общих логических переходов.
Боюсь что количество абстракций в математике настолько велико, что для того чтобы их формализовать и описать на машинно понятном языке потребуются настолько огромные затраты времени, труда, ресурсов, и в конечном итоге не факт что объема доступных на данный момент вычислительных мощностей хватит для того чтобы справится со всем этим массивом данных.
Как пример возьмите доказательство простейшей теоремы Пифагора, и задумайтесь о создание системы верификации ее доказательства, боюсь что количество сущностей с которым вам придется оперировать зашкалит за сотню.
Как пример возьмите доказательство простейшей теоремы Пифагора, и задумайтесь о создание системы верификации ее доказательства, боюсь что количество сущностей с которым вам придется оперировать зашкалит за сотню.
Вообще-то многие доказательства формализованы. perso.ens-lyon.fr/jeanmarie.madiot/coq100/ теоремы Пифагора тоже. А что до количества абстракций в математике… Это тоже проблема. Многие абстракции по сути описывают одно и то же.
Насколько я понял, это формализация теорем, а не их доказательств, и верификацию теоремы на предмет правильности лишь на основе этих строчек произвести не получится.
Там, вроде, есть доказательства в contrib/… исходников. Хотя, у меня не было времени разбираться с ними. Поэтому не знаю, закончены они или нет.
Это формализация, которая (в силу изоморфизма Карри-Говарда) является верификацией. Проверка доказательства — задача куда как более простая, чем оного доказательства поиск.
Проверка же заключается не в подстановке в теорему каких-то конкретных значенийкажется, вы «не» пропустили
> Современные компьютеры не всегда хорошо работают с банальными дробями
В каком смысле? В чем проблема?
В каком смысле? В чем проблема?
Ну попробуйте записать одну треть в переменную. Нельзя же просто взять и написать где-нибудь в коде: x = 1/3. Хранимое в памяти значение будет отличаться. Чтобы обойти это нужно использовать костыли, в то время как для человека такая операция вообще не представляет сложности.
Ну, например, http://ru.wikipedia.org/wiki/Символьные_вычисления. А ещё в лиспе по умолчанию есть тип рациональных чисел, который дроби хранит как дроби, а не в десятичной записи с округлением.
Prelude> import Data.Ratio
Prelude Data.Ratio> 1 % 3
1 % 3
Prelude Data.Ratio> 1 % 3 + 2 % 7
13 % 21
Prelude Data.Ratio>
Для человека операции с простыми дробями — это тоже своего рода костыль (а точнее надстройка над целочисленной арифметикой). Кстати, многие дети понимают суть простых дробей намного позже, чем овладевают умением совершать операции над ними.
Кстати, очень многие вещи не хранятся «просто в переменных», например те же строки, или переменные типа «датавремя». Для работы над ними надстроены в языках программирования соответствующие перегрузки операторов, встроенные функции, методы классов и т.д. Просто мы к этому привыкли и не замечаем.
Тоже самое и простыми дробями. Если нужно хранить дроби как дроби — с ними можно работать и строго математически, но для этого потребуется использовать не стандартные типы данных, а пользовательские структуры и для операций над этими структурами использовать специфические функции/методы.
Кстати, очень многие вещи не хранятся «просто в переменных», например те же строки, или переменные типа «датавремя». Для работы над ними надстроены в языках программирования соответствующие перегрузки операторов, встроенные функции, методы классов и т.д. Просто мы к этому привыкли и не замечаем.
Тоже самое и простыми дробями. Если нужно хранить дроби как дроби — с ними можно работать и строго математически, но для этого потребуется использовать не стандартные типы данных, а пользовательские структуры и для операций над этими структурами использовать специфические функции/методы.
Ну разумеется можно хранить каким нибудь хитрым образом, я не спорю. Но архитектура компьютеров изначально не предусматривала работы с дробями и прочими математическими конструкциями. Нет же такой машинной команды как вычисление корня или дифференцирование.
Вычисление корня — есть, но в мат. сопроцессоре. Но т.к. он давно уже является стандартным модулем процессора, можно считать, что такая машинная команда есть.
А вообще, если посмотреть, чем мы на компьютерах занимаемся, то не для чего из этого машинной команды нет. Не тем мы, значит, на компьютерах занимаемся, не для того они.
А вообще, если посмотреть, чем мы на компьютерах занимаемся, то не для чего из этого машинной команды нет. Не тем мы, значит, на компьютерах занимаемся, не для того они.
Называть дроби «банальными» — весьма смелый трюк.
Особенно в свете того, что запись дробей очень зависит от выбранной системы счисления, и они бывают бесконечными, и могут содержать любые виды чисел, позволяющих операцию деления.
Логика в этом отношении куда проще — она работает лишь с утверждениями. Булева алгебра на компьютерах реализована в полной мере.
Особенно в свете того, что запись дробей очень зависит от выбранной системы счисления, и они бывают бесконечными, и могут содержать любые виды чисел, позволяющих операцию деления.
Логика в этом отношении куда проще — она работает лишь с утверждениями. Булева алгебра на компьютерах реализована в полной мере.
Тоже задавался таким вопросом. Насколько я понял, вся классическая математика построена на теории множеств, а Coq — на теории типов. А это не одно и то же. Поправьте, если я не прав.
Я тоже слабо понимаю, на да — не одно и то же. Coq был лишь для примера. Ясно что если теория множеств формально описана, то и для неё можно написать (или уже написан) верификатор.
Насколько я понял, вся классическая математика построена на теории множеств, а Coq — на теории типов. А это не одно и то же.Это действительно не одно и то же, поскольку теории типов изоморфны исчислениям (изоморфизм Карри-Говарда), а не теории множеств. Впрочем, что происходит в исчислении (индуктивных) конструкций под капотом в Coq, я слабо представляю, так что разъяснение знатока не повредило бы.
Я вообще слабо понимаю в математике, но может причина в ней: ru.wikipedia.org/wiki/Теорема_Гёделя_о_неполноте?
Нет, точно не в ней. Грубо говоря, эта теорема говорит о том, что не все истинные утверждения доказуемы в формальной арифметике. Но если есть доказательство, то формализовать его можно.
Я и сам задавался вопросом, почему нельзя задать машинопонятный язык (вместо имеющегося «полуформального»). Похоже, что это не делается из-за возрастающей сложности, неудобства инструментов и имеющихся научных традиций. Механизмы (соответствующая логическая теория или в некоторых случаях даже прикладные программы) существуют, но, видимо, не столь удобны. К тому же для этого пришлось бы вносить огромное количество имеющейся информации в базы… Учитывая сложность подобной работы, вряд ли кто-то за нее возьмется, во всяком случае в ближайшее время.
Я и сам задавался вопросом, почему нельзя задать машинопонятный язык (вместо имеющегося «полуформального»). Похоже, что это не делается из-за возрастающей сложности, неудобства инструментов и имеющихся научных традиций. Механизмы (соответствующая логическая теория или в некоторых случаях даже прикладные программы) существуют, но, видимо, не столь удобны. К тому же для этого пришлось бы вносить огромное количество имеющейся информации в базы… Учитывая сложность подобной работы, вряд ли кто-то за нее возьмется, во всяком случае в ближайшее время.
Кстати, формализация похожего плана формально допустима и не только для математики (в примитивном случае можно воспользоваться хотя бы тем же исчислением/секвенциальным исчислением предикатов). Все это проваливается по вышеописанным причинам, но в теории такие штуки помогли бы решить проблему верификации, а так же устранили проблему «неоткрытого общественного знания», т.е. ситуации, когда известны утверждения «А влечет В» и «В влечет С», но неизвестно утверждение «А влечет С» (и прочие вариации на эту тему).
А можно поподробнее? Или хотя бы ссылки на это самое секвенциальное исчисление.
Без проблем, но мне кажется, что в математической логике существуют более подходящие инструменты, чем секвенциальное исчисление предикатов. Есть что-то на вики, но я не ручаюсь за качество материала.
На базовом уровне это рассматривается в любых учебниках по матлогике, вот например:
Ершов, Палютин — «математическая логика», изд. второе.
Эдельман — «матматическая логика»
На базовом уровне это рассматривается в любых учебниках по матлогике, вот например:
Ершов, Палютин — «математическая логика», изд. второе.
Эдельман — «матматическая логика»
Но у Эдельмана не очень наглядно представлен вопрос именно секвенций… Грубо говоря, с помощью них можно работать с предикатами синтаксически, а не семантически. У нас это входило в базовый курс матлогики в университете, поэтому затрудняюсь порекомендовать что-либо другое из литературы.
Более подходящие — это какие?
Логика высших порядков (например, логика второго порядка расширяет исчисление предикатов такими штуками, как работа кванторов с предикатами) и теория типов. Язык Coq, кстати, построен на частном случае лямбда-исчислений — на исчислении конструкций.
Но мои знания в них очень поверхностны и я понятия не имею, какой математический аппарат стоит за ними, потому не могу ничего порекомендовать из литературы.
Но мои знания в них очень поверхностны и я понятия не имею, какой математический аппарат стоит за ними, потому не могу ничего порекомендовать из литературы.
Мне всегда не нравилось, что на эту теорему указывают, когда не понимают сути происходящего. Но в данном контексте, мне кажется, вы очень точно указали на проблему.
Странное(но понимаемое и не разделяемое) желание алгоритмизировать процесс проверки доказательств теорем. Почему бы не пойти дальше и не алгоритмизировать проверку на «красоту» и «правильность» различных произведений искусства вроде картин, скульптур, стихотворений, музыки.
Не может иметь это смысла.
Не может иметь это смысла.
Хотелось бы пояснений. Чем принципиально плоха возможность автоматической проверки? Почему это не может иметь смысла?
В оценке произведений искусства неотделимо присутствует субъективная оценка, здесь же ее не может быть — доказательство может быть или верно, или нет. Доказательство может быть верным, для объектов искусства же подобный термин не определен. К тому же подобная проверка не исключает проверки человеком, для обучения просто необходимо разбираться в доказательствах и методах доказательств.
В оценке произведений искусства неотделимо присутствует субъективная оценка, здесь же ее не может быть — доказательство может быть или верно, или нет. Доказательство может быть верным, для объектов искусства же подобный термин не определен. К тому же подобная проверка не исключает проверки человеком, для обучения просто необходимо разбираться в доказательствах и методах доказательств.
Потому что задача сводится к построению системы, которая умеет думать. При оценке нового математического доказательства, нужно понимать применимость тех или иных математических методов или приемов, используемых в доказательстве, а не формальное наличие алгоритмических ошибок.
Я все равно не понимаю Вас. Причем здесь алгоритмические ошибки? Все методы, которые были использованы, будут ровно таким же образом формализованы (принципиальной разницы, кроме сложности исполнения, между имеющейся на сегодня формальной записью и подобной машинопонятной записью нет). Если метод неприменим, мы просто не получим необходимого логического следствия.
А кто знает какое следствие является логически необходимым? Простой пример: Есть факт A. Есть два метода(утверждения, аксиомы, приема, формулы и т.д. применимых для А): M1 и M2 (на самом деле сколь угодно). И вот автор применяя M1 к А получает следствие S1: S1 = M1(A). Аналогично S2=M2(A). Выбирая M1 и M2 можно получить взаимно противоречивые или просто разные следствия S1 и S2 при полностью формально правильном применении M1 и M2, что можно алгоритмически проверить. Но как алгоритмически проверить правильность выбора M1 или M2? Сколько методов не формализуй остается проблема правильности их выбора. Собственно это и есть самая большая проблема в оценке правильности математических доказательств.
Если у нас есть система, в которой можно из истинных утверждений формально вывести два взаимопротиворечивых утверждения, данная система называется противоречивой, и в ней можно формально доказать все что угодно. Противоречивые системы — плохие системы, нам не имеет смысла с ними работать.
Или Вы имели в виду проверку метода на корректность, т.е. проблему применимости? Здесь эта проблема выглядит несколько иначе, чем у машин Тьюринга. При введении метода необходимо изначально пояснить, на каких данных он работает, и обосновать, почему он работает, иначе данный метод применять мы не имеем права.
Или Вы имели в виду проверку метода на корректность, т.е. проблему применимости? Здесь эта проблема выглядит несколько иначе, чем у машин Тьюринга. При введении метода необходимо изначально пояснить, на каких данных он работает, и обосновать, почему он работает, иначе данный метод применять мы не имеем права.
При оценке нового математического доказательства, нужно понимать применимость тех или иных математических методов или приемов
Именно. Любая подобная программа будет работать с уже выбранными автором методами и пытаться искать «ошибки» в уже сформированном доказательстве. В общем случае, алгоритмически правильно обосновать правильность выбора каждого метода равносильно задаче автоматически доказывать произвольные математические утверждения, что равносильно созданию, даже не «искусственного», интеллекта.
Машина Тьюринга, строго говоря, это и есть математическое определение алгоритма. А доказательство произвольных суждений, в общем случаем, вряд ли алгоритмически реализуемая на настоящий момент, задача.
Любая подобная программа будет работать с уже выбранными автором методами и пытаться искать «ошибки» в уже сформированном доказательстве.
Для проверки доказательства нам ничего больше и не нужно. Вот только методы не «выбраны автором», а заранее предопределены математической логикой. И набором «общепризнанных» теорем (чтобы не пришлось доказывать всё с самых основ). Всё, что может автор — это сказать «берём такую-то теорему, подставляем вместо свободных переменных некоторые формулы — получаем новую теорему. Если её условие оказалось в списке доказанных утверждений, то и вывод можно поместить в тот же список».
В книге «Гедель, Эшер, Бах» приводится пример полностью формализованного доказательства одной из теорем. Правда, там доказывалась всего лишь коммутативность сложения. Доказательство заняло около трёх страниц.
Вот только методы не «выбраны автором», а заранее предопределены математической логикой.
Методы не могут быть заранее предопределены:) Существуют множества, в том числе и еще неизвестные, доказательств одних и тех же утверждений.
набором «общепризнанных» теорем
Все сводится к созданию этого «набора», но проблема в том, что этот набор по-определению уже будет неполон в силу искусственности своего происхождения.
приводится пример полностью формализованного доказательства одной из теорем
Речи о том, что формализовать существующие доказательства нельзя — не было. Речь о том, что в общем случае, алгоритмизировать доказательство произвольных суждений пока что невозможно, а соответственно любая работа в этом направлении пока что лишена смысла в силу.
Как раз речь изначально была не о доказательстве произвольных суждений, а о проверке доказательства.
А в чем разница?)
Программе не нужно создавать свое доказательство. Нужно лишь проверить уже заданное формально доказательство.
А в чем ценность, если «заданное формально доказательство» неверно? Ведь выбор неверных исходных данных, гипотез, приемов, следствий при логической непротиворечивости цепочки вывода даст недостоверный результат.
В возможности автоматической проверки, является ли оно верным. Все выбранные приемы и теоремы должны быть предварительно определены, ибо это математика.
Все выбранные приемы и теоремы должны быть предварительно определены, ибо это математика.
Не могут быть в принципе — ибо это математика. Если бы все они были бы определены — все существующие утверждения были бы уже доказаны или опровергнуты.
Неверно, значит неверно. И тогда вопрос с конкретным доказательством, приведённым этим конкретным математиком, можно закрыть. А можно попытаться всё-таки разобраться, чего он напридумывал, и как это называется в общепринятом языке.
Речь о том, что в общем случае, алгоритмизировать доказательство произвольных суждений пока что невозможно
С этим никто и не спорит. Но в нашем случае, цель — проверить уже написанное доказательство, в котором, если оно полное, все используемые теоремы доказаны, а все цепочки вывода — приведены в явном виде. И нам не нужно угадывать, какое бы следствие вывести из теоремы A — за нас это сделал автор. Надо только проверить, что он в этом выводе не ошибся.
Я так и не понял, что в вашем понимании значит «обосновать правильность выбора каждого метода».
Что есть «правильность выбора»? Мы имеет метод, для которого доказана работа на данных класса А. Если этот метод используем в теореме на данных не класса А, то он неприменим. Если на данных класса А, то он применим.
Если проверяемое доказательство уже задано в машину, мы всего лишь проверяем корректность всех логических переходов. Причем здесь произвольные суждения?
Что есть «правильность выбора»? Мы имеет метод, для которого доказана работа на данных класса А. Если этот метод используем в теореме на данных не класса А, то он неприменим. Если на данных класса А, то он применим.
Если проверяемое доказательство уже задано в машину, мы всего лишь проверяем корректность всех логических переходов. Причем здесь произвольные суждения?
что в вашем понимании значит «обосновать правильность выбора каждого метода»
То, что любое доказательство, это совокупность различных приемов. Вот пример: school14-v.ucoz.ru/publ/1-1-0-2
Возможно, существуют и другие. От выбора метода на любом этапе зависят дальнейшие результаты. Выбор правильного метода — дает правильные результаты. Неприменимого — недостоверные.
Мы имеет метод, для которого доказана работа на данных класса А. Если этот метод используем в теореме на данных не класса А, то он неприменим. Если на данных класса А, то он применим.
Метод M — неприменим в конкретном доказательстве утверждения, но для M — доказана работа на данных класса А.
Применение М в рассуждениях даст недостоверный результат.
Если проверяемое доказательство уже задано в машину, мы всего лишь проверяем корректность всех логических переходов. Причем здесь произвольные суждения?
Одна только «корректность всех логических переходов» не гарантирует достоверность доказательства.
Необходимы так же достоверность исходных данных и логическая обоснованность самих переходов.
Так Вы и не объяснили, что за «правильность метода».
Корректность и есть логическая обоснованность. У нас не могут появиться новые правила логических рассуждений, кроме определенных изначально и скомбинированных из них позднее.
«Достоверность исходных данных» — что есть в вашем понимании достоверность и причем тут она мне тоже неясно. Все используемые в теореме утверждения должны быть предварительно доказаны. Все методы — обоснованы. Доказательство — формализовано.
Работа математиков при проверке корректности работы в этом плане тоже совершенно техническая, не творческая. За сим я откланяюсь, мне неинтересно разбираться в вашей терминологии.
Корректность и есть логическая обоснованность. У нас не могут появиться новые правила логических рассуждений, кроме определенных изначально и скомбинированных из них позднее.
«Достоверность исходных данных» — что есть в вашем понимании достоверность и причем тут она мне тоже неясно. Все используемые в теореме утверждения должны быть предварительно доказаны. Все методы — обоснованы. Доказательство — формализовано.
Работа математиков при проверке корректности работы в этом плане тоже совершенно техническая, не творческая. За сим я откланяюсь, мне неинтересно разбираться в вашей терминологии.
Так вы и не объяснили, что за «правильность метода».
Так вы и не спрашивали и странно, что требуется пояснение. Имеется ввиду любой математический метод или прием, который в данной ситуации приведет построению в дальнейшем непротиворечивых суждений.
«Достоверность исходных данных» — что есть в вашем понимании достоверность и причем тут она мне тоже неясно.
Достоверность — самый обычный термин. В своем значении он и употребляется. Любые строгие утверждения могут строится исключительно на достоверных данных.
Все методы — обоснованы.
О чем и речь. Обоснование выбора метода — в этом вопросе задача не алгоритмическая в общем случае. И что делать с новыми методами без вмешательства человека совсем понятно. А если от обоснованность выбора метода является ключевым пунктом доказательства, то смысл существования такого «автоматизированного» средства совсем нивелируется.
мне неинтересно разбираться в вашей терминологии.
Терминология тут, право, не причем. Она самая обычная и разбираться в ней нет необходимости:)
Термин неприменим для той ситуации с точки зрения математики, потому и странный.
Про методы Вам уже ответили выше. И причем здесь новые методы? Почему без участия человека? Мы только проверяем уже имеющееся доказательство, это работа чисто техническая. Если Вы с этим не согласны, то у Вас проблемы с пониманием математики как таковой.
Скажем, если у нас есть обоснованный агорифм нахождения наибольшего общего делителя, на наутральных числах он будет работать для них всегда, в любом месте доказательства, в любое время дня и ночи, для любого человека. Его обоснование формируется в виде теоремы, доказательство которой проверяется аналогичным же образом.
Про методы Вам уже ответили выше. И причем здесь новые методы? Почему без участия человека? Мы только проверяем уже имеющееся доказательство, это работа чисто техническая. Если Вы с этим не согласны, то у Вас проблемы с пониманием математики как таковой.
Скажем, если у нас есть обоснованный агорифм нахождения наибольшего общего делителя, на наутральных числах он будет работать для них всегда, в любом месте доказательства, в любое время дня и ночи, для любого человека. Его обоснование формируется в виде теоремы, доказательство которой проверяется аналогичным же образом.
*под «Мы только проверяем уже имеющееся доказательство» я имел в виду данную ситуацию. Разумеется, у математиков есть и иные занятия.
проверяем уже имеющееся доказательство, это работа чисто техническая
Странное заявление, для человека, считающего, что у него нет «проблемы с пониманием математики как таковой».
Вам дают доказательство утверждения, построенное на своей новой уникальной математической теории. Приводят в рамках этой теории доказательство. Вы отдаете его своей чудо-программе и проверяете(еще непонятно как, т.к. надо ее не только правильно понять в итоге, но и прежде правильно формализовать для программы). Программа говорит — ОК (Errors — 0, Warnings — 14 567)
Доказательство утверждения в рамках теории успешное.
Теория и утверждение берется на вооружение научным сообществом. И вот в рамках углубленного последующего изучения и развития этой новой теории в ней обнаруживаются неустранимые противоречия или несостыковки с уже доказанными и проверенными теориями, которые приводят в итоге и пересмотру всех результатов.
На мой взгляд, текст такой программы должен быть предельно прост:
{
print(42)
}
Вы вообще занимались математикой?
Про введение новых теорий я ничего не говорил, предполагается использование классических теорий. Если формализация доказательства невозможна, то это не доказательство.
Далее, у нас две теории. Если имеется их взаимная противоречивость, то, очевидно, в рамках более глобальной теории, иначе терминология «противоречие с другими теориями» является бессмыслицей в математике (Вы же не будете утверждать, что геометрии Лобачевского и Эвклида противоречат друг другу? Это просто разные формальные системы).
Если глобальная теория оказалась противоречивой, то она либо не имеет отношения, скажем, к формальной арифметике (в ней противоречивость доказать невозможно), либо есть утверждения, которые на самом деле не были доказаны.
Про введение новых теорий я ничего не говорил, предполагается использование классических теорий. Если формализация доказательства невозможна, то это не доказательство.
Далее, у нас две теории. Если имеется их взаимная противоречивость, то, очевидно, в рамках более глобальной теории, иначе терминология «противоречие с другими теориями» является бессмыслицей в математике (Вы же не будете утверждать, что геометрии Лобачевского и Эвклида противоречат друг другу? Это просто разные формальные системы).
Если глобальная теория оказалась противоречивой, то она либо не имеет отношения, скажем, к формальной арифметике (в ней противоречивость доказать невозможно), либо есть утверждения, которые на самом деле не были доказаны.
Забыл, еще есть вариант, что базовая формализация теории была противоречивой. Противоречивые аксиомы, например.
Про введение новых теорий я ничего не говорил, предполагается использование классических теорий.
Вы и обратного не говорили. И каких это классических теорий предполагается и кем? Если разговор скатывается в какие-то частные случаи — не вижу смысла его поддерживать. Мне уже предлагали здесь «новую логику». С моей стороны выражение «в общем случае» было почти в каждом ответе.
Далее, у нас две теории.
Речь лишь об обнаружении ошибок, которые выясняются после развития и исследования изложенной теории и не фигурируют в доказательстве непосредственно. Не больше и не меньше.
Эти ошибки лежат за рамками доказательства теоремы.
Так о чем и речь.
Тогда в чем противоречие с моими словами?
Когда читаю о таких случаях, всегда возникает вопрос: почему доказательства не формализуют? В компьютерном смысле слова
Это оригинальный вопрос, на который я ответил, что не вижу в этом смысла.
И в частности потому, что в общем случае, там где подобные средства будут необходимы, очень вероятно, что
ошибки лежат за рамками доказательства теоремы.
Соотнося трудозатраты на разработку подобного продукта, его сложность, и практический выхлоп я до сих пор не услышал ни одного аргумента, чтобы поменять своего мнения:)
Вот теперь я услышал ответ на вопрос, хотя непонятно, зачем Вы изначально упомянули произведения искусства.
Банальная экономия времени и денег, тем более системы а-ля Coq уже существуют. В итоге станет выгоднее создать систему с достаточным функционалом, чем оплачивать труд рецензентов и терять время выдающихся математиков.
Банальная экономия времени и денег, тем более системы а-ля Coq уже существуют. В итоге станет выгоднее создать систему с достаточным функционалом, чем оплачивать труд рецензентов и терять время выдающихся математиков.
Вряд ли это в реальности возможно. Возможно, наличие такого инструмента сократило бы время на доказывание, скажем теоремы о классификации простых конечных групп.
Но ведь в науке не только важен результат. Но и сам путь к нему. Даже неверное доказательство может открыть пути для более выдающихся результатов.
На хабре понятно желание программистов автоматизировать все и вся. Но со временем и до них дойдет, что некоторые вещи лучше оставить как есть. Для математиков, в частности, уже существует достаточное количество нужных им инструментов. И самые ценные для них это все-таки листок бумаги и ручка.
Но ведь в науке не только важен результат. Но и сам путь к нему. Даже неверное доказательство может открыть пути для более выдающихся результатов.
На хабре понятно желание программистов автоматизировать все и вся. Но со временем и до них дойдет, что некоторые вещи лучше оставить как есть. Для математиков, в частности, уже существует достаточное количество нужных им инструментов. И самые ценные для них это все-таки листок бумаги и ручка.
Произвольный предикат M1(A), который ниоткуда не следует, означает введение новой аксиомы. С чего вдруг «вброшена» новая аксиома?
Вот как раз такие вещи и легко автоматически отследить, если доказательство описано формально. И, наоборот, при визуальном контроле легко пропустить утверждение, которое не следует из предыдущих и вообще из никакой математики.
Проблема для пишущих будет в том, что нельзя будет делать так.
Приходит Лившиц к Ландау и говорит:
— Лев Давыдович, я в трамвае 40 страниц выкладок потерял!
— Ничего, напишем «Откуда, очевидно, следует»
Вот как раз такие вещи и легко автоматически отследить, если доказательство описано формально. И, наоборот, при визуальном контроле легко пропустить утверждение, которое не следует из предыдущих и вообще из никакой математики.
Проблема для пишущих будет в том, что нельзя будет делать так.
Приходит Лившиц к Ландау и говорит:
— Лев Давыдович, я в трамвае 40 страниц выкладок потерял!
— Ничего, напишем «Откуда, очевидно, следует»
Вы неправильно интерпретировали запись M1(A). Это не предикат, в общем случае. Это некоторый способ или прием, который применяется к некоторому набору фактов А, чтобы получить другой набор фактов S1 (скорее некоторый набор предикатов). Одну и ту же теорему можно доказать множеством совершенно разных способов используя разные приемы. Результата это не меняет. Но выбрав неправильный прием, можно получить уже другой результат. Как алгоритмически в общем случае определять применимость использования того или иного приема совершенно непонятно. Более того, как оценивать применимость совершенно нового и неизвестного ранее математического приема или способа?
>Это некоторый способ или прием, который применяется к некоторому набору фактов А, чтобы получить другой набор фактов S1 (скорее некоторый набор предикатов).
Так ведь изучением способов получать одни суждения из других занимается логика.
(any (x) Металл (x) => Металлопроводен (x)) ^ Металл (Медь) => Металлопроводен(Медь)
Есть определенные правила, по которым из исходных суждений получаются результирующие, им и надо следовать, соответственно, можно записывать суждения формально и преобразовывать одно в другое.
Например
perso.ens-lyon.fr/jeanmarie.madiot/coq100/
nevidal.org/sad.ru.html
>Более того, как оценивать применимость совершенно нового и неизвестного ранее математического приема или способа?
Путем голосования, серьезно. Такой «новый способ» есть «новая логика». Ну а почему нет, если существующих логик недостаточно, надо предложить новую формальную систему, аргументировать ее новизну и применимость, ее оценит научный мир и далее можно использовать.
Так ведь изучением способов получать одни суждения из других занимается логика.
(any (x) Металл (x) => Металлопроводен (x)) ^ Металл (Медь) => Металлопроводен(Медь)
Есть определенные правила, по которым из исходных суждений получаются результирующие, им и надо следовать, соответственно, можно записывать суждения формально и преобразовывать одно в другое.
Например
perso.ens-lyon.fr/jeanmarie.madiot/coq100/
nevidal.org/sad.ru.html
>Более того, как оценивать применимость совершенно нового и неизвестного ранее математического приема или способа?
Путем голосования, серьезно. Такой «новый способ» есть «новая логика». Ну а почему нет, если существующих логик недостаточно, надо предложить новую формальную систему, аргументировать ее новизну и применимость, ее оценит научный мир и далее можно использовать.
ведь изучением способов получать одни суждения из других занимается логика
Получать одни суждения из других это не проблемная часть математических доказательств. Гораздо интересней оценить адекватность выбора исследуемой модели и соотношение всех значимых следствий, которые получаются после ее построения с уже существующими теориями. Вы можете придумать свою теорию. Доказать в ее рамках требуемое утверждение. Но потом выяснится, что ваша теория противоречит другим, уже доказанным и общепризнанным теориям и/или сама является противоречивой.
Ну а почему нет, если существующих логик недостаточно
Ну в качестве эксперимента можно делать все что угодно:) Я же про это ничего не могу сказать и не знаю как это соотносится с объективной реальностью:) Эли это строго детерминированный алгоритм — это круто.
>Получать одни суждения из других это не проблемная часть математических доказательств.
В данном случае проблема в оценке, верно ли проложена цепь к доказательству abc-гипотезы, исходит ли она везде из общепринятой аксиоматики, или же где-то неявно вброшены новые положения.
Автомат бы легко все это проверил, выявил бы начала логических цепочек, и нужно было бы только убедится, что эти исходные суждения общеприняты в качестве аксиом или доказаны где-то еще.
Вот саму цепь составить — это во многом искусство, конечно.
В данном случае проблема в оценке, верно ли проложена цепь к доказательству abc-гипотезы, исходит ли она везде из общепринятой аксиоматики, или же где-то неявно вброшены новые положения.
Автомат бы легко все это проверил, выявил бы начала логических цепочек, и нужно было бы только убедится, что эти исходные суждения общеприняты в качестве аксиом или доказаны где-то еще.
Вот саму цепь составить — это во многом искусство, конечно.
Не так. Задача «думать» (самостоятельно искать пути от аксиом к доказываемой теореме, причём так, что бы заняло меньше бесконечного количества времени) — слишком большая. Программу — формализацию доказательства теоремы можно снабдить хинтами, благодаря которому верификатор затратит небольшое количество времени. Расстановка таких хинтов — творческий процесс, проверка — чисто механический.
Для произведений искусства есть золотое сечение. На сколько я понимаю, оно должно присутствовать в изобразительных произведениях, скульптуре, архитектуре, музыке. Если его нет, то произведение искусства, скорее всего, отстойное. Т.е. это универсальная, объективная оценка.
Конечно есть и субъективная составляющая. Но она есть и в науке. Доказательство или какая-нибудь теория тоже может субъективно (не)нравиться.
Ещё есть какая-то смысловая или прагматичная составляющая. И произведение искусства, и научная теория могут быть гармоничными/правильными, но совершенно бессмысленными.
Вообще тема автоматической проверки, критериев истинности научного знания очень топтаная в философии науки:
Есть позитивисты, которые считают, что единственный критерий истинности — это опыт. Для них эта теорема — какая-то бессмыслица, оторванная от физической реальности.
Есть неопозитивисты, которые как-раз попробовали бы проверить истинность доказательства как предлагаете вы — в плоскости формального языка.
Есть постпозитивисты, которые уделяют большее внимание роли научного сообщества и т.п. Типа если никто не может опровергнуть доказательство, значит его можно пока считать истинным. Если его никто не хочет опровергать, то скорее всего это какой-то бред, который может и правильный, но никому не нужен. Как-то так :)
Конечно есть и субъективная составляющая. Но она есть и в науке. Доказательство или какая-нибудь теория тоже может субъективно (не)нравиться.
Ещё есть какая-то смысловая или прагматичная составляющая. И произведение искусства, и научная теория могут быть гармоничными/правильными, но совершенно бессмысленными.
Вообще тема автоматической проверки, критериев истинности научного знания очень топтаная в философии науки:
Есть позитивисты, которые считают, что единственный критерий истинности — это опыт. Для них эта теорема — какая-то бессмыслица, оторванная от физической реальности.
Есть неопозитивисты, которые как-раз попробовали бы проверить истинность доказательства как предлагаете вы — в плоскости формального языка.
Есть постпозитивисты, которые уделяют большее внимание роли научного сообщества и т.п. Типа если никто не может опровергнуть доказательство, значит его можно пока считать истинным. Если его никто не хочет опровергать, то скорее всего это какой-то бред, который может и правильный, но никому не нужен. Как-то так :)
Думаю, не делают, потому что пока такие доказательства — редкость, и в целом текущие доказательства можно «осилить». А так хорошо было бы принимать работы в чем-нибудь типа
nevidal.org/sad.ru.html
Если не хватает этой системы автоматизации дедукции, можно язык специальный разработать, на базе haskell :) И на нем писать вообще ВСЕ научные работы в естественных науках. Плюсы огромны — общая база знаний, поиск нужной работы, автоматическое построение доказательств, исключение плагиата и так далее.
А рецензентам-то насколько проще будет — сразу смотришь на вывод, который гарантированно обладает новизной и следует из посылок.
nevidal.org/sad.ru.html
Если не хватает этой системы автоматизации дедукции, можно язык специальный разработать, на базе haskell :) И на нем писать вообще ВСЕ научные работы в естественных науках. Плюсы огромны — общая база знаний, поиск нужной работы, автоматическое построение доказательств, исключение плагиата и так далее.
А рецензентам-то насколько проще будет — сразу смотришь на вывод, который гарантированно обладает новизной и следует из посылок.
Потому что доказательства математических теорем базируются на нашем умении представлять (фантазировать) множеста.
Компьютер не умеет выдумывать множества, и невозможно написать алгоритм, который может формализовать придумывание множеств.
Компьютер не умеет выдумывать множества, и невозможно написать алгоритм, который может формализовать придумывание множеств.
Некоторые множества можно перебирать и, таким образом, придумывать. К примеру, можно написать алгоритм придумывания элементов множества всех строк (или фраз, соответствующих определённой грамматике). Другое дело, что ресурсы ограничены.
Никто не предлагает сделать человеко-заменителя (ИР). Достаточно лишь механически проверить непротиворечивую выводимость каждого конкретного шага доказательства из фиксированного набора аксиом, неопределяемых понятий и правил вывода). Где нужно расставить хинты для выбора верификатором способов переборов, что бы верификация проходила в небольшое время.
Никто не предлагает сделать человеко-заменителя (ИР). Достаточно лишь механически проверить непротиворечивую выводимость каждого конкретного шага доказательства из фиксированного набора аксиом, неопределяемых понятий и правил вывода). Где нужно расставить хинты для выбора верификатором способов переборов, что бы верификация проходила в небольшое время.
Уже умеет lenta.ru/articles/2012/06/29/cats/
Я как-то не уловил связь между «отличает кошку от собаки» и «умеет придумывать множества».
Не отличает кошку от собаки, а на основе 10 миллионов случайных изображений из роликов на ютубе нейронная сеть сама выделила встречающиеся объекты на фотографиях, например кошек и стала отвечать на наличие данного объекта на фотографии. При этом фотографии с кошками никак не помечались при обучении.
То есть нейронная сеть выделила абстрактное множество кошек. Это безусловно еще очень примитивный результат, но уже показывает, что компьютеры фактически могут абстрагироваться.
То есть нейронная сеть выделила абстрактное множество кошек. Это безусловно еще очень примитивный результат, но уже показывает, что компьютеры фактически могут абстрагироваться.
Эээ. Вот хаусдорфоры пространства — абстрактные множества. А множество кошек — ещё какое конкретное.
Какое же оно конкретное, если каждая кошка обладает уникальным генотипом и фенотипом, а некоторые кошки вообще существуют только в рисованном виде?
Конкретный = существующий в реальном мире
Абстрактный = существующий только в нашем воображении.
У хаусдорфовых пространств нет ни фотографий, ни рисунков. Нет реального объекта, который можно назвать хаусдорфовым пространством. Нет даже базы примеров, из которых можно вывести классификацию пространств.
Абстрактный = существующий только в нашем воображении.
У хаусдорфовых пространств нет ни фотографий, ни рисунков. Нет реального объекта, который можно назвать хаусдорфовым пространством. Нет даже базы примеров, из которых можно вывести классификацию пространств.
Вы используете свой вариант определения абстрактного объекта не совпадающий с общепризнанным. Вполне может быть, что хаусдорфовы пространства являются намного более абстрактным понятием, чем кошка, но от этого понятие «кошка» не становится конкретным. Сама кошка как конкретный объект не существует, она лишь идеализированный абстрактный объект описывающий то, что мы привыкли понимать под кошками.
Более того, открытый вопрос, существует ли реальный объект, который можно назвать биологическим видом или это просто абстракция, потому что не всегда понятно как делить совокупность живых существ ведь генотип то у каждого живого существа свой.
Более того, открытый вопрос, существует ли реальный объект, который можно назвать биологическим видом или это просто абстракция, потому что не всегда понятно как делить совокупность живых существ ведь генотип то у каждого живого существа свой.
Я вот тоже не могу себе представить формального четкого и полного определения, что такое «кошка». Нейронные сети-то не с определениями и не с формальными критериями работают.
К слову естественно тестировали нейросеть не на тех же картинках, на каких ее тренировали.
Я тоже задумывался об этом. И даже решил, что хочу создать проект а-ля «математическая википедия». Где разные пользователи смогли бы формулировать свои гипотезы (узлы некоторой сети), а также размещать и редактировать доказательства, связывающие гипотезы с одной или несколькими стандартизованными аксиоматическими системами.
После гугления у меня возникло мнение, что страницы такой «википедии» должны быть написаны на симбиозе математического (декларативного) языка и языка императивных комментариев на около-естественном языке (на упрощенной разновидности английского). Что бы утверждения на математическом языке верифицировали не только конечные узлы-гипотезы, но и комментарии по конкретным фразам. Т.е. комментарии, в общем-то, должны быть избыточными для доказательства (но недостаточными для оного сами по себе), но благодаря ним должна сохраниться возможность ориентироваться в доказательствах.
Думаю, что если никто не займёт эту нишу, то в течение ближайших 5 лет я мог бы создать ризонер-верификатор подобного языка… Единственно, у меня сложилось впечатление, что профессиональным математикам это не интересно, соответственно, мне тем более тяжело выделить своё свободное время. Видел в сети только сборник доказательств на ML — этого мало.
После гугления у меня возникло мнение, что страницы такой «википедии» должны быть написаны на симбиозе математического (декларативного) языка и языка императивных комментариев на около-естественном языке (на упрощенной разновидности английского). Что бы утверждения на математическом языке верифицировали не только конечные узлы-гипотезы, но и комментарии по конкретным фразам. Т.е. комментарии, в общем-то, должны быть избыточными для доказательства (но недостаточными для оного сами по себе), но благодаря ним должна сохраниться возможность ориентироваться в доказательствах.
Думаю, что если никто не займёт эту нишу, то в течение ближайших 5 лет я мог бы создать ризонер-верификатор подобного языка… Единственно, у меня сложилось впечатление, что профессиональным математикам это не интересно, соответственно, мне тем более тяжело выделить своё свободное время. Видел в сети только сборник доказательств на ML — этого мало.
Почитайте про проект sciencewise.info Семантическая сеть на базе arxiv.org
Как раз семантическая википедия для научных статей. Написана на Django. Руководители проекта рускоязычные, если интересуетесь, то можете попробовать присоединиться.
Как раз семантическая википедия для научных статей. Написана на Django. Руководители проекта рускоязычные, если интересуетесь, то можете попробовать присоединиться.
Это, наверное, не совсем то… Это механизм генерации связей между понятиями (как я понял), а не способ формализации знаний. Или я ошибаюсь?
Я не сильно знаком с проектом. Я просто знаю людей, которые с ним работают. Так что точно вам не смогу сказать, но по моему вы правы, это именно связь между научными статьями и как следствие понятиями. Возможно на базе sciencewise.info можно было бы сделать и формализацию знаний, т.к. инструментов там много уже создано.
Я тоже хотел. Для начала хотел перенести в формальную систему те теоремы что изучал в университете, когда понял что к пятому курсу начал их забывать. Но потом руки так и не дошли.
«Просто перенести» довольно много начинали. Проблема в том, что формальные языки математических доказательств практически не читаемы — слишком формальны они по сравнению с естественным языком. На естественном языке (пусть и с кванторами и специальными обозначениями) — дохлый номер описывать. Так что нужно для начала придумать как описывать достаточно кратко, что бы человек мог понять, но не все детали расписывались — либо, как я написал, хотя бы придумывать, как аннотировать машинный язык доказательства понятным человеку языком, но так, что бы не нужно было думать: «а не придумал ли комментатор лишнего».
Ну тут мне кажется также как с программным кодом.
Достаточно понятным для читателя образом записывать утверждения (не переходы). Как и в доказательстве на естественном языке делаем цепочку утверждений, неявно подразумевая, что каждое следующее «очевидным образом следует», то есть не нужно доказывать каждую деталь. Отличие от доказательства на естественном языке лишь в том, для каждого следующего утверждения верификатор будет с помощью ограниченного по времени перебора пытаться доказать это следование. Если не сможет — извиняйте, значит не так уж очевидно следует и нужно более подробно расписать почему именно оно следует.
В том числе и кванторами можно, код всё-таки для человека а не для машины. Вот пример:
И проблема комментариев та же, что и в программном коде. Комментарии могут устаревать, и не соответствовать коду.
Верифицировать их мне честно говоря не кажется хорошей идеей.
Как и в программном коде, хочется обходиться минимумом комментариев, а просто разбивать теоремы на подтеоремы с говорящими именами. Следить чтобы доказательство каждой отдельной теоремы не было слишком длинным (иначе нужно выносить часть «кода» в отдельную теорему). Если какой-то участок совсем уж сложный, то можно к нему написать комментарий с основной идеей и какими-то интуитивными соображениями. Если «комментатор придумал лишнего» — то кто-то из читателей это обнаружит и исправит, также как это делается в программном коде. Отличие лишь в том, что в программном коде ситуацию когда в комментарии написано одно — а в коде другое — и код неправильно работает — обнаружить сложно (и то как-то живем с этим), а тут будет легко.
Ну и точно также, как в программировании кроме программного кода мы имеем всякую документацию, диаграммы, алгоритмы и тому подобные вещи, которые нужны не для компилятора, а для людей — так и в доказательствах можно дать на пару страниц интуитивные соображения, идеи, диаграммы и т.п., а ниже полный код на формальном языке. Кто поймёт идею по неформальному описанию — хорошо, кто не поймёт — пусть идёт разбираться в коде.
Достаточно понятным для читателя образом записывать утверждения (не переходы). Как и в доказательстве на естественном языке делаем цепочку утверждений, неявно подразумевая, что каждое следующее «очевидным образом следует», то есть не нужно доказывать каждую деталь. Отличие от доказательства на естественном языке лишь в том, для каждого следующего утверждения верификатор будет с помощью ограниченного по времени перебора пытаться доказать это следование. Если не сможет — извиняйте, значит не так уж очевидно следует и нужно более подробно расписать почему именно оно следует.
В том числе и кванторами можно, код всё-таки для человека а не для машины. Вот пример:
forall n m : nat, le n m -> le (S n) (S m)
И проблема комментариев та же, что и в программном коде. Комментарии могут устаревать, и не соответствовать коду.
Верифицировать их мне честно говоря не кажется хорошей идеей.
Как и в программном коде, хочется обходиться минимумом комментариев, а просто разбивать теоремы на подтеоремы с говорящими именами. Следить чтобы доказательство каждой отдельной теоремы не было слишком длинным (иначе нужно выносить часть «кода» в отдельную теорему). Если какой-то участок совсем уж сложный, то можно к нему написать комментарий с основной идеей и какими-то интуитивными соображениями. Если «комментатор придумал лишнего» — то кто-то из читателей это обнаружит и исправит, также как это делается в программном коде. Отличие лишь в том, что в программном коде ситуацию когда в комментарии написано одно — а в коде другое — и код неправильно работает — обнаружить сложно (и то как-то живем с этим), а тут будет легко.
Ну и точно также, как в программировании кроме программного кода мы имеем всякую документацию, диаграммы, алгоритмы и тому подобные вещи, которые нужны не для компилятора, а для людей — так и в доказательствах можно дать на пару страниц интуитивные соображения, идеи, диаграммы и т.п., а ниже полный код на формальном языке. Кто поймёт идею по неформальному описанию — хорошо, кто не поймёт — пусть идёт разбираться в коде.
Естественно, при прочих равных лучше разбить код на разные леммы. Но проблема в том, что в отличие от кода (реализующего игры, бизнес-процессы и т.п.), математика — очень абстрактная, часто не имеющая «физического смысла»… И работать с кодом, состоящим из «леммы1, леммы2,… леммы 4234, объединяющей леммы 42 и т.п.» — очень сложно.
Собственно, идея с комментариями пришла ко мне, когда я участвовал в холиварах: комментировать или нет. Во-первых, мне показалось, что код нужно комментировать так, что бы осветить аспекты программы, плохо выражаемые на данном языке. К примеру, блок из кучи императивных mov/jmp на ассемблере имеет смысл прокомментировать декларацией того, что этот код должен делать в предметной области (открывать файл, мигать светодиодиками и т.п.). Или, наоборот, код на прологе или лиспе часто имеет смысл прокомментировать: как конкретно обходится та или иная рекурсия на используемой платформе.
Во-вторых, в качестве решения устаревания кода мне пришла идея включить комментарии в сам язык — сделав таким образом гибридный императивно-декларативный язык. Т.е. комментарии могут быть значимым кодом — и, к примеру, если с учётом синонимов/фразеологизмов (устоявшихся языковых паттернов) комментарий соответствует коду на 50%, то пропускать этот код через интерпретатор без ошибки.
К слову, идея смеси декларативного языка с императивным не нова (только цели другие): к примеру, SQL`ем описать запросы к БД часто невозможно без того, что бы база не начала тупить, перебирая то, что не надо. Для того, что бы этого избежать любая вменяемая СУБД имеет механизм хинтов — позволяющих скорректировать план запросов для данного запроса. Получается, что декларативный SQL — это всего лишь человеко-понятный комментарий к программе, использующей глубокое знание деталей платформы (которая, в свою очередь использует SQL как основу).
Ещё никто не мешает там, где это удобно, использовать один язык, а в других местах — другой. Один императивный, другой декларативный (или какой-нибудь аспектный, не важно).
Собственно, идея с комментариями пришла ко мне, когда я участвовал в холиварах: комментировать или нет. Во-первых, мне показалось, что код нужно комментировать так, что бы осветить аспекты программы, плохо выражаемые на данном языке. К примеру, блок из кучи императивных mov/jmp на ассемблере имеет смысл прокомментировать декларацией того, что этот код должен делать в предметной области (открывать файл, мигать светодиодиками и т.п.). Или, наоборот, код на прологе или лиспе часто имеет смысл прокомментировать: как конкретно обходится та или иная рекурсия на используемой платформе.
Во-вторых, в качестве решения устаревания кода мне пришла идея включить комментарии в сам язык — сделав таким образом гибридный императивно-декларативный язык. Т.е. комментарии могут быть значимым кодом — и, к примеру, если с учётом синонимов/фразеологизмов (устоявшихся языковых паттернов) комментарий соответствует коду на 50%, то пропускать этот код через интерпретатор без ошибки.
К слову, идея смеси декларативного языка с императивным не нова (только цели другие): к примеру, SQL`ем описать запросы к БД часто невозможно без того, что бы база не начала тупить, перебирая то, что не надо. Для того, что бы этого избежать любая вменяемая СУБД имеет механизм хинтов — позволяющих скорректировать план запросов для данного запроса. Получается, что декларативный SQL — это всего лишь человеко-понятный комментарий к программе, использующей глубокое знание деталей платформы (которая, в свою очередь использует SQL как основу).
Ещё никто не мешает там, где это удобно, использовать один язык, а в других местах — другой. Один императивный, другой декларативный (или какой-нибудь аспектный, не важно).
> леммы1, леммы2,… леммы 4234, объединяющей леммы 42 и т.п.
Вопрос об именовании лемм выходит за рамки верификации. Ведь при текущем положении дел математики как-то ссылаются на леммы, приведенные несколькими страницами ранее, то есть дают им какие-то имена, пусть и численные.
> код нужно комментировать так, чтобы осветить аспекты программы, плохо выражаемые на данном языке
С этим согласен.
> Во-вторых, в качестве решения устаревания кода мне пришла идея включить комментарии в сам язык — сделав таким образом гибридный императивно-декларативный язык. Т.е. комментарии могут быть значимым кодом — и, к примеру, если с учётом синонимов/фразеологизмов (устоявшихся языковых паттернов) комментарий соответствует коду на 50%, то пропускать этот код через интерпретатор без ошибки.
Вот это уже не нравится. Рассуждения про 50% и т.п. вносят нестрогость в эту проверку. На мой взгляд либо верификатор умеет читать эти комментарии полноценно — тогда почему бы не выкинуть основной человеконепонятный код и не писать всё доказательство такими комментариями, либо не умеет (если комментарии добавляют интуитивного понимания, которого верификатор не имеет) — тогда смиримся что они только для людей.
> К слову, идея смеси декларативного языка с императивным не нова: к примеру, SQL`ем описать запросы к БД часто невозможно без того, что бы база не начала тупить, перебирая то, что не надо. Для того, что бы этого избежать любая вменяемая СУБД имеет механизм хинтов — позволяющих скорректировать план запросов для данного запроса. Получается, что декларативный SQL — это всего лишь человеко-понятный комментарий к программе, использующей глубокое знание деталей платформы (которая, в свою очередь использует SQL как основу).
Интересный пример. Но здесь это имеет смысл из-за скорости вычислений. В аналогичном случае в верификаторе ничего не мешает написать утверждение на языке высокого уровня, которое транслятор переведёт на язык низкого уровня, пусть и неэффективно, эффективность тут не нужна.
Может быть моё сомнение по поводу включения комментариев в язык можно сформулировать так: проверить соответствие между кодом и комментарием не проще чем сгенерировать код по комментарию.
Другое дело что можно писать.
То есть для человека утверждение3 действительно следует очевидным образом, но для верификатора в скобках это доказано более детально. Причем код в скобках можно от человека спрятать за ссылкой «подробнее». Но это уже непринципиальные детали, связанные с тем что верификатор маломощен. Иначе он мог бы (раз человеку очевидно) вывести то что написано в скобках самостоятельно методом перебора.
Вопрос об именовании лемм выходит за рамки верификации. Ведь при текущем положении дел математики как-то ссылаются на леммы, приведенные несколькими страницами ранее, то есть дают им какие-то имена, пусть и численные.
> код нужно комментировать так, чтобы осветить аспекты программы, плохо выражаемые на данном языке
С этим согласен.
> Во-вторых, в качестве решения устаревания кода мне пришла идея включить комментарии в сам язык — сделав таким образом гибридный императивно-декларативный язык. Т.е. комментарии могут быть значимым кодом — и, к примеру, если с учётом синонимов/фразеологизмов (устоявшихся языковых паттернов) комментарий соответствует коду на 50%, то пропускать этот код через интерпретатор без ошибки.
Вот это уже не нравится. Рассуждения про 50% и т.п. вносят нестрогость в эту проверку. На мой взгляд либо верификатор умеет читать эти комментарии полноценно — тогда почему бы не выкинуть основной человеконепонятный код и не писать всё доказательство такими комментариями, либо не умеет (если комментарии добавляют интуитивного понимания, которого верификатор не имеет) — тогда смиримся что они только для людей.
> К слову, идея смеси декларативного языка с императивным не нова: к примеру, SQL`ем описать запросы к БД часто невозможно без того, что бы база не начала тупить, перебирая то, что не надо. Для того, что бы этого избежать любая вменяемая СУБД имеет механизм хинтов — позволяющих скорректировать план запросов для данного запроса. Получается, что декларативный SQL — это всего лишь человеко-понятный комментарий к программе, использующей глубокое знание деталей платформы (которая, в свою очередь использует SQL как основу).
Интересный пример. Но здесь это имеет смысл из-за скорости вычислений. В аналогичном случае в верификаторе ничего не мешает написать утверждение на языке высокого уровня, которое транслятор переведёт на язык низкого уровня, пусть и неэффективно, эффективность тут не нужна.
Может быть моё сомнение по поводу включения комментариев в язык можно сформулировать так: проверить соответствие между кодом и комментарием не проще чем сгенерировать код по комментарию.
Другое дело что можно писать.
Утверждение1.
Утверждение2.
Отсюда очевидным образом следует утверждение3 (в скобках куча кода)
То есть для человека утверждение3 действительно следует очевидным образом, но для верификатора в скобках это доказано более детально. Причем код в скобках можно от человека спрятать за ссылкой «подробнее». Но это уже непринципиальные детали, связанные с тем что верификатор маломощен. Иначе он мог бы (раз человеку очевидно) вывести то что написано в скобках самостоятельно методом перебора.
Вообще-то этой проблемой занимается сейчас много людей, Воеводский, например, продвигает свою гомотопическую теорию типов homotopytypetheory.org/
Потому что настоящие открытия в математики могут вообще не вписываться в формальный язык, который вы придумаете.
Статьи не компьютерной программой были написаны? Судя по тому что математики не смогли в них разобраться, очень похоже.
Хотя в доказательстве Перельмана тоже разобрались единицы, и прятался он от коллег-математиков не хуже
Хотя в доказательстве Перельмана тоже разобрались единицы, и прятался он от коллег-математиков не хуже
Нет, просто тело в том, что во всём мире наберётся полсотни человек, которые разбираются в этой области математики. И у них, разумеется, есть свои проблемы, помимо чтения чужих архиважных доказательств. Может на следующей конференции они соберутся и наконец разберутся что к чему.
Статьи, написанные компьютерной программой, распознаются очень легко, если хоть чуть-чуть шарить в этой области.
Вроде ж об этом писали на хабре — Японский математик доказал АВС-гипотезу
Это похоже на тарабарщину не только для обывателя. Это было тарабарщиной и для математического сообщества.Это не вся правда. Дело в том, что среди приведенной литературы, Мотидзуки ссылается на свои собственные работы, т.е. кроме 500 страниц доказательства abc-гипотезы, нужно сначала освоить несколько сот страниц других его работ.
Если провести аналогию для программиста: это если бы он создал свой собственный язык программирования, нет скорее свою библиотеку, а за тем на ней разработал все остальное.
Если дальше развить эту аналогию, как пример для C/C++, человек разработал (пусть под себя) «другую» stdlib, далее используя ее доказал гипотезу — с его точки зрения единственно правильное решение, ведь стандартная stdlib не достаточно гибка, не удобна, да и вообще не позволяет ему развернуться как следует. Для понимающих, это как после java/c# и ко, пересесть ну например на erlang (не в обиду разработчикам java/c#).
Что абсолютно не понятно, с моей точки зрения, это нежелание всего «математического» мира, всех этих выдающихся «Перельманов», «Уайльсов» и т.д. «изучить» эту библиотеку, чтобы понять доказательство этой важнейшей гипотезы.
Другая аналогия — вот вы выложили в интернете крутющую библиотеку, которую заметим, вы писали в свое свободное время. Но она ну например для ada. И теперь все ее хотят, но для C++, и вам говорят — мы не понимаем как оно работает, а перепишите ка это для C++ и кроме того не используйте своих библиотек, а юзайте исключительно stdlib.
Мне все, что происходит с Мотидзуки и его доказательством, видится как то так.
Отличие в том, что в случае программирования можно проверить, работает ли библиотека — даже не заглядывая в код, просто запустив и пользуясь. А убедившись что код работает, можно уже портировать на другие языки если хочется.
А единственная ценность доказательства — это его «код» — потому что не разобравшись в нём нельзя быть уверенным что оно истинно, и пользоваться его утверждением. А раз так — пока доказательство никто не понимает — оно не несёт никакой ценности. И нет уверенности что если кто-то потратит кучу времени на разбор этого доказательства — не окажется что в нём ошибка и время потрачено зря.
А единственная ценность доказательства — это его «код» — потому что не разобравшись в нём нельзя быть уверенным что оно истинно, и пользоваться его утверждением. А раз так — пока доказательство никто не понимает — оно не несёт никакой ценности. И нет уверенности что если кто-то потратит кучу времени на разбор этого доказательства — не окажется что в нём ошибка и время потрачено зря.
Отличие в том, что в случае программирования можно проверить, работает ли библиотека — даже не заглядывая в код, просто запустив и пользуясь.
Можно копнуть дальше, изобретена не только библиотека но и архитектура железа, на котором все это вертится.
… пока доказательство никто не понимает — оно не несёт никакой ценности.Вот и вас логика какая-то потребительски однобокая.
А убедившись что код работает, можно уже портировать на другие языки если хочется.А если нет ады под рукой?
И нет уверенности что если кто-то потратит кучу времени на разбор этого доказательства — не окажется что в нём ошибка и время потрачено зря.Не зря, т.к. вы постигли мышление выдающегося математика (или выучили его библиотеку).
> Не зря, т.к. вы постигли мышление выдающегося математика (или выучили его библиотеку).
Эту будет иметь смысл только если математик действительно выдающийся (а не безумен), а также если те, кто будут разбирать его рукопись менее выдающиеся. Иначе их время можно было бы потратить с большей пользой.
Эту будет иметь смысл только если математик действительно выдающийся (а не безумен), а также если те, кто будут разбирать его рукопись менее выдающиеся. Иначе их время можно было бы потратить с большей пользой.
Согласен отчасти: с одной стороны, достаточно много его работ признаны математическим сообществом. Напомню мы говорим о человеке, ставшим в 23 года доктором, а в 33 профессором.
С другой стороны, для того что бы понять не безумен ли он, нужно понять его выкладки ..., а это имеет смысл только если он не безумен. Согласитесь, это замкнутый круг получается.
С другой стороны, для того что бы понять не безумен ли он, нужно понять его выкладки ..., а это имеет смысл только если он не безумен. Согласитесь, это замкнутый круг получается.
ага.
и предлагаемый софт даёт из него выход.
и предлагаемый софт даёт из него выход.
Какой простите софт? Где и кем предлагаемый?
простите. Тут: habrahabr.ru/post/183374/#comment_6378020
В математике такого порядка я скорее дилетант, чем профи. В программировании же, скорее наоборот. Тем не менее думается мне, что создать что-то предложеное там не является возможным, как минимум по нескольким причинам:
— количество абстракций просто гигантское;
— множество понятий просто нельзя формализовать, можно формализовать только например действия над этими понятиями либо только результат определенного действия;
— некоторые уже существующие доказательства (например доказательство от обратного) невероятно сложно описать какими либо абстракциями алгоритмически;
— еще сложнее представить его в такой абстрактной форме, что бы алгоритм софта (какой бы умный он не был) однозначно ответил да/нет/константа/множество и т.д. — иногда математика оперирует оценочными суждениями;
— все это вообще не реально, если мы имеем дело с экспандирующими абстракциями (что-нибудь вида произведения двух и более «матричных» или даже «бесконечных» абстракций);
Чтобы не быть голословным, пример:
Есть какая-то (неточная) мат. абстракция LA, которая может быть реализована только лямбдой (в программистском смысле). В доказательстве используется интеграл от этой лямбды или еще хуже произведение с другой мат. абстракцией LB, тоже представленой только лямбдой. Так вот, моей дилетантской математики достаточно чтобы представить в голове или на бумаге свойства такого интеграла или произведения. Но я как программист не имею ни малейшего понятия как представить результат алгоритмически — даже что это за конструкция (как должна быть формализована в программе) не представляю.
Я только за, если кто сможет ..., но пока помоему, без вариантов.
Для тех кто в танке, просьба не делать голословных заявлений, а описать алгоритмически ну например какую нибудь элементарную функцию (по Лиувилю) а потом применить эту абстракцию для доказательства ну например следующего следствия теоремы Лиувилля: интеграл от e^{x^2} не является элементарной функцией.
— количество абстракций просто гигантское;
— множество понятий просто нельзя формализовать, можно формализовать только например действия над этими понятиями либо только результат определенного действия;
— некоторые уже существующие доказательства (например доказательство от обратного) невероятно сложно описать какими либо абстракциями алгоритмически;
— еще сложнее представить его в такой абстрактной форме, что бы алгоритм софта (какой бы умный он не был) однозначно ответил да/нет/константа/множество и т.д. — иногда математика оперирует оценочными суждениями;
— все это вообще не реально, если мы имеем дело с экспандирующими абстракциями (что-нибудь вида произведения двух и более «матричных» или даже «бесконечных» абстракций);
Чтобы не быть голословным, пример:
Есть какая-то (неточная) мат. абстракция LA, которая может быть реализована только лямбдой (в программистском смысле). В доказательстве используется интеграл от этой лямбды или еще хуже произведение с другой мат. абстракцией LB, тоже представленой только лямбдой. Так вот, моей дилетантской математики достаточно чтобы представить в голове или на бумаге свойства такого интеграла или произведения. Но я как программист не имею ни малейшего понятия как представить результат алгоритмически — даже что это за конструкция (как должна быть формализована в программе) не представляю.
Я только за, если кто сможет ..., но пока помоему, без вариантов.
Для тех кто в танке, просьба не делать голословных заявлений, а описать алгоритмически ну например какую нибудь элементарную функцию (по Лиувилю) а потом применить эту абстракцию для доказательства ну например следующего следствия теоремы Лиувилля: интеграл от e^{x^2} не является элементарной функцией.
Да еще чего забыл: у такого мета-языка (буде его кто-либо осилит) будет огромнейшая семантическая составляющая, со всеми вытекающеми. Ну или если короче, сложный будет очень и для освоения и для написания «сценариев» доказательства. Я уж молчу про читабельность по сравнению с сухим «языком» мат. формул. То что в результате получится в исходниках, сам «писатель» врядли осилит через пару месяцев.
Так вот, доказательство теоремы от Мотидзуки на английском и «математическом» то языках никто не может (не хочет) понять, а вы собираетесь в эту кучу еще какой-то мета-язык запихнуть? Или вы считаете, что он самодостаточен, т.е. ошибки на этом языке исключены по определению? — накидал кучу исходников — оно сказало теорема доказана и все?
Смею вас разочаровать, такого не бывает. За свою карьеру программером, я много повидал исходников, кстати написанных в том числе и гениями (по моим скромным понятиям) — так вот абстрактный код в вакууме (об ошибках говоря) бывает трех типов:
— код содержит явные ошибки;
— ошибки в коде еще не выявлены;
— ошибки есть но пока не происходят на текущих данных (зависят от каких-либо входных параметровв том числе от положения звезд на небе).
Какими бы тест-кейсами код не покрывался, какой бы ревью не делался, сколь долго тестеры не гоняли бы этот код. И чем абстрактнее или формальнее язык программирования, тем чаще можно словить баг. А здесь у нас вообще абстрактно-формально-описательный язык в абсолюте(в степени X факториал), который оперирует даже не объектами, классами и выражениями, а абстрактными моделями и функциональными описаниями.
Я вам больше скажу — тот кто будет вынужден писать на этом — пострадает почище того, кто этот «язык» будет реализовывать.
Почему-то эту сторону вопроса никто из поборников «универсального математического компилятора» вообще не рассматривал. А надо было бы…
Так вот, доказательство теоремы от Мотидзуки на английском и «математическом» то языках никто не может (не хочет) понять, а вы собираетесь в эту кучу еще какой-то мета-язык запихнуть? Или вы считаете, что он самодостаточен, т.е. ошибки на этом языке исключены по определению? — накидал кучу исходников — оно сказало теорема доказана и все?
Смею вас разочаровать, такого не бывает. За свою карьеру программером, я много повидал исходников, кстати написанных в том числе и гениями (по моим скромным понятиям) — так вот абстрактный код в вакууме (об ошибках говоря) бывает трех типов:
— код содержит явные ошибки;
— ошибки в коде еще не выявлены;
— ошибки есть но пока не происходят на текущих данных (зависят от каких-либо входных параметров
Какими бы тест-кейсами код не покрывался, какой бы ревью не делался, сколь долго тестеры не гоняли бы этот код. И чем абстрактнее или формальнее язык программирования, тем чаще можно словить баг. А здесь у нас вообще абстрактно-формально-описательный язык в абсолюте
Я вам больше скажу — тот кто будет вынужден писать на этом — пострадает почище того, кто этот «язык» будет реализовывать.
Почему-то эту сторону вопроса никто из поборников «универсального математического компилятора» вообще не рассматривал. А надо было бы…
Существуют языки, отсутствие ошибок в которых формально доказано. Математически. И если такой язык скажет, что доказательство верно — оно действительно верно, в рамках математики, которой доказано что верен язык (интерпретатор языка). Если же интерпретатор говорит, что док-во неверно, он сообщает также, какой переход неправилен. Математику нужно лишь проверить, соответствует ли код, написанный для этого перехода, самому переходу в док-ве. При этом переход достаточно элементарен — на том уровне абстракций, на котором он применяется (а ля «согласно теореме Х», при этом у теоремы простые условие и вывод, но сложное док-во). Если переход закодирован неверно, математик его исправляет и возобновляет проверку, в противном случае док-во содержит ошибку.
Я подозреваю что у всего математического мира нежелание проверять из-за того, что по аналогии с языками программирования, людям привыкшим к C#/Java для понимания доказательства придется предварительно изучить Brainfuck
Что абсолютно не понятно, с моей точки зрения, это нежелание всего «математического» мира, всех этих выдающихся «Перельманов», «Уайльсов» и т.д. «изучить» эту библиотеку, чтобы понять доказательство этой важнейшей гипотезы.
Это-то как раз понятно. Никто не оплатит эту работу. Ну поймёт кто-то эту работу, и что? Математикам же платят за количество публикаций (во всём мире), а не за понимание (и это гигантская печалька).
Спасибо за локализацию статьи :)
И такие вещи существуют в программировании. Взять, например, язык K и написанную на нем kdb.
Синтаксис K:
Синтаксис 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Это вы к чему вообще? Язык «программирования» K видел, ну и-и?
Я вообще-то просто аналогию проводил. Безпредметно.
Кстати, если это к другой ветке, где обсуждается «универсальный математический доказатель». И вы язык «К» собираетесь в этом качестве прицепить — не стоит. Это примерно, то же что пытатся для решения математических задач использовать 1C-бухгалтерию вместо например матлаб.
Я вообще-то просто аналогию проводил. Безпредметно.
Кстати, если это к другой ветке, где обсуждается «универсальный математический доказатель». И вы язык «К» собираетесь в этом качестве прицепить — не стоит. Это примерно, то же что пытатся для решения математических задач использовать 1C-бухгалтерию вместо например матлаб.
Ещё раз убедился в том, что математика является гуманитарной наукой.
Как Вы определяете термин «гуманитарная наука»?
Только гуманитарий мог такое сморозить.
Физ-мат, аспирантура, аналитические решения внутренних задач гидродинамики при ламинарном и стационарном режимах, решение бигармонического уравнения Навье-Стокса методом малых возмущений, цепочки Боголюбова,… — такое у меня образование. Более того, я искренне понимаю Ваши поспешные минусы к фразе о математике.
В таком случае, вы просто не понимаете смысла слова "гуманитарный".
Строго говоря, математика даже не является наукой. Это формальная система правил, которыми руководствуется человек в своих построениях. Математика — явление человеческой природы, один из языков человека.
Наукой является не язык сам по себе, а лингвистика — нечто, что этот язык изучает.
Ну а т.к. математика — порождение человеческого разума, то очевидно, что ее изучение это точная гуманитарная дисциплина.
Курите философию науки, господа.
Наукой является не язык сам по себе, а лингвистика — нечто, что этот язык изучает.
Ну а т.к. математика — порождение человеческого разума, то очевидно, что ее изучение это точная гуманитарная дисциплина.
Курите философию науки, господа.
Не люблю такие холивары, потому что нереально кого-либо переубедить. Но я все таки отвечу.
Литература, философия — это не науки. Это вот точно просто порождение человеческой мысли. Если подумать, то ясно, что без человека философии бы не возникло. Если б на планете появились мыслящие кристаллы, думали бы они по-другому и нашей философии бы точно не было. А вот математика от человека точно не зависит. Она одинакова в любой точке Вселенной. Как и физика, как и химия. Да, математика — свод правил. Но они взялись из нашего мира, а не из человеческого воображения. Так что называть математику гуманитарной наукой неправильно. Я бы сказал, что ставить рядом слова «наука» и «гуманитарная» вообще неправильно, но это уже отдельный разговор.
Дальше спорить не вижу смысла.
Литература, философия — это не науки. Это вот точно просто порождение человеческой мысли. Если подумать, то ясно, что без человека философии бы не возникло. Если б на планете появились мыслящие кристаллы, думали бы они по-другому и нашей философии бы точно не было. А вот математика от человека точно не зависит. Она одинакова в любой точке Вселенной. Как и физика, как и химия. Да, математика — свод правил. Но они взялись из нашего мира, а не из человеческого воображения. Так что называть математику гуманитарной наукой неправильно. Я бы сказал, что ставить рядом слова «наука» и «гуманитарная» вообще неправильно, но это уже отдельный разговор.
Дальше спорить не вижу смысла.
. А вот математика от человека точно не зависит.
Ошибка в этом.
Звезды или галактики объективно существуют без наблюдателя. Числа и прочие математические понятия — не существуют. Они абстрактны. Даже при всей их неизменности.
Звезды или галактики объективно существуют без наблюдателя.
Кстати не факт.
Тем не менее, математика описывает некие законы, как правильно было подмечено — не зависящие от человека, пусть и субъективно (в рамках некой человеческой логики). Другой вопрос — насколько хорошо мы описываем их? Наши абстракции возможно и не существуют, но то, к чему мы подбираемся с помощью них — вполне реально
А если брать пример с кристаллами, то да, философия у них скорее всего была бы другой. И математика тоже другой, но тут речь идет скорее о реализации, а не о целях и конечных результатах. Так что математику «кристаллов» (да простит меня Император за эту ересь) вполне можно было бы назвать другим «языком» математики. К тому же есть вероятность, что и человеческая математика еще существенно изменится со временем.
Звёзды и галактики существуют только в предположении, что законы природы везде одинаковы. Если убрать это предположение, то мы можем лишь сказать, что из сферы, окружающей нас, на наш разум воздействуют чем-то похожим на свет от свечи.
А насчет гуманитарных наук. Та же социология вполне удовлетворяет критериям настоящей науки, при этом оставаясь гуманитарной (т.к. существует только в контексте человека). Другое дело, что она чуть менее чем полностью захвачена идиотами, но это не мешает в ней ставить эксперименты и вести настоящие исследования.
Что это значит? Математика — наука. Если попросят привести пример науки, и вы скажете «Математика», то будете правы на 100%. В энциклопедии Британника математика определяется как наука. Конечно, вы можете иметь альтернативный взгляд на смысл понятий «наука» и «математика», однако в том виде, в котором пытаетесь представить их вы, они явно противоречат общепринятым. По меньшей мере, то, о чём вы говорите, скорее соответствует разделу философии под названием «логика», чем понятию «математика».
Не гуманитаризируйте на техническом ресурсе, не надо патетичненьких фраз вроде «математика — язык человека» или «математика — царица наук».
Не гуманитаризируйте на техническом ресурсе, не надо патетичненьких фраз вроде «математика — язык человека» или «математика — царица наук».
Мой взгляд на понятие математики — это общепринятый взгляд серьезных ученых-естественников, да и самих математиков, интересующихся предметом дальше своего носа.
А ваш взгляд — это ололо-кококо студента-недоучки, который знает только то, что он должен ненавидеть гуманитариев.
Даже ваша фраза про язык вас выдает с головой. У этого слова есть строгое формальное определение, о котором вы, разумеется, не слышали.
Для большинства людей математика является наукой, что и отражено в определении британики. Они так привыкли и им так вдолбили в школе. Хотите уподобляться большинству — стоит начать сидеть в одноклассниках и смотреть Дом-2.
А ваш взгляд — это ололо-кококо студента-недоучки, который знает только то, что он должен ненавидеть гуманитариев.
Даже ваша фраза про язык вас выдает с головой. У этого слова есть строгое формальное определение, о котором вы, разумеется, не слышали.
Для большинства людей математика является наукой, что и отражено в определении британики. Они так привыкли и им так вдолбили в школе. Хотите уподобляться большинству — стоит начать сидеть в одноклассниках и смотреть Дом-2.
Каких учёных? Каких математиков? Где пруфы на научные работы? На книги, цитаты? Вы знаете, что допустили как минимум две логические ошибки разных типов (аргумент к социальной безуспешности, аппеляция к анонимному авторитету), о которых вы, разумеется, даже не слышали?
wwintspace.net/n-427.html
Рекомендую ознакомиться со статьей целиком. Это лишь малый отрывок.
Рекомендую ознакомиться со статьей целиком. Это лишь малый отрывок.
Никто не знает, сохранят ли грядущие века и тысячелетия сегодняшнее деление наук на естественные и гуманитарные. Но даже и сегодня безоговорочное отнесение математики к естественным наукам вызывает серьезные возражения. Ее родство с естественными науками, прежде всего — с физикой, очевидно, и нередко приходится слышать, что математика является частью физики, поскольку описывает свойства внешнего, физического мира. Но с тем же успехом ее можно считать частью психологии, поскольку изучаемые в ней абстракции суть явления нашего мышления, а значит, должны проходить по ведомству психологии. Не менее очевидна и логическая, приближающаяся к философской, природа математики. Скажем, знаменитую теорему Гёделя о неполноте, гласящую, что какие бы способы доказывания ни установить, всегда найдется истинное, но не доказуемое утверждение — причем даже среди утверждений о натуральных числах, — эту теорему можно считать теоремой теории познания.
Владимир Андреевич Успенский, доктор физико-математических наук, заведующий кафедрой математической логики и теории алгоритмов мехмата МГУ, Земля (Sol III).
Там многовато проблематики и воды, но отдельные моменты вполне точно отражают сомнения самих математиков по поводы природы того, что они изучают.
Когда учили нас, то математику относили не к естественным и не к гуманитарным наукам, а к точным.
Потому что есть существенные отличия и от естественных (изучается порождение человеческого разума, а не природный объект), и от гуманитарных (есть понятие эксперимента, позволяющее объективно разделить утверждения на истинные и ложные).
Потому что есть существенные отличия и от естественных (изучается порождение человеческого разума, а не природный объект), и от гуманитарных (есть понятие эксперимента, позволяющее объективно разделить утверждения на истинные и ложные).
Ну, во-первых, нужно отметить, что
Поэтому, если ссылаться на авторитеты, то получим две противоборствующие стороны: «математика — наука» и «математика — не наука» (а лучше уточнить: «математика — естественная наука» и «математика — гуманитарная наука», потому что, насколько я понял из статьи, В.А. Успенский говорит об отнесении «науки математики» к гуманитарной ветке, а не о лишении математики статуса науки, что, с другой стороны, хотите сделать вы:
Потом, В.А. Успенский называет «вторым и более глубоким фактором» то, что
Ну и третий фактор, который упоминается статье уже смещён до безобразия. Ображение к этимологии и толкованию слов для… для чего? Это вообще аргументом можно назвать? В англ. языке есть слово fail, которому нет прямого аналога в русском — так что теперь? А может отсутствие в (исконно?) русском языке толкования слова «ложь» в том смысле, в котором это делают в математике, наоборот отдаляет математику от блока гуманитарных наук. Разве нет?
В общем лучи негодования В.А. Успенскому за его статью. Не примите меня за технофашиста, но статья в самом деле «гуманитарная с ног до головы», с безобразной, маразматичной, аргументацией. Зачем автор опять затрагивает эту якобы проблему «физиков и лириков» («технарей и гуманитариев»), да сколько можно! Это моё ИМХО, естестественно.
Авторами «Британники» являются ведущие мировые эксперты, среди которых десятки лауреатов Нобелевской премии. В разное время статьи для «Британники» писали Зигмунд Фрейд, Альберт Эйнштейн, Мария Кюри, Генри Форд, Лев Троцкий. Современная версия «Британники» создана при участии около 4000 авторов и редакторов.(взято из вики)
Поэтому, если ссылаться на авторитеты, то получим две противоборствующие стороны: «математика — наука» и «математика — не наука» (а лучше уточнить: «математика — естественная наука» и «математика — гуманитарная наука», потому что, насколько я понял из статьи, В.А. Успенский говорит об отнесении «науки математики» к гуманитарной ветке, а не о лишении математики статуса науки, что, с другой стороны, хотите сделать вы:
Строго говоря, математика даже не является наукой.Во-вторых, с рассуждениями В.А. Успенского я тоже не согласен. То, что математика отошла от «сухой цифири» (хотя весьма глупым выглядит попытка доказать это путем упоминания о парадоксе близнецов, который не является чисто математической проблемой (а тем более глупо говорить о парадоксе близнецов как о проблеме, ждущей решения), или о «попытках (математиков) познания бесконечного, которые значительно расширяют горизонты мышления») — не повод переносить её в разряд гуманитарных дисциплин. А почему бы туда не перенести физику? Физики (особенно квантовые) сейчас рассуждают о немыслимых вещах, куда дальше уходя от «тупо цифири». Опять же, то, что математика «расширяет навыки мышления», улучшает «строгость мышления и воображение» — это просто свойство математики (и, скажем, того же программирования тоже) — не повод сделать её гуманитарной. А может сделаем информатику гуманитарной дисциплиной? Ведь у нас тут абстракции разные, знаете ли.
Потом, В.А. Успенский называет «вторым и более глубоким фактором» то, что
занятия математикой и сопряженное с ними систематическое использование точной терминологии определенным образом сказываются на психологии, по крайней мере в части восприятия словНа хабре была не одна статья о профессиональной деформации программистов — так что, может всё же сделаем информатику гуманитарной дисциплиной, ведь программирование сопряжено с использованием точной терминологии, что определённым образом складывается на психологии (кстати, почему на психологии, а не на психике?). Или физику?
Ну и третий фактор, который упоминается статье уже смещён до безобразия. Ображение к этимологии и толкованию слов для… для чего? Это вообще аргументом можно назвать? В англ. языке есть слово fail, которому нет прямого аналога в русском — так что теперь? А может отсутствие в (исконно?) русском языке толкования слова «ложь» в том смысле, в котором это делают в математике, наоборот отдаляет математику от блока гуманитарных наук. Разве нет?
В общем лучи негодования В.А. Успенскому за его статью. Не примите меня за технофашиста, но статья в самом деле «гуманитарная с ног до головы», с безобразной, маразматичной, аргументацией. Зачем автор опять затрагивает эту якобы проблему «физиков и лириков» («технарей и гуманитариев»), да сколько можно! Это моё ИМХО, естестественно.
Вы сейчас воспроизводите мнение группы Бурбаки. Многие наши математики не разделяет ее. Хорошо известно выражение Арнольда, что математика — экспериментальная наука.
Я отношусь к естественникам и не встречал еще кого-либо среди коллег, кто разделял это определение. Т.к. различия между математическим «экспериментом» и натурным достаточно очевидны.
Считайте, что одного человека вы знаете — это я.
Различия лишь в форме. А так схема одна: наблюдение, выдвижение гипотез и доказательство.
И там и там доказательство сводится к получению ожидаемого поведения, которому проявляться всякого рода помехи. Только в естесвеных науках это решается с помощью увеличению точности приборов, завязанное на понимании физических процессов.
То в математике это сводится к формализацию формулировок, завязанных на логических построениях.
Различия лишь в форме. А так схема одна: наблюдение, выдвижение гипотез и доказательство.
И там и там доказательство сводится к получению ожидаемого поведения, которому проявляться всякого рода помехи. Только в естесвеных науках это решается с помощью увеличению точности приборов, завязанное на понимании физических процессов.
То в математике это сводится к формализацию формулировок, завязанных на логических построениях.
Это сейчас схема такая. Раньше было по-другому — кто кого переспорит на площади, тот и прав. Возможно, через некоторое время схема снова изменится, и истинность теорем будет решаться на заседаниях Думы голосованием. Или наоборот, найдётся теория, для которой и нынешняя матлогика, и теория множеств будут следствиями (в рамках правил вывода — или того, что их заменит — уже этой теории). И это не сделает математику ни естественной, ни, тем более, гуманитарной наукой. «Математика — это язык».
Вы не правы, причем не правы во всем. Да еще и передергиваете с думой.
1) В математике никогда не было того, что вы говорите. Вы явно путаете с философией и риторикой.
2) Доказательства эволюционировали, что в физике, что в математике. Достаточно вспомнить Аристотеля и то, как он доказывал то, что для движения нужна сила.
3) Эти новые рамки будут созданы на основе решения парадоксов и проблем, вызванных старой системой. Так теория множеств возникла на основе развитии рядов и геометрии, так и интуиционизм и теория Цермело-Френкеля возникли на основе парадоксов теории множеств, ровно как действительные число ввели из-за развития геометрии, ровно как комплексные числа из-за появления формулы Кардано.
1) В математике никогда не было того, что вы говорите. Вы явно путаете с философией и риторикой.
2) Доказательства эволюционировали, что в физике, что в математике. Достаточно вспомнить Аристотеля и то, как он доказывал то, что для движения нужна сила.
3) Эти новые рамки будут созданы на основе решения парадоксов и проблем, вызванных старой системой. Так теория множеств возникла на основе развитии рядов и геометрии, так и интуиционизм и теория Цермело-Френкеля возникли на основе парадоксов теории множеств, ровно как действительные число ввели из-за развития геометрии, ровно как комплексные числа из-за появления формулы Кардано.
1) Наверное, путаю. Но была ли до Евклида и Аристотеля математика отделена от философии?
2) Действительно. В математике — из-за уточнения набора аксиом той или иной теории. В физике? Наверное, можно законы рассматривать, как разновидность аксиом, а объекты «реального мира» — как объекты этой теории. Но получится не более, чем математическая модель соответствующего кусочка мира. И задачей физики будет проверить соответствие этой модели наблюдаемому миру, а задачей математики — говорить, какие теоремы будут работать и как они будут проявляться в «наблюдаемых» терминах. У математиков будут «доказательства», а у физиков — «подтверждения».
3) Вот упоминание интуиционизма здесь действительно интересно. Интуиционизм и конструктивизм предлагают использование другой логики, т.е. из одного и того же набора аксиом получаются разные наборы теорем. Можно сказать, что это разные математики.
А насчет «парадоксов и проблем»… как насчёт континуум-гипотезы и аксиомы выбора? В реальном мире континуум-гипотеза не нужна вообще, ни она, ни её отрицание ничего особенного не дают. А от аксиомы выбора вообще одни неприятности, вроде парадокса Банаха-Тарского. Тем не менее, математики её почему-то очень любят :)
2) Действительно. В математике — из-за уточнения набора аксиом той или иной теории. В физике? Наверное, можно законы рассматривать, как разновидность аксиом, а объекты «реального мира» — как объекты этой теории. Но получится не более, чем математическая модель соответствующего кусочка мира. И задачей физики будет проверить соответствие этой модели наблюдаемому миру, а задачей математики — говорить, какие теоремы будут работать и как они будут проявляться в «наблюдаемых» терминах. У математиков будут «доказательства», а у физиков — «подтверждения».
3) Вот упоминание интуиционизма здесь действительно интересно. Интуиционизм и конструктивизм предлагают использование другой логики, т.е. из одного и того же набора аксиом получаются разные наборы теорем. Можно сказать, что это разные математики.
А насчет «парадоксов и проблем»… как насчёт континуум-гипотезы и аксиомы выбора? В реальном мире континуум-гипотеза не нужна вообще, ни она, ни её отрицание ничего особенного не дают. А от аксиомы выбора вообще одни неприятности, вроде парадокса Банаха-Тарского. Тем не менее, математики её почему-то очень любят :)
1) Да, более чем. Справедливости ради надо отметить, что платоновская философия аппелировала к математики, но не более
2) Вы сейчас отождествляете мир как таковой с материальной его частью, но это не так.
3) Нет, не разные. Фундаментальная математика формирует разные подходы к решению задач. Но их набор остается одинаковым. Возникающие противоречия составляют обойму тех парадоксов, которые необходимо решать и которые в будущем приведут к развитию новых теорий.
Вы сейчас делаете грубейшую ошибку пытаясь напрямую связать свое понимание реального мира и его проблем с проблемами математики, как впрочем и любой фундаментальной науки.
К примеру, обычному электрику или программисту из гугла глубоко наплевать на то является ли электрон неделимой частицой или нет. Также не волнует вопрос о количестве видов нейтрино или о распаде протона. Ну и т.д.
2) Вы сейчас отождествляете мир как таковой с материальной его частью, но это не так.
3) Нет, не разные. Фундаментальная математика формирует разные подходы к решению задач. Но их набор остается одинаковым. Возникающие противоречия составляют обойму тех парадоксов, которые необходимо решать и которые в будущем приведут к развитию новых теорий.
Вы сейчас делаете грубейшую ошибку пытаясь напрямую связать свое понимание реального мира и его проблем с проблемами математики, как впрочем и любой фундаментальной науки.
К примеру, обычному электрику или программисту из гугла глубоко наплевать на то является ли электрон неделимой частицой или нет. Также не волнует вопрос о количестве видов нейтрино или о распаде протона. Ну и т.д.
Я вообще не считаю, что математика имеет отношение к реальному миру (если реальный мир вообще существует). Она занимается абстрактными понятиями, некоторые из которых физика и другие науки используют для своих моделей.
Насколько математика универсальна — не знаю. Например, может ли существовать математика без натуральных чисел или без теории множеств. Или теория множеств быть совсем не такой, как у нас (и вообще не иметь модели в «нашей» математике). Скорее всего, это всё возможно.
«Набор подходов остаётся одинаковым»? Наверное, смотря насколько обобщать. «Доказывать от противного» — это подход? В «нашей» математике он работает, а, например, в конструктивизме нет. Или «подходами» вы называете правила вывода? Или общий принцип «есть аксиомы, и есть теоремы»? Или вообще «утверждения могут быть истинными, а могут быть ложными»? Я пока не слышал о математических теориях, в которых эти принципы бы нарушались. Но это не значит, что «у кристаллов» они обязаны быть.
Насколько математика универсальна — не знаю. Например, может ли существовать математика без натуральных чисел или без теории множеств. Или теория множеств быть совсем не такой, как у нас (и вообще не иметь модели в «нашей» математике). Скорее всего, это всё возможно.
«Набор подходов остаётся одинаковым»? Наверное, смотря насколько обобщать. «Доказывать от противного» — это подход? В «нашей» математике он работает, а, например, в конструктивизме нет. Или «подходами» вы называете правила вывода? Или общий принцип «есть аксиомы, и есть теоремы»? Или вообще «утверждения могут быть истинными, а могут быть ложными»? Я пока не слышал о математических теориях, в которых эти принципы бы нарушались. Но это не значит, что «у кристаллов» они обязаны быть.
Помнится, Фейнман не считал математику наукой, т.к. её «нельзя» проверить экспериментально.
Признаться, я с этим не согласен. Да и проверить её очень даже можно: взять, к примеру, геометрию. Берём относительно плоскую поверхность, рисуем круг радиуса R, измеряем площадь. Математика предсказывает, что она будет примерно равна 22/7 R^2. Рисуем концентрический круг радиуса 2R и измеряем его площадь. Математика предсказывает, что площадь увеличится ровно в четыре раза.
Если бы эти соотношения не выполнялись, современная математика была бы совсем иной, ведь по преданию математика родилась как раз из практической необходимости измерять землю в Египте.
Даже на замечательной связи, объединяющей физику с математикой, мы не задержимся. (Математика, с нашей точки зрения, не наука в том смысле, что она не относится к естественным наукам. Ведь мерило ее справедливости отнюдь не опыт.) Кстати, не все то, что не наука, уж обязательно плохо. Любовь, например, тоже не наука. Словом, когда какую-то вещь называют не наукой, это не значит, что с нею что-то неладно: просто не наука она, и всё.
Признаться, я с этим не согласен. Да и проверить её очень даже можно: взять, к примеру, геометрию. Берём относительно плоскую поверхность, рисуем круг радиуса R, измеряем площадь. Математика предсказывает, что она будет примерно равна 22/7 R^2. Рисуем концентрический круг радиуса 2R и измеряем его площадь. Математика предсказывает, что площадь увеличится ровно в четыре раза.
Если бы эти соотношения не выполнялись, современная математика была бы совсем иной, ведь по преданию математика родилась как раз из практической необходимости измерять землю в Египте.
не наука в том смысле, что она не относится к естественным наукамТо бишь Фейнман не относит математику к естественным наукам, а не к наукам вообще. Если выделить категории «точных, естественных и инженерных наук», то математика попадает в «точные».
Спор о верности любого утверждения вида «А — это Б», где А и Б — некоторые слова естественного языка, на мой взгляд лишены всякого смысла. Естественный язык отличается от формального тем, что в нём значение слов держится лишь на негласном предположении, что собеседники подразумевают одно и то же понятие. В общем случае два человека могут иметь разные точки зрения о значении слова «наука», и нет чёткого критерия, по которому одно из них можно однозначно выбрать верным. При некоторых значениях слова «наука», фраза «математика — наука» верна, при некоторых нет. Принцип большинства, отсылка к авторитету — это всё логические заблуждения.
Статья читается с такой интригой! Прямо детектив какой-то. Очень интересно, большое спасибо.
200 лет спустя:
«Вот ведь люди в эпоху пресингулярности обленились, ехидничал AI0x0AB3, – начиная анализировать „математической мир Мотидзуки“ начала XXI-го века, — даже не удосужились перепроверить доказательство abc-гипотезы своих коллег». AI0x0AB3 ругнулся на ограничения по энергии выделяемые на исторические исследования и со словами: «Интересно, интересно… сейчас проверим», — отправил 90% всех своих скудных ресурсов на перепроверку приведенных доказательство". Через 2^36 мкс было найдено несколько формальных ошибок, но конца и края этому док-ву не было видно… AI0x0AB3 ещё раз посетовал на энергетические ограничения для исторических исследований, сгенерировал отчет с указанием формальных ошибок и выставил метку напротив работы «Статус непределенный. Полное исследование требует энергетических затрат, первышающих доступные ресурсы выделенные на исторические исследования пресингулярной эпохи человечества. »
«Вот ведь люди в эпоху пресингулярности обленились, ехидничал AI0x0AB3, – начиная анализировать „математической мир Мотидзуки“ начала XXI-го века, — даже не удосужились перепроверить доказательство abc-гипотезы своих коллег». AI0x0AB3 ругнулся на ограничения по энергии выделяемые на исторические исследования и со словами: «Интересно, интересно… сейчас проверим», — отправил 90% всех своих скудных ресурсов на перепроверку приведенных доказательство". Через 2^36 мкс было найдено несколько формальных ошибок, но конца и края этому док-ву не было видно… AI0x0AB3 ещё раз посетовал на энергетические ограничения для исторических исследований, сгенерировал отчет с указанием формальных ошибок и выставил метку напротив работы «Статус непределенный. Полное исследование требует энергетических затрат, первышающих доступные ресурсы выделенные на исторические исследования пресингулярной эпохи человечества. »
Тоже мне, гений. Вот Янукович — голова! Хоть и профессора получил позже. Зато у него были другие «университеты».
«Если сообщество не понимает, ты не сделал свою работу»
Видимо, это проблема сообщества…
Видимо, это проблема сообщества…
Это не проблема. Это feature. Математика — это объективное знание, если кто-то что-то там себе напридумывал, это ещё не означает, что он получил объективное знание. А объективным оно станет, когда кто-то другой сможет проверить рассуждения. Так что, с сообществом всё в порядке. А вот, что всё в порядке с товарищем Мотидзуки, — не факт. Даже Гёдель сломался… Так что…
Если вы не можете объяснить пятилетнему ребенку свою мысль Если вы не можете объяснить пятилетнему ребенку свою мысль, значит, вы сами ее не очень то понимаете. (Альберт Эйнштейн)
В этой фразе, так любимой многими, ни слова не говорится о времени, которое необходимо на это потратить. И пятилетнему ребенку можно объяснить квантмех в терминах камешков и стеклышек, только времени на составление таких предложений придется затратить столько, что ребенок быстрее закончит профильный ВУЗ и научится соответствующему формальному языку. Математика для того и создает свой аналитический аппарат, чтобы укладывать целые серии (вложенных) соображений буквально в одной строке символов.
мне кажется во фразе «Если вы не можете объяснить пятилетнему ребенку свою мысль Если вы не можете объяснить пятилетнему ребенку свою мысль, значит, вы сами ее не очень то понимаете. » заложено ограничение на объяснение в 1 год.
А если ему 5 с половиной?
Интересное наблюдение, однако Эйнштейн всё же оставил лазейки: всегда можно, например, начать перемещать ребёнка на околосветовой скорости, тем самым выиграв время :)
Возникнет проблема с передачей информации от вас ребенку, движущемуся на такой скорости. Время выиграете, а информации ему все равно сможете передать то же количество (точно не уверен, лишь гипотеза)
Да не в коем разе. Субъективное время движущегося на околосветовой скорости ребенка будет гораздо быстрее объективного. С точки зрения вас у него ионы в нейронах станут медленнее двигаться, и время вы выиграете только на собственные раздумья, но не на объяснение ребенку.
Попробовал почитать. Я совсем не специалист по теории чисел, но Google при попытке найти непонятные мне термины выдаёт почти всегда ссылки на статьи S. Mochizuki (это он же, да?). Видимо, действительно, какая-то у него совсем своя система понятий.
Вот пишут «своя система понятий», «свой мир» — а если я тут введу свою систему понятий в духе «пускай у нас есть белый кролик, часовщик и шляпник, которые....» и в этой системе докажу abc-теорему, P=NP и прочие забавные штуки, которые может быть будут логично вытекать в этой моей системе из самого существования кролика, часовщика и шляпника — какой от этого толк? Это ведь никак не повлияет на реальные вещи, знания и мат.теоремы в нашем мире.
Аксиоматика одна и та же.
Вы здесь немного передергиваете — так можно и до собственной системы счисления дойти (чего Мотидзуки никак не делал).
Снова проведя аналогию к программированию, согласитесь, что для того чтобы понять как работает какой-нибудь синтаксический анализатор (парсер), построеный на регулярных выражениях, нужно все-таки разбираться в регулярных выражениях.
Хотя можно конечно потребовать от создателя этого парсера, переписать его вообще не используя регулярок, на чистых сях.
Аналогия становится понятней, если рассмотреть давний случай с Генри Спесером, когда он выложил лексер написаный с использованием его же библиотеки regex. Теперь она (библиотека) очень даже используется, хотя раньше вызывала похожие чувства, что и с выкладками Мотидзуки.
Снова проведя аналогию к программированию, согласитесь, что для того чтобы понять как работает какой-нибудь синтаксический анализатор (парсер), построеный на регулярных выражениях, нужно все-таки разбираться в регулярных выражениях.
Хотя можно конечно потребовать от создателя этого парсера, переписать его вообще не используя регулярок, на чистых сях.
Аналогия становится понятней, если рассмотреть давний случай с Генри Спесером, когда он выложил лексер написаный с использованием его же библиотеки regex. Теперь она (библиотека) очень даже используется, хотя раньше вызывала похожие чувства, что и с выкладками Мотидзуки.
Попросту говоря, теорема — это наблюдение, которое считается истинным.
Аксиома — это наблюдение, которое считается истинным. Теорему доказывать надо.
"… Так, например, если бы a было 64, что равняется 2^6, то b не может быть никаким числом, которое является произведением двух."
Наверное, не «является произведением двух», а «делится на два». Потому что как вообще понимать «произведение двух»?
Наверное, не «является произведением двух», а «делится на два». Потому что как вообще понимать «произведение двух»?
Так Мотидзуки — это же Шелдон во плоти!
Разговорить его сможет только здоровая конкуренция.
Хотя, на самом деле, по-человечески, думаю ему просто обидно, что никто не читает тысячи страниц его стараний, вот и молчит.
Разговорить его сможет только здоровая конкуренция.
Хотя, на самом деле, по-человечески, думаю ему просто обидно, что никто не читает тысячи страниц его стараний, вот и молчит.
По слухам, за псевдонимом Сатоси Накамото, создателя Bitcoin, скрывается всё тот же Мотидзуки.
Главное, чтобы не оказалось, что за псевдонимом bananafish скрывался все тот же Мотидзуки.
Я подозревал, что японцы — инопланетяне. Что этот Мотидзуки, что основатель биткойна Сатоси Накамото.
Что-то сделали и исчезли.
Что-то сделали и исчезли.
А нельзя ли придумать некий «язык программирования для доказательств», в нём в качестве библиотек внести аксиоматику, затем вводить определения, как классы или функции? Корректность доказательств будет проверяться «компилятором», а проверенные утверждения будут ложиться в «библиотеку классов». Тогда уже будет не важно, хоть тысяча страниц доказательство — компьютер всё проверит. Кроме того, мне кажется, математику-интраверту будет проще переформулировать доказательство в автоматически верифицируемом языке, нежели общаться с коллегами.
Я написал самую прекрасную программу на свете, которая решает все проблемы человечества. Но, к сожалению, для языка, на котором я её написал, пока не существует ни описания, ни работающего интерпретатора.
Теперь я понял, что значит «математический swag».
Похожую проблему описывал Станислав Лем в истории компьютеров будущего. Вычислительные машины незаметно перешли порог разумности и стали сверхразумны. Но вместо военных вычислений они занимаются философией. Люди им не интересны — компьютеры могут предсказывать ответ любого человека за секунду до того, как он его произнесёт. Сходство же ситуаций вот в чём — желая всё-таки поделиться с людьми своими наработками, компьютер сталкивается с проблемой — теорема, записанная на специально им разработанном языке, непонятна людям. Однако, чтобы точно транслировать её на любой человеческий язык потребовалось бы бесконечное количество слов. Тем самым компьютеры производили новые знания, но никто из людей не мог ими воспользоваться.
Мм, а как произведение Лема называется? Сходу не нашел в гугле по «истории компьютеров будущего».
Это не научно, к счастью (или к сожалению?). Если речь идёт именно о доказательстве, то оно должно быть записано в виде выражения, которое можно проверить алгоритмом. А конечные алгоритмы всегда работают с конечными величинами (это верно даже для квантовых компьютеров). Можно, конечно, в доказательствах оперировать чем-то, что требует бесконечного выражения для записи своего точного значения (какие-нибудь иррациональные числа), но математические свойства этих объектов, всё равно, выражаются на конечном языке. Иначе, невозможно было бы проверять доказательства.
Но тут вообще не нужно бесконечности. Компьютеру просто достаточно написать трактат на 10000 страниц, и ни один человек в мире не сможет его осилить, вполне возможно, что чисто из-за биологических ограничений на сложность мозга.
Но тут вообще не нужно бесконечности. Компьютеру просто достаточно написать трактат на 10000 страниц, и ни один человек в мире не сможет его осилить, вполне возможно, что чисто из-за биологических ограничений на сложность мозга.
Почему-то пример Мотидзуки-сан мотивирует на сосредоточенную работу больше всех статей из профильного хаба GTD вместе взятых.
Читая, все ожидал в конце развязки типа: статья оказалась написанной бредогенератором, вроде пресловутого «Корчевателя».
У меня одного осталось ощущение, что я могу настрогать пару десятков таких доказательств?
ru.wikipedia.org/wiki/Открытые_математические_проблемы
Строгайте. Только чур не жульничать!
Строгайте. Только чур не жульничать!
Примечательна также история компьютерного доказательства проблемы четырех красок. В 1960-х появилось первое доказательство с использованием программы для перебора вариантов на комьпютере, а в 2010-х, как я понял, доказательство «перебазировали» на СПО Coq.
Начал читать википедию, чтобы понять суть проблемы — ru.wikipedia.org/wiki/Abc-%E3%E8%EF%EE%F2%E5%E7%E0, а там написано, что:
«В августе 2012 года японский математик Синъити Мотидзуки заявил, что ему удалось доказать эту гипотезу.[3] В октябре того же года Веселин Димитров и Акшай Венкатеш (Akshay Venkatesh) обнаружили ошибку в доказательстве. Мотидзуки признал этот факт, но заявил, что данная ошибка не влияет на основные результаты, а также обещал в ближайшее время опубликовать исправленную версию.»
Я правильно понимаю, что после этого Мотидзуки обновления не выкладывал? Значит можно считать, что проблема то есть, а раз кроме Мотидзуки не может сказать, что она «несущественная», а он сам исправления не выкладывает, то значит доказательство неверное.
«В августе 2012 года японский математик Синъити Мотидзуки заявил, что ему удалось доказать эту гипотезу.[3] В октябре того же года Веселин Димитров и Акшай Венкатеш (Akshay Venkatesh) обнаружили ошибку в доказательстве. Мотидзуки признал этот факт, но заявил, что данная ошибка не влияет на основные результаты, а также обещал в ближайшее время опубликовать исправленную версию.»
Я правильно понимаю, что после этого Мотидзуки обновления не выкладывал? Значит можно считать, что проблема то есть, а раз кроме Мотидзуки не может сказать, что она «несущественная», а он сам исправления не выкладывает, то значит доказательство неверное.
Ввиду объемности выкладок, я понимаю, что задача проверки этого доказательства сложна технически, но она не сложна методически. Каждое математическое утверждение пребывает в причинно-следственной связи с какими-нибудь другими утверждениями. Причем цепи причинно-следственных связей должны быть именно цепями, а не кольцами. Таким образом, любую кучу математических утверждений можно потихоньку разобрать и представить в виде орграфа, где вершинами будут утверждения, а ребра будут соединять утверждение-следствие с утверждением-причиной. (каждое ребро направлено от причины к следствию). Если в этом орграфе обнаружится хоть один неизбыточный цикл (т.е. такой, который невозможно устранить) — все утверждения, прямо или косвенно зависящие от утверждений, входящих в цикл, не могут считаться доказанными (хотя это и не означает, что они не верны). Если же граф окажется без циклов, но у него обязательно должны получиться вершины, в которые не входят ребра. Эти вершины и образуют аксиоматическую базу той математики, в которой работал автор. Далее возможны два варианта:
1) (приятный) аксиоматическая база совпадает с аксиоматической базой общепринятой математики. Тогда можно потихоньку раскручивать тот мат. аппарат, который предлагает японский математик.
2) (неприятный) аксиоматическая база не совпадает с аксиоматической базой общепринятой математики. В таком случае у нас появляется теорема доказательства (или опровержения) эквивалентности предложенной аксиоматической базы и применяемой сейчас. Если они окажутся эквивалентными — см. п1. Если они окажутся неэквивалентными, тогда доказательство просто бесполезно, т.к. оно применимо только для какого-то неведомого нам математического мира.
1) (приятный) аксиоматическая база совпадает с аксиоматической базой общепринятой математики. Тогда можно потихоньку раскручивать тот мат. аппарат, который предлагает японский математик.
2) (неприятный) аксиоматическая база не совпадает с аксиоматической базой общепринятой математики. В таком случае у нас появляется теорема доказательства (или опровержения) эквивалентности предложенной аксиоматической базы и применяемой сейчас. Если они окажутся эквивалентными — см. п1. Если они окажутся неэквивалентными, тогда доказательство просто бесполезно, т.к. оно применимо только для какого-то неведомого нам математического мира.
Освоить мат. аппарат настолько, чтобы проверять доказательства, построенные с его помощью, намного проще, чем освоить настолько, чтобы этот мат. аппарат применять. Поэтому, даже если этот математик владеет изобретенным им мат. аппаратом в разы лучше других выдающихся современных математиков, они могут поэтапно проверить каждое утверждение, если только у этого клубка утверждений есть начало, за которое можно потянуть. Вам не приходилось поражаться простоте задач, которые вы сами не смогли решить, но разобранное решение которых поняли с легкостью?
Приведу еще один пример, который вам, конечно же, не понравится. Допустим, стоит задача доказать некое неравенство, являющееся не совсем очевидным следствием Неравенства Коши (но вы об этом не знаете). Вы будете его долго крутить, пока кто-то вам не покажет, связь между доказываемым неравенством и Неравенством Коши. И когда вы увидите ту самую группировку членов, которая превращает доказываемое неравенство в Неравенство Коши, истинность неравенства не будет вызывать никаких сомнений. (Плюс, разумеется, проверки на области определения и множества значений отдельных выражений неравенства, которые позволят вам сделать нужные преобразования).
P.S. Если он использовал стандартную аксиоматику, то где-то в его многочисленных записях должен быть «логический мостик» (и не один) между общеизвестными утверждениями и понятиями, и его собственными разработками.
Приведу еще один пример, который вам, конечно же, не понравится. Допустим, стоит задача доказать некое неравенство, являющееся не совсем очевидным следствием Неравенства Коши (но вы об этом не знаете). Вы будете его долго крутить, пока кто-то вам не покажет, связь между доказываемым неравенством и Неравенством Коши. И когда вы увидите ту самую группировку членов, которая превращает доказываемое неравенство в Неравенство Коши, истинность неравенства не будет вызывать никаких сомнений. (Плюс, разумеется, проверки на области определения и множества значений отдельных выражений неравенства, которые позволят вам сделать нужные преобразования).
P.S. Если он использовал стандартную аксиоматику, то где-то в его многочисленных записях должен быть «логический мостик» (и не один) между общеизвестными утверждениями и понятиями, и его собственными разработками.
Человек дело говорит, а вот Вы — как-раз занялись балабольством.
Вы излагаете старую и заманчивую математическую идею, идущую еще со времен если не Аристотеля, то Лейбница, о том, как бы нам придумать такую матнотацию, которая будет строго вести все от аксиом, переложить на нее все теоремы и строго их проверить. К сожалению, время, которое требуется что бы переложить даже доказательства теорем средней сложности на подобный язык, значительно превышает время жизни среднего математика. А проверку таких вещей придется поручать компьютеру, так как никто не сможет сделать это вручную. Получается, что даже если некое утверждение и будет строго доказано, математический мир не сможет вынести ничего ценного из самого доказательства — потому что люди не смогу его прочесть и осмыслить.
Это вроде как читать бинарный код. Конечно, можно придумать «дизассемблеры» и можно просить математика сохранять сорцы своих рассуждений, не переложенных на логическую нотацию, анализируя их. Но проблема необходимости ручной компиляции все еще остается. Вот у этого Мотидзуки 512 страниц с ссылками на еще, возможно, миллион страниц изысканий различных мыслителей, которые он прочитал, осмыслил и включил в работу. Вроде теории Тейхмюллера. И каждая строчка в этих страницах, возможно, раскладывается в сотни килобайт «логического кода», так как человеческие языки, в особенности математический — очень сжаты и рассчитаны на передачу огромного количества специальной информации в небольшом объеме. И без искусственного интеллекта никто не сможет компилировать такую громадину в граф причинно-следственных связей, а ИИ у нас нет.
Да нет же, не предлагаю я это компилировать и проверять автоматически. Я предлагаю создать сравнительно простую ИС, состоящую, в общем-то, из БД специальной структуры и интерфейса к ней, которая поможет «разложить по полочкам» все, о чем идет речь в тех доказательствах. Приведу пример. В «Задачнике по математике» Г.Остера есть несколько «непонятных» задачек, которые, на мой взгляд, прекрасно иллюстрируют ход математической мысли при решении.
«Если раздрюсить пусик – получится 3 фарика, если фарик – 5 бляк, если бляку – 2 хрунечка. Мряка однажды нашла 3 пусика и раздрюсила их всех до хрунечков. Сколько получилось хрунечков».
Безусловно, здесь «аксиомы» будут очень простыми и отстоять от конечного результата они будут недалеко.
Тем не менее:
А1: Существует Мряка.
А2: Существуют пусики. Сущности исчислимые, аддитивные.
А3: Существуют фарики. Сущности исчислимые, аддитивные.
А4: Существуют бляки. Сущности исчислимые, аддитивные.
А5: Существуют хрунечки. Сущности исчислимые, аддитивные.
А6: для Мряки и 1 пусика определена операция «раздрюсить». Результат операции – 3 фарика. (некоммутативная)
А7: для Мряки и 1 фарика определена операция «раздрюсить». Результат операции – 5 бляк. (некоммутативная)
А8: для Мряки и 1 бляки определена операция «раздрюсить». Результат операции – 2 хрунечка.
А теперь радостно пользуясь исчислимостью, аддитивностью и определенностью операций над этими сущностями делаем то, что от нас требуется.
«Если раздрюсить пусик – получится 3 фарика, если фарик – 5 бляк, если бляку – 2 хрунечка. Мряка однажды нашла 3 пусика и раздрюсила их всех до хрунечков. Сколько получилось хрунечков».
Безусловно, здесь «аксиомы» будут очень простыми и отстоять от конечного результата они будут недалеко.
Тем не менее:
А1: Существует Мряка.
А2: Существуют пусики. Сущности исчислимые, аддитивные.
А3: Существуют фарики. Сущности исчислимые, аддитивные.
А4: Существуют бляки. Сущности исчислимые, аддитивные.
А5: Существуют хрунечки. Сущности исчислимые, аддитивные.
А6: для Мряки и 1 пусика определена операция «раздрюсить». Результат операции – 3 фарика. (некоммутативная)
А7: для Мряки и 1 фарика определена операция «раздрюсить». Результат операции – 5 бляк. (некоммутативная)
А8: для Мряки и 1 бляки определена операция «раздрюсить». Результат операции – 2 хрунечка.
А теперь радостно пользуясь исчислимостью, аддитивностью и определенностью операций над этими сущностями делаем то, что от нас требуется.
Я говорю о том, что для сложных задач число разнообразных A100500 пусюсики: исчислимые, аддитивные, антикоммутативен при скрещивании с фрянечками — будет измеряться сотнями мегабайт в любой строгой записи доказательства. За всю жизнь образованный человек способен прочесть и впитать не более чем пару гигабайт текстовой информации, поэтому сложность доказательств в иерархической пусик-нотации будет превышать возможности любого человека прочесть (или написать) ЭТО меньше чем за несколько десятилетий непрерывного чтения или письма.
Нет, в том-то и дело, что А (т.е. аксиом) в любом случае будет не более нескольких сотен. Все остальные утверждения будут уже Т (теоремами). Причем каждая следующая Т будет опираться далеко не на все предыдущие, а, опять-таки, на несколько десятков-сотен предыдущих, которые легко просмотреть перед началом работы со следующим утверждением. Передоказывать их не надо, т.к. в БД уже стоит отметка о том, что они доказаны и им можно верить.
А, я понял вас. Ну, собственно, насколько я знаю, в какой то степени так и делается.
Проблема в том, что это все равно часто слишком сложно записать в формальной системе и итог получается слишком объемным для понимания отдельно взятым человеком — не смотря на то, что теоремы упираются на другие теоремы и так далее. Так и тут.
Проблема в том, что это все равно часто слишком сложно записать в формальной системе и итог получается слишком объемным для понимания отдельно взятым человеком — не смотря на то, что теоремы упираются на другие теоремы и так далее. Так и тут.
Мне было бы интересно ознакомиться с работой подобных систем или реализацией подобных механизмов.
На мой взгляд, компьютеры как раз очень-очень могли бы помочь и систематизации таких знаний и в контроле тождественности преобразований. Ведь значительная часть математических выкладок — это именно тождественные преобразования. А правила тождественных преобразований легко формализуются. Правила для получения выражений-следствий тоже во многих случаях можно формализовать.
На мой взгляд, компьютеры как раз очень-очень могли бы помочь и систематизации таких знаний и в контроле тождественности преобразований. Ведь значительная часть математических выкладок — это именно тождественные преобразования. А правила тождественных преобразований легко формализуются. Правила для получения выражений-следствий тоже во многих случаях можно формализовать.
Я не предлагаю переводить доказательства на машинный язык. Я предлагаю задокументировать в электронной форме только причинно-следственные связи между утверждениями, сами же утверждения и их интерпретация пусть остается задачей человека.
Документирование же причинно-следственных связей между утверждениями позволит:
1) установить алгоритмически «нормальность» этой сети утверждений, т.е. отсутствие петель, циклов, отсеять побочные ветви (которые нас временно не интересуют)
2) выявить аксиоматическую базу (как множество утверждений нулевого ранга — таких, которые не ссылаются ни на какие другие утверждения как на обоснование).
3) проверить тождественность или эквивалентность предлагаемого базиса и одного из известных и применяемых в математике базисов.
4) организовать методически работу по осознанию живыми математиками этой сети утверждений «снизу вверх», т.е. таким образом, чтобы каждое новое понятие вводилось на основе уже имеющихся, а каждое новое утверждение доказывалось на основании уже доказанных (собственно, как оно в математике и делается).
Документирование же причинно-следственных связей между утверждениями позволит:
1) установить алгоритмически «нормальность» этой сети утверждений, т.е. отсутствие петель, циклов, отсеять побочные ветви (которые нас временно не интересуют)
2) выявить аксиоматическую базу (как множество утверждений нулевого ранга — таких, которые не ссылаются ни на какие другие утверждения как на обоснование).
3) проверить тождественность или эквивалентность предлагаемого базиса и одного из известных и применяемых в математике базисов.
4) организовать методически работу по осознанию живыми математиками этой сети утверждений «снизу вверх», т.е. таким образом, чтобы каждое новое понятие вводилось на основе уже имеющихся, а каждое новое утверждение доказывалось на основании уже доказанных (собственно, как оно в математике и делается).
Вот несложное изящное доказательство того, что сумма обратных квадратов натурального ряда равна pi^2/6.
heller.ru/blog/2010/09/a-funny-serie/
Можете проиллюстрировать на живом примере?
heller.ru/blog/2010/09/a-funny-serie/
Можете проиллюстрировать на живом примере?
Тут получится очень большая иллюстрация, неподъемная для меня ) Если вы не против, я возьму что-нибудь из геометрии за 5й класс, чтобы уложиться в 10-20 утверждений.
Разумно; просто вышеприведенное доказательство — самое простое из известных мне когитивно сложных доказательств — то есть таких, которые не помещаются в уме. Для геометрии 5 класса такой подход не интересен)
Можете проиллюстрировать на примере доказательства того, что объем конуса равен трети объема цилиндра с таким же основанием и высотой?
Можете проиллюстрировать на примере доказательства того, что объем конуса равен трети объема цилиндра с таким же основанием и высотой?
Ну вот, вы еще не видели, а уже говорите, что это неинтересно :(
А на счет конуса, я что-то не смекну, как это без интегралов доказать.
Кстати, утверждение об объеме выполняется для всех конусов, или только для прямых, у которых в основании окружность?
(я ж не зря лезу аж в геометрию 5 класса, там я не запутаюсь в самой математике и сосредоточусь на примере. А тут я и в самой математике ошибиться могу, и никакого чуда не выйдет).
А на счет конуса, я что-то не смекну, как это без интегралов доказать.
Кстати, утверждение об объеме выполняется для всех конусов, или только для прямых, у которых в основании окружность?
(я ж не зря лезу аж в геометрию 5 класса, там я не запутаюсь в самой математике и сосредоточусь на примере. А тут я и в самой математике ошибиться могу, и никакого чуда не выйдет).
Я вам как раз хотел предложить скатиться в интегралы =) Вообще можно вывести это, разрезав конус на множество маленьких блинчиков условно-цилиндрической формы и просуммировав их объемы… да, я знаю: те же интегралы, только в профиль и для семиклассников.
Ладно, давайте тогда что ли докажем теорему Пифагора. Тут точно негде запутаться.
Ладно, давайте тогда что ли докажем теорему Пифагора. Тут точно негде запутаться.
Непонятно, о какой загадочной связи между сложением и умножением идёт речь, когда в целых числах умножение — это «сахар» над сложением.
В поддержку Мотидзуки хочу напомнить историю Галуа, который, для доказательства не менее простой в формулировке теоремы о неразрешимости в радикалах, также создал свой «математичкеский мир» — теорию групп (в 19 лет!), в которую математический свет тоже не сразу вкурил, а сейчас она доступна студентам младших курсов математических специальностей. Просто «чистая логика» не достаточна для автоматического понимания всеми математиками. Для освоения новой теории должно пройти какое-то время, чтобы математики научились мыслить в категориях этой теории.
В поддержку Мотидзуки хочу напомнить историю Галуа, который, для доказательства не менее простой в формулировке теоремы о неразрешимости в радикалах, также создал свой «математичкеский мир» — теорию групп (в 19 лет!), в которую математический свет тоже не сразу вкурил, а сейчас она доступна студентам младших курсов математических специальностей. Просто «чистая логика» не достаточна для автоматического понимания всеми математиками. Для освоения новой теории должно пройти какое-то время, чтобы математики научились мыслить в категориях этой теории.
Только почему-то число на два слагаемых разложить элементарно, а на два множителя иногда невозможно, а в большинстве случаев дико сложно. Сахар какой-то непростой получается. А теория Галуа, с доказательством неразрешимости — это 250 страниц текста, в которых каждый шаг очевиден, и в которых всё от базовых аксиом и определений до результатов. У Митодзуки совсем не так. И Галуа помогал другим людям разобраться в его теории, в переписке состоял со многими. У Митодзуки тоже совсем не так.
Я думаю, что не нужны тут аналогии. Результат у Митодзуки выдающийся, и рано или поздно какая-нибудь группа математиков его осилит. Аналогии тут не нужны, ибо математика работает и без аналогий :)
Я думаю, что не нужны тут аналогии. Результат у Митодзуки выдающийся, и рано или поздно какая-нибудь группа математиков его осилит. Аналогии тут не нужны, ибо математика работает и без аналогий :)
Галуа помогал другим людям разобраться в его теорииИ даже лекции бесплатные пытался вести по алгебре, только молодые люди не осилили и быстро разбежались.
Я пытался изучать доказательство неразрешимости, даже имея за спиной неплохой бэкэнд в виде весьма неплохого учебника алгебры Кострикина, с самостоятельно прорешенными упражнениями, плюс несколько курсов матмеха. Да, все шаги логически понятны, но КАК?! Как оно работает? Это была какая-то магия. Логически, по шагам, понятно, но в целом — сразу не осилил. Все-таки настаиваю на длительном периоде «усвоения» категорий новой теории.
То, что умножение вычислимо через сложение в целых, еще не позволяет называть его сахаром.
Кстати, а вычислимо ли сложение, через умножение?
Нет, в общем случае сложение невычислимо в целых через умножение. Например, можно с помощью конечного числа операций сложения и вычитания любых двух целых взаимно простых чисел получить любое целое число, однако не существует такого конечного множества целых чисел, из которых с помощью операций сложения и деления можно получить любое целое число — это тривиально доказывается через основную теорему арифметики и утверждение о бесконечном множестве простых чисел.
Прекрасное доказательство. Я бы сам до такого дошел очень не сразу, но услышав его от вас, я его прекрасно понимаю: между множеством чисел, которые можно получить в результате операции сложения не равно множеству чисел, которые можно получить операцией умножения.
(мне эта ситуация подходит в качестве примера того, что доказательство проще проверить, чем вывести).
Кстати, утверждение о бесконечном множестве простых чисел доказано?
(мне эта ситуация подходит в качестве примера того, что доказательство проще проверить, чем вывести).
Кстати, утверждение о бесконечном множестве простых чисел доказано?
Кстати, утверждение о бесконечном множестве простых чисел доказано?
Что вы, конечно доказано, у него же элементарное доказательство!
(решил привести доказательство за время, пока можно редактировать комментарий)
Пусть множество простых конечно. Перемножив все его члены и прибавив к произведению единицу, мы получим число, которое не делится ни на одно из простых чисел вообще — а это очевидно невозможно. Следовательно, это число само простое, или делится на некие простые, не включенные в множество.
Вообще, насколько я знаю, если две операции связаны дистрибутивностью на каком-то множестве, то обычно одна из них вычислима через другую, но не наоборот. То есть умножение и возведение в степень, допустим, будут вести себя точно так же.
Если разрешена еще парочка операций — то да: x+y=log(exp(x)*exp(y))
Неделя математической логики на хабре! Как давно я этого ждал!
Он не оставил сообщение ни на одном сетевом форуме, которые часто посещают математики со всего мира.
А что это за форумы?
Есть еще math.stackexchange.com, но он более прикладной.
Что-то последний месяц математиков прорвало:
Числа-близнецы.
ABC теорема.
Слабая гипотеза Гольдбаха.
Будем ждать гипотезу Римана…
Числа-близнецы.
ABC теорема.
Слабая гипотеза Гольдбаха.
Будем ждать гипотезу Римана…
Эта ситуация сильно напоминает ситуацию из фантастического романа «Бегство земли», когда математик из будущего попал в наш век и ему было крайне трудно подобрать слова для объяснения самых великих теорем 20-го века.
Нет, Дюпон, нет, нет и нет! — кричал профессор. — Это уже чистейший
идиотизм! Это противоречит принципу сохранения энергии, и математически — слышите? — ма-те-мати-чес-ки невозможно!
— С вашей математикой, пожалуй, — спокойно ответил Поль.
— То есть как это, с моей математикой? У вас что, есть другая? Так
изложите ее принципы, черт побери, изложите!
— Да, изложу! — взорвался Поль. — И вы ничего не поймете! Потому что
эта математика ушла от вашей на тысячи лет вперед!
— На тысячи лет, как вам это нравится, а? — вкрадчиво проговорил
профессор. — Позвольте узнать, на сколько именно тысяч лет?
— Ах, если бы я это знал!
Нет, Дюпон, нет, нет и нет! — кричал профессор. — Это уже чистейший
идиотизм! Это противоречит принципу сохранения энергии, и математически — слышите? — ма-те-мати-чес-ки невозможно!
— С вашей математикой, пожалуй, — спокойно ответил Поль.
— То есть как это, с моей математикой? У вас что, есть другая? Так
изложите ее принципы, черт побери, изложите!
— Да, изложу! — взорвался Поль. — И вы ничего не поймете! Потому что
эта математика ушла от вашей на тысячи лет вперед!
— На тысячи лет, как вам это нравится, а? — вкрадчиво проговорил
профессор. — Позвольте узнать, на сколько именно тысяч лет?
— Ах, если бы я это знал!
У Лурье, к слову, тоже были (и до сих пор есть) подобные сложности: его «высшая теория топосов» с доказательством гипотезы Баеца-Долана — работа крайне абстрактная и тяжёлая для усвоения. Однако же её усвоили. Характерен, к слову, комментарий о роли Гротендика по ссылке на MO.
Если в работах Мотидзуки есть интересные мысли — их там обязательно найдут, отряхнут и объяснят простоым языком (ну, как когомологии на примере арифметики за третий класс).
Если в работах Мотидзуки есть интересные мысли — их там обязательно найдут, отряхнут и объяснят простоым языком (ну, как когомологии на примере арифметики за третий класс).
Down to Gehenna or up to the Throne,
He travels the fastest who travels alone. © R. Kipling
He travels the fastest who travels alone. © R. Kipling
Я так понимаю, что «все гениальное — просто», это не про творение Мотидзуки :-)
как написано в дзене питона:
«Простое лучше, чем сложное.
Сложное лучше, чем запутанное. „
может, Мотидзуки как раз занимается способом сделать свое доказательство максимально доступным? тогда понятно его нежелание объяснять работу в незнакомых терминах)
«Простое лучше, чем сложное.
Сложное лучше, чем запутанное. „
может, Мотидзуки как раз занимается способом сделать свое доказательство максимально доступным? тогда понятно его нежелание объяснять работу в незнакомых терминах)
Тем временем процесс идет, хотя и не так быстро: уже четверо математиков разобрались в доказательстве, на подходе ещё люди.
Привет из 2025 года:
Вместо того чтобы показывать моделям нулевого типа миллионы примеров человеческого языка и человеческого мышления, почему бы не научить их основным правилам логики, дедукции, индукции, заблуждениям, когнитивным предубеждениям, научному методу и общему философскому исследованию и не позволить им открыть для себя лучшие способы мышления, которые люди никогда не смогут придумать?
Это👆 то, что DeepSeek попытался сделать с R1-Zero и почти добился.
Когда DeepSeek обучил R1-Zero, им стало трудно читать ответы модели. Она начала смешивать языки. Это снова напоминает мне DeepMind. AlphaGo Zero научилась играть в го лучше, чем AlphaGo, но и более странной для человеческого глаза . В конце концов, AlphaGo научилась у нас , но AlphaGo Zero пришлось открывать свои собственные пути посредством самостоятельной игры. У нее не было наших данных, поэтому у нее не было наших недостатков. Что еще важнее, у нее не было и наших манер.
Из этого возникают вопросы: существуют ли нечеловеческие способы рассуждать о мире, которые более эффективны, чем наши? Станут ли более разумные ИИ не только еще более разумными, но и все более непонятными для нас?
Парадокс доказательства