Существует ли математический аналог википедии

[fractalon]

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

[kp9r4d]

Если полностью формализованные, то есть metamath proof explorer и HoTT (правда не в виде сайта, а в виде библиотек для некоторого ЯП). Если не полностью формализованные, то есть stack project (по алгебраической геометрии) и proofwiki.

Теоретически возможно, наверное, stack project ведь как-то сделали, но я бы не стал за такое браться не будучи уверенным, что я по-настоящему хорошо разбираюсь во всём этом. Какие-то первичные наброски архитектуры должен всё же сделать один человек и он-то должен действительно хорошо понимать, что происходит.

[fractalon]

kp9r4d в сообщении #1250924 писал(а):

но я бы не стал за такое браться не будучи уверенным, что я по-настоящему хорошо разбираюсь во всём этом

Что вы имеете ввиду? Понимание оснований математики и того, как такую систему можно было бы качественно универсализировать? Знание того, как в принципе программно устроены штуки типа википедии? Или знание того, какие уже есть на свете подобные ресурсы? Где тут наибольший риск по-вашему?

[пианист]

fractalon в сообщении #1250904 писал(а):

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

И для чего такой кошмар?

[kp9r4d]

fractalon в сообщении #1250952 писал(а):

Что вы имеете ввиду? Понимание оснований математики и того, как такую систему можно было бы качественно универсализировать? Знание того, как в принципе программно устроены штуки типа википедии? Или знание того, какие уже есть на свете подобные ресурсы? Где тут наибольший риск по-вашему?

Расстановка акцентов на то, какие сюжеты важны, а какие нет, знание различных терминологических традиций, общая архитектура повествования и доказательств, такое всё. Это конечно если есть желание написать качественный магнум опус, вроде того же stack project, если просто хочется сделать вики про доказательство теорем, то уже есть proofwiki, вы можете выучить математику и поддержать проект своим участием, если вам симпатична идея.

[arseniiv]

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

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

-- Вт сен 26, 2017 22:37:36 --

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

[george66]

arseniiv в сообщении #1251001 писал(а):

Можно было бы взяться за формализованную систему с человекочитаемыми доказательствами. Языки с такими свойствами, кстати, уже есть

В каких языках человекочитаемые доказательства? Единственное, что мне приходит на ум, это Globular
https://golem.ph.utexas.edu/category/20 ... bular.html

[kp9r4d]

Ну в реализациях HoTT ничего так читаются ведь.

[arseniiv]

george66 в сообщении #1251038 писал(а):

В каких языках человекочитаемые доказательства?

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

-- Ср сен 27, 2017 01:43:49 --

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

[fractalon]

Спасибо! proofwiki - как раз то, что меня интересовало. А есть ли у него русскоязычный раздел/аналог?

[Мастак]

fractalon в сообщении #1250904 писал(а):

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

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

А идея (как по математике, так и по другим естественным наукам) ведь не нова, вот есть уже такие вики-интернет-проекты для преподавания математики, где открыты двери для новых участников проектов, например:

для первого класса школ http://wiki.iro.yar.ru/index.php/%D0%9F ... 0%BA%D0%B5
для первых курсов ВУЗов http://ru.math.wikia.com/wiki/%D0%97%D0 ... 1%86%D0%B0
...

PS Проекты есть, но участников недостаточно, так как наверно еще не настолько актуально.

[atlakatl]

Мастак в сообщении #1251690 писал(а):

есть уже такие вики-интернет-проекты для преподавания математики, где открыты двери для новых участников проектов, например:
...для первых курсов ВУЗов http://ru.math.wikia.com/wiki/%D0%97%D0 ... 1%86%D0%B0

Взяли готовые статьи из Википеди и безбожно измываются над ними. Из статьи "Натуральное число":

Цитата:

Существуют два подхода к определению натуральных чисел — числа, используемые при :

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

Заповедник для фриков.

[Someone]

Мастак в сообщении #1251690 писал(а):

Вот такой УЧЕБНИК коллективного написания наверно имеет смысл и может быть создан всеми, у кого есть энтузиазм такого рода.

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

[Dmitriy40]

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

[beroal]

Someone в сообщении #1251798 писал(а):

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

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