Есть ли поисковая система по теоремам?

[bayah]

Здравствуйте.

Читал С. Улама "Приключения математика", а там упоминается так называемая "Шотладская книга" - тетрадь, которая хранилась в шотландском баре, в котором различные математики, зависавшие в баре, записывали различные задачи, гипотезы, для доказательства. Другие читали, решали. Эта тетрадь приобрела некоторую известность и поэтому теперь ее можно скачать в интернете.

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

Спасибо).

[itmanager85]

bayah в сообщении #1018788 писал(а):

Существует ли какая нибудь поисковая система по теоремам?

гугл ?

[Sender]

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

[arseniiv]

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

Sender
Можно ведь не пытаться сравнивать на эквивалентность до конца. Можно применить небольшое число преобразований, и если после них совпадения не получилось, честно сказать: «ищите сами, а я выдам для помощи статьи с похожим контекстом».

Кстати вот выдача статей с похожим контекстом — это, наверно, реально уже сейчас. Но всё равно не с помощью поисковых систем общего этого самого, как невпопад написал itmanager85.

[Brukvalub]

А разве все доказанные теоремы уже представлены так, что поисковые машины могут с ними работать? Например, теоремы из какой-нибудь статьи типа: "Об одном свойстве одного уравнения в одном частном случае", опубликованной в 1936 г. в Вестнике ПТУ № 23 г. Волчешкурска?

[arseniiv]

В том и дело, что нет.

[g______d]

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

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

А вообще такая система будет удобной. Например, дополнительное средство проверки доказательств на отсутствие ошибок — нет ли в базе контрпримера к только что доказанной теореме (я думаю, что там сначала будут только формулировки и определения, а доказательства будет проверяться традиционно). Или охватывает ли данный набор лемм все возможные случаи.

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

[Sender]

g______d в сообщении #1020239 писал(а):

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

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

[grizzly]

g______d в сообщении #1020239 писал(а):

Я думаю, дело будет так:...

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

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

[Brukvalub]

Согласно легенде, ТеХ был написан Д. Кнутом тогда, когда ему надоело видеть уродливо набранные издателями тексты его статей. Кто и зачем напишет систему регистрации и распознавания теорем? Не вижу реальных стимулов,чтобы кто-нибудь взялся за такую непростую работу, а вот этот стимул:

g______d в сообщении #1020239 писал(а):

дополнительное средство проверки доказательств на отсутствие ошибок — нет ли в базе контрпримера к только что доказанной теореме

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

[grizzly]

Brukvalub в сообщении #1020298 писал(а):

Согласно легенде, ТеХ был написан Д. Кнутом тогда, когда ему надоело видеть уродливо набранные издателями тексты его статей. Кто и зачем напишет систему регистрации и распознавания теорем?
...
ведь, обычно, специалист и так хорошо знает свою научную "поляну"

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

[Brukvalub]

grizzly в сообщении #1020303 писал(а):

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

Так это про вас писалось: "Боян, бо вещий, аще кому хотяше песнь творити, то растекашется мыслию
по дереву,серым вълком по земли,шизым орлом под облакы." !!!

[Sender]

Brukvalub в сообщении #1020298 писал(а):

Кто и зачем напишет систему регистрации и распознавания теорем?

Например, тот, кто полжизни бился над какой-нибудь проблемой, чтобы потом случайно обнаружить простое короткое доказательство в Вестнике ПТУ № 23 г. Волчешкурска от 1936 г.

[grizzly]

Brukvalub в сообщении #1020305 писал(а):

Так это про вас писалось: "Боян, бо вещий, аще кому хотяше песнь творити, то растекашется мыслию по дереву,серым вълком по земли...

Да-да:

Цитата:

Про нас про всех -- какие, к чёрту, волки?!

[g______d]

Бывают всякие данные, которые удобно систематизировать даже специалистам. Например, существует ли объект со свойствами $A$, $B$ и $C$, но не с $D$. Или, например, в анализе какие пространства куда вкладываются. Ну вот я основные теоремы вложения Соболева помню, но бывают же всякие пространства Бесова с несколькими значками, и вообще их до чёрта.

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

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