Доказательства без слов.

[g______d]

Munin в сообщении #1310220 писал(а):

А вы могли бы пояснить

Munin в сообщении #1310220 писал(а):

- The first homotopy group of SO_3 has an order 2 element (that's a classic).

Роберт Асприн писал(а):

— А что касается этой фигуры, — показал Фрумпель на Квингли, игнорируя бесов, — то это ученик Гаркина. Именно он и занимался магией с тех пор, как извращенец потерял свои способности.
— В самом деле? — с энтузиазмом спросил Иштван. — Ты умеешь делать фокус с чашечкой и шариками? Я очень люблю его.

Но можно продолжить в той теме (ссылка внутри цитаты).

-- Сб, 05 май 2018 09:05:50 --

Munin в сообщении #1310220 писал(а):

- The surface area of a quarter of the unit sphere is Pi via Gauss-Bonnet (My source is Ariel Shaqed - it should have been a classic, but no one I asked seems to knew it). The sphere is what you reach with a straight hand while standing still. Hold a Pencil in your hand, that's your tangent vector. Now parallel transport the pencil on a quarter sphere: it points in the opposite direction. QED

Тут вроде в чистом виде теорема Гаусса-Бонне. Мы вычисляем сумму углов криволинейного двуугольника, стороны которого являются геодезическими. Её отклонение от нуля будет площадью соответствующего участка на единичной сфере.

[alcoholist]

Munin в сообщении #1310220 писал(а):

Цитата:

The pathspace of any topological space is contractible.

Pf (as given in my homotopy theory class): slurp spaghetti.

Конус стягивается к вершине.
На том же уровне доказывается, что высшие (и относительные) гомотопические группы коммутативны

[Munin]

g______d
Спасибо! Про первый факт знал, и даже картинку к нему приложил.

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

Тут вроде в чистом виде теорема Гаусса-Бонне.

А как она сама-то доказывается? Графически или оченьсложно?

[george66]

Вот пруфчекер Globular
https://golem.ph.utexas.edu/category/20 ... bular.html
и к нему статья про string diagrams
http://arxiv.org/pdf/1401.7220v2.pdf

[Dan B-Yallay]

Qlin в сообщении #1310256 писал(а):

Dan B-Yallay, а картинки требуются обязательно? Если нет, то посмотрите доказательства теорем на us.metamath.org. Они как бы тоже speechless.

Спасибо за интересную ссылку. Возможно, пригодятся позже.

[arseniiv]

Metamath тут оффтоп, у него другая цель: маленький пруфчекер, корректность которого просто проверить (и использование метапеременных — отюда meta в названии — и некоторые другие вещи). Это накладывает отпечаток на наглядность выводов теорем для человека. Можно быть уверенным, что выводы верны, коль скоро нет ошибок в нём, но следить за ними, даже имея такой хороший экспорт, не самое лучшее занятие.

-- Пн май 07, 2018 02:28:28 --

То есть, наглядность в целях там есть, но не та наглядность, которая имеется в виду тут.

[Dan B-Yallay]

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

То есть, наглядность в целях там есть, но не та наглядность, которая имеется в виду тут.

+1

[george66]

Там интересно, в Globular. Утверждения о категориях представляются в виде картинок (string diagrams), доказательство строится в виде последовательности картинок в графическом редакторе, а затем можно все картинки сложить стопочкой и получить изображение доказательства в виде трёхмерной фигуры -- узла. Если проделать шаги в обратную сторону, мы этот узел как бы распутываем. Придумали, что характерно, посторонние -- квантовые физико-математики (не из той тусовки, что пишет пруфчекеры).

[Dan B-Yallay]

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

Там интересно, в Globular.

А где там эта страница, ссылку можете сюда дать? А то поиск Globular по странице этого слова не находит.

[george66]

Не совсем понял, какая страница. Вот сам Globular, он работает в браузере
http://globular.science/

[Dan B-Yallay]

А, дошло. Так как перед этим контекст шел о Metamath, я подумал, что Globular - это что-то оттуда.