Как проводят свободное время философы и/или математики

[Red_Herring]

Xaositect в сообщении #1087858 писал(а):

А можно пример "минимально серьезной" теоремы не из алгебры? А то оценка серьезности у каждого своя.

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

[sqribner48]

На сайте журнала Formalized Mathematics выложено довольно много формализованных доказательств разных теорем.
Например, в номере Volume 22, Issue 2 (Jun 2014) (по ссылке: http://www.degruyter.com/view/j/forma.2014.22.issue-2/issue-files/forma.2014.22.issue-2.xml)
я нашел пару статей:

(Оффтоп)

с Лагранжем

Yasushige Watase. Lagrange’s Four-Square Theorem. Formalized Mathematics. Volume 22, Issue 2, Pages 105–110, ISSN (Online) 1898-9934, DOI: 10.2478/forma-2014-0012, June 2014

(Оффтоп)

и с Коши

Adam Grabowski. Cauchy Mean Theorem. Formalized Mathematics. Volume 22, Issue 2, Pages 157–166, ISSN (Online) 1898-9934, DOI: 10.2478/forma-2014-0016, June 2014

Там же есть формализованное доказательство невозможности обхода 7 Кенигсбергских мостов.
Есть список 100 формализованных теорем Formalizing 100 Theorems (по ссылке:http://www.cs.ru.nl/F.Wiedijk/100/)

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

[g______d]

Эти обе теоремы, фактически, из алгебры. Было бы интересно увидеть, насколько продвинулась формализация вещественного анализа — например, сколько теорем из учебника для 1 курса формализовано.

Впрочем, я и сам могу попробовать поискать.

[sqribner48]

Уважаемый g______d

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

Было бы интересно увидеть, насколько продвинулась формализация вещественного анализа — например, сколько теорем из учебника для 1 курса формализовано.

Пробежал быстрым косым взглядом по вышеуказанному списку 100 формализованных теорем. По формализации вещественного анализа нашел только это:
15. Fundamental Theorem of Integral Calculus
26. Leibniz's Series for Pi
34. Divergence of the Harmonic Series
35. Taylor's Theorem
64. L'Hôpital's Rule
76. Fourier Series
Слева стоит номер, данный в списке этой проблеме.
Конечно - это "капля в море". Но номера 15, 35 и 64 впечатляют.

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

Впрочем, я и сам могу попробовать поискать.

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

[maximk]

Anton_Peplov в сообщении #1086912 писал(а):

Последние 15 минут лекции – ответы на вопросы и комментарии из зала. Вопросы и комментарии большей частью … эээ… весьма невысокого уровня, в связи с чем приводить их я не стану. Впрочем, и Вавилов при ответе на один вопрос неприятно удивил, заявив, что для работы мозга существенны квантовые эффекты, «потому что было бы смешно, если бы все в природе было устроено в соответствии с квантовой механикой, а мозг нет». Это, мягко говоря, странное «потому что». Вот так: в своей области специалист суров и беспощаден – видите ли, в учебниках матана использование аксиомы выбора не отслеживают, ах, мерзавцы! – а стоило ступить чуть в сторону, как «Остапа понесло».

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

[Anton_Peplov]

maximk в сообщении #1091212 писал(а):

Поясните пожалуйста мне, что здесь странного.

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

[maximk]

Разве из того, что мозг моделируется квантовой механикой, не следует, что он устроен по законам квантовой механики? Подобно тому, как количество людей устроено по законам арифметики (в числе прочих законов).
Разумеется, это не исключает других точек зрения на устройство мозга.

-- 16.01.2016, 17:09 --

Речь не идет о надобности. Если есть возможность рассматривать мозг с этой стороны, то почему бы и нет?

[Anton_Peplov]

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

[maximk]

Если так, то странно. А он точно это имел в виду? И какой ему задали вопрос, что он вообще так ответил?

[Anton_Peplov]

А Вы сами посмотрите последние 15 минут видео.

[maximk]

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

[sqribner48]

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

[Anton_Peplov]

sqribner48 в сообщении #1107273 писал(а):

Но это не является доказательством правильности раскраски.

Продемонстрированное Матиясевичем "убедительство" доказательством в математическом смысле не является и не претендует на это. Лектор показывает лишь, как можно прийти к двум альтернативам: либо гипотеза верна, либо произошло событие, вероятность которого равна экспоненте в минус лохматой степени. Тогда можно сказать, что гипотеза подтверждается экспериментально. Здесь математика становится такой же экспериментальной наукой, как и физика.

sqribner48 в сообщении #1107273 писал(а):

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

Вы не обратили внимания на одну фразу: "способ раскраски графа - мое ноу-хау, я не хочу его показывать". Насколько я понял посредством легкого гуглежа термина "интерактивное доказательство", это метод, применяемый для проверки покупателем программных продуктов - когда надо, не раскрывая решения, убедить покупателя в том, что решение существует.
В математике, конечно, раскраску графа не надо менять, надо ее зафиксировать однократно и перебирать случайно выбранные вершины. Рассуждениям Матиясевича это не вредит, т.к. в случае фиксированной раскраски вероятность ошибки еще меньше.
Конечно, если перед нами граф из обозримого числа вершин, проще всего перебрать его полностью. Но, скажем, в теории Рамсея встречаются графы, число вершин в которых измеряется лохматыми степенями, для полного перебора категорически недоступными. Там метод "убедительства" может быть полезным.

[sqribner48]

Уважаемый Anton_Peplov

(Оффтоп)

Всегда с интересом читаю Ваши сообщения и сразу стараюсь отвечать.
К сожалению в период с 18.03.2016 по 22.03.2016 я был очень занят и сразу не смог ответить, а потом подумал, что может быть и не надо.

После Вашего поста я еще несколько раз прослушал лекции Вавилова и Матиясевича. К моему сожалению, из-за плохого качества звука я так и не смог расслышать некоторые вещи из лекции Матясевича, особенно в части перехода от «показательства» раскраски графа к доказательствам общего вида. Т.е. там, где он переходит от доказательства длины $n$ к доказательству длины $n\log n$ и к строке из нулей и единиц. Не совсем понял, как с помощью такой строки кодируется доказательство и откуда взялись эти 32 бита?
Очень прошу Вас, помогите мне в этом разобраться и, если Вам не трудно, напишите конспект лекции Матиясевича. (У Вас так здорово, четко, просто и наглядно получается). Мне кажется, это было бы не только помощью мне, но и достойным завершением темы.

Anton_Peplov в сообщении #1107277 писал(а):

Вы не обратили внимания на одну фразу: "способ раскраски графа - мое ноу-хау, я не хочу его показывать".

Все-таки мне не понятно, зачем надо скрывать конкретную раскраску? Разве это может быть секретом. Известно много алгоритмов и компьютерных программ для раскраски графов….
Если «способ раскраски» - это алгоритм, то мне тоже непонятно зачем его скрывать. Разработчики алгоритма обычно стараются его «застолбить» в литературе или другим способом.
Разумеется, тонкие детали реализации алгоритма могут быть скрыты.
Вы писали, что это применяется для презентации программ... Ну не знаю. Я когда-то сам и программировал, и даже один раз принимал участие в приемке, правда не самой программы, а результатов ее расчета (программа была разработана в другой организации). При этом, мы (т.е. органиция, в которой я работал) сначала ознакомились с алгоритмом программы, опубликованным в нескольких статьях и в книге, а потом подготовили свои исходные данные (в том числе и простые тестовые, с известными результатами расчета), и только потом нам по нашим данным вычислили результаты.
Может я не прав, но мне кажется, что приемка программы таким способом сродни покупке «кота в мешке». Потому, что остаются неизвестными разные ее особенности, "бяки" и "подводные камни".
Я тоже погуглил тему «интерактивное доказательство». Это огромное, интересное и многообещающее направление. И может быть, нам когда-нибудь повезет и на нашем форуме мы с помощью наших мастеров вернемся к этой теме.

(Оффтоп)

А вообще, что-то скучновато стало на форуме dxdy. Особенно после бессрочного бана Nataly-Mak.
А ведь действительно, bin больше не занимается проблемой изоморфизма графов (см. его посты «Полиномиальный алгоритм изоморфизма графов» и «Новость: задача GI имеет квазиполиномиальную сложность?»), Pulseofmalstrem больше не ищет партнеров для решения гипотезы Келли-Улама (см. post1113128.html#p1113128 ), а maximk больше не ищет какой бы великой проблемой чем ему бы заняться.
«Все ходят скучные. Директор магазин идет, мы его не замечаем, товаровед идет, мы на него пилюем.» Уважаемый Munin пишет - мы его не читаем (шутка конечно)…

[Anton_Peplov]

Уважаемый sqribner48
Спасибо за высокую оценку моих сообщений и моих конспектов.

sqribner48 в сообщении #1122001 писал(а):

Не совсем понял, как с помощью такой строки кодируется доказательство и откуда взялись эти 32 бита?

Откуда взялись эти 32 бита, Матиясевич не говорит. Он лишь упоминает, что такой результат есть, не уточняя, как он получен.

sqribner48 в сообщении #1122001 писал(а):

если Вам не трудно, напишите конспект лекции Матиясевича

Я подумаю над Вашей просьбой.

sqribner48 в сообщении #1122001 писал(а):

Вы писали, что это применяется для презентации программ... Ну не знаю.

Такое впечатление у меня сложилось после легкого гуглежа термина "интерактивное доказательство". Может быть, оно и неправильное, сам я от IT-бизнеса далек.

(Оффтоп)

sqribner48 в сообщении #1122001 писал(а):

А вообще, что-то скучновато стало на форуме dxdy.

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