2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу 1, 2  След.
 
 Существует ли математический аналог википедии
Сообщение26.09.2017, 13:50 


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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение26.09.2017, 14:45 
Заслуженный участник
Аватара пользователя


09/02/14

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

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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение26.09.2017, 17:32 


08/09/13
210
kp9r4d в сообщении #1250924 писал(а):
но я бы не стал за такое браться не будучи уверенным, что я по-настоящему хорошо разбираюсь во всём этом

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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение26.09.2017, 17:41 
Заслуженный участник
Аватара пользователя


03/06/08
2147
МО
fractalon в сообщении #1250904 писал(а):
где для разных теорем были бы описаны полные доказательства (вместо ссылок на источники) и при нажатии на вспомогательные утверждения, используемые в этих доказательствах, можно было бы перейти на страницу этого утверждения

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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение26.09.2017, 18:09 
Заслуженный участник
Аватара пользователя


09/02/14

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

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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение26.09.2017, 20:35 
Заслуженный участник


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

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

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

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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение26.09.2017, 22:55 
Заслуженный участник


31/12/15
922
arseniiv в сообщении #1251001 писал(а):
Можно было бы взяться за формализованную систему с человекочитаемыми доказательствами. Языки с такими свойствами, кстати, уже есть

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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение26.09.2017, 22:59 
Заслуженный участник
Аватара пользователя


09/02/14

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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение26.09.2017, 23:36 
Заслуженный участник


27/04/09
28128
george66 в сообщении #1251038 писал(а):
В каких языках человекочитаемые доказательства?
Кто-то тут на форуме упоминал всуе Mizar. Вроде их целью были понятные доказательства, но я особо не смотрел. Вообще сама идея должна быть довольно распространена; например, Metamath выглядит так как выглядит лишь потому, что его автор хотел минимализма, а это почти несовместимо с человекочитаемостью.

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

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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение28.09.2017, 21:21 


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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение29.09.2017, 03:21 
Аватара пользователя


27/02/09

416
Мегаполис
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 Проекты есть, но участников недостаточно, так как наверно еще не настолько актуально.

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение29.09.2017, 04:00 
Аватара пользователя


21/09/12

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

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

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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение29.09.2017, 15:34 
Заслуженный участник
Аватара пользователя


23/07/05
17973
Москва
Мастак в сообщении #1251690 писал(а):
Вот такой УЧЕБНИК коллективного написания наверно имеет смысл и может быть создан всеми, у кого есть энтузиазм такого рода.
Если этот "учебник" будут коллективно писать все желающие, то получится хаос, а не учебник. Потому что в учебнике автор продумывает последовательность определений и теорем так, чтобы соблюдалась логическая последовательность: если теорема A доказывается с использованием теоремы B, то теорема B должна быть доказана раньше теоремы A и не ссылаться на неё никаким способом. Ситуации, когда для какой-то теоремы существует множество различных доказательств, использующих различные методы и ссылающихся на различные теоремы, которые предполагаются ранее доказанными, являются типичными, и уследить за отсутствием порочных кругов при независимом коллективном написании будет невозможно.

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение29.09.2017, 15:43 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Существует ли математический аналог википедии
Сообщение29.09.2017, 16:08 
Аватара пользователя


17/04/11
658
Ukraine
Someone в сообщении #1251798 писал(а):
Если этот "учебник" будут коллективно писать все желающие, то получится хаос, а не учебник. Потому что в учебнике автор продумывает последовательность определений и теорем так, чтобы соблюдалась логическая последовательность: если теорема A доказывается с использованием теоремы B, то теорема B должна быть доказана раньше теоремы A и не ссылаться на неё никаким способом. Ситуации, когда для какой-то теоремы существует множество различных доказательств, использующих различные методы и ссылающихся на различные теоремы, которые предполагаются ранее доказанными, являются типичными, и уследить за отсутствием порочных кругов при независимом коллективном написании будет невозможно.

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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 16 ]  На страницу 1, 2  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group