М.Двач / Математика

Двач.hk не отвечает.
Вы видите копию треда, сохраненную 13 июня в 14:30.

Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее

Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.

81 Кб, 480x360
ОПРОСИК Господа и дамы, сообщите хотя бы частичную 19 апр 2020, 16:42 67659 В конец треда | Веб

ОПРОСИК

Господа и дамы, сообщите хотя бы частичную информацию: когда, а главное - где и/или от кого вы узнали про homotopy type theory? Нужно отследить цепочку распространения заразы вплоть до нулевого пациента. (понятно кого)

Ответы6770967717677346774467852680457871879072

2 20 апр 2020, 00:07 2 67708

На двачах. Несколько лет назад, ещё когда не было этой доски и маттетреды были в /sci. От местного конструктивиста.

3 20 апр 2020, 00:34 3 67709

>>67659 (OP)
Что в ней плохого, объясните?

4 20 апр 2020, 00:39 4 67710

Учился на физика @ кафедра физики частиц @ хочу быть теоретиком @ КТП @ БРСТ @ когомологии @ топология...
Трактор @ хочешь остаться - давай считай количественный результат @ компьютер программировать @ Haskell @ Ocaml @ Coq @ Воеводский @ HoTT
Как-то так.

Ответы677296773167958

5 20 апр 2020, 07:46 5 67717

>>67659 (OP)
> (понятно кого)
Кого? Понятно кому?

6 20 апр 2020, 11:04 6 67729

>>67710
Эх, друже, после нормальной математики хаскелом занялся...

остальное - клёвые вещи, так держать

Ответы67731

7 20 апр 2020, 12:10 7 67731

>>67729
>нормальной математики хаскелом занялся
Почему математики такие высокомерные?

>>67710
А ты, физик, сам как считаешь, то что ты докатился до хаскеля, это деградация?

Ответы677326773367741

8 20 апр 2020, 12:36 8 67732

>>67731
>Почему математики такие высокомерные?
не увидел в его посте высокомерия, честно говоря
что нравится, тем и занимайся
но сравнивать хаскелл с математикой, скажем, брст вполне себе можно объективно
то, что она в разы или даже на целые порядки проще в первом случае, тебя волновать не должно, если тебя интересует эта область

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

9 20 апр 2020, 13:18 9 67733

>>67731
Хаскель это грааль теории категорий, которая в свою очередь является программироваем и второй культурой.

Ответы677346773667741

10 20 апр 2020, 13:28 10 67734

>>67733
>Хаскель это грааль теории категорий
Ну не то, чтобы там была какая-то особо замысловатая теория категорий.
>>67659 (OP)
Уже довольно давно (лет 8 назад), когда я учил логику.

11 20 апр 2020, 14:14 11 67736

>>67733
Что такое вторая культура?

12 20 апр 2020, 14:33 12 67738

Почему среди математиков так много верующих?

Ответы67740

13 20 апр 2020, 14:50 13 67740

>>67738
Если ты уже веришь в реальность вне-временных бесконечных объектов, что очень естественно для математиков, то почему бы еще не принять бога.

14 20 апр 2020, 14:51 14 67741

>>67731
>А ты, физик, сам как считаешь, то что ты докатился до хаскеля,

На самом деле я больше по Coq / OCaml, а не по Хаскелю.

> это деградация?

Соглашусь, что занятие теорией/математикой, так сказать, "на бумажке" -- это чуть более "возвышенная" деятельность, чем запрограммировывание пусть и того-же самого. С другой стороны, мне, как физику, приятно видеть как мои идеи реализовываются "в железе". Кроме того, у меня довольно хаотичное мышление - физически не могу исписывать 40 листовые тетрадки выкладками как некоторые коллеги. Компьютер помогает организовывать и проверять -- Coq мне находил пару нетривиальных ошибок в моих построениях.

Т.е. я бы на "это деградация?" ответил что это вопрос вкуса и личных предпочтений, но... Не знаю как оно у математиков, но среди физиков наблюдал неоднократно что навык программирования вызывает у многих чувство некоего такого испуганного раздражения. Особенно если автоматизировать какую-нибудь муторную символьную выкладку - могут почти открыто злиться на тебя. И вот это довольно сложно объяснить только тем, что это им "не интересно".

это >>67733 не я

Ответы677456774767751

15 20 апр 2020, 15:04 15 67744

>>67659 (OP)
>, а главное - где и/или от кого вы узнали про homotopy type theory?
Интервью с Воеводским.

16 20 апр 2020, 15:07 16 67745

>>67741
Просто пограмирование отвратительный аутизм и тупость, вполне понятно, что адеквату неприятно марать этим мозг.

Ответы67751

17 20 апр 2020, 15:24 17 67747

>>67741
Не понял, на что конкретно физики раздражаются и почему злятся на тебя?

Ответы67752

18 20 апр 2020, 16:05 18 67751

>>67745
>Просто пограмирование отвратительный аутизм и тупость, вполне понятно, что адеквату неприятно марать этим мозг.
Ты правда считаешь, что программирование хуже чем та деятельность, которую оно автоматизирует?

Как по мне, автоматизация нудных выкладок, о которой пишет >>67741, это безусловно позитивная вещь.

Ответы68371

19 20 апр 2020, 16:10 19 67752

>>67747
> на что конкретно
Деталей не хочу говорить, слишком деанон.

Пример 1: докладываю семинар @ вот модель, вот пара нетривиальных свойств модели, все формально доказано @ у дядечки вопрос "а вот если такой параметр то это контрпример" @ аlt-tab вбиваю параметр в конфиг, запускаю Coq @ за две секунды готово доказательство что все ок @ дядечка остался злой и недовольный.

Пример 2: есть несколько классов моделей, скажем A,B,C и у каждой параметр - натуральное число. Коллега взял модель B2, сказал, что она наиболее интересная из " соображений натуральности" и навыводил ее свойств, опубликовав статью с полотнами выкладок. Взялся делать то-же самое для С1. А тут я со своим Coq - вбиваешь класс модели и параметр - через секунду получаешь ту самую портянку со всеми доказательствами. Коллега со мной с тех пор не разговаривает.

> почему злятся на тебя?
Яж почем знаю...

Ответы67753677546777868210

20 20 апр 2020, 16:15 20 67753

>>67752
Похоже, высокоинтеллектуальные круги - тот еще гадюшник. Слышал, что шахматисты тоже люто, бешено ненавидят друг друга.

21 20 апр 2020, 16:18 21 67754

>>67752
Ради любопытства, в чем бонус Coq в такого рода деятельности? Казалось бы для обсчета моделей куда проще было бы использовать систему символических вычислений. Понятно, что так не получишь формального доказательства; но обычно в физике никто и не ставит таких критериев строгости. При этом получение именно формального доказательства вещь явно не бесплатная и требует кучи дополнительных усилий.

Ответы67755

22 20 апр 2020, 16:33 22 67755

>>67754
>Ради любопытства, в чем бонус Coq в такого рода деятельности?
Опять детали не скажу. Это специфика данной области теорфизики - тут Coq очень хорошо подходит.

Ответы67784

540 Кб, 680x621
23 20 апр 2020, 17:21 23 67762

Я правильно понимаю, что хейт в сторону кока и всего такого основан на суеверии, что на бумаге ручкой можно сделать больше, чем в коке, и типа как ручка с бумагой это высокий штиль, а кок - презренный бездушный быдлокодинг?

Ответы67765677676777367780

24 20 апр 2020, 17:48 24 67765

>>67762
Да

25 20 апр 2020, 18:01 25 67767

>>67762
Нет. Хейта к коку нет, есть хейт к его слепым последователям, которые утверждают, что маняматика нинужна и автоматизированные пруверы - будущее. У таких вот "экспертов" просто не хватает образования, чтобы понять, о чём вообще современная математика, но они её уже "решили".

Ответы67773

26 20 апр 2020, 19:57 26 67773

>>67762
Да, но большинство в этом не признается и будет рационализировать>>67767

Ответы67777

27 20 апр 2020, 20:41 27 67777

>>67773
В чем преймущество проверки на бумаге?

Ответы67778

28 20 апр 2020, 21:03 28 67778

>>67777
Тебеж >>67752 объяснил -- по статье в год на каждое натуральное число. И получ, что ты не хуйней страдаешь, а ресерч.

Ответы67779

29 20 апр 2020, 21:17 29 67779

>>67778
Это практическое виденье.
Я о тех кому и образование достает и денег не особо требуется. Что с ними не так?

Ответы67793

30 20 апр 2020, 21:20 30 67780

>>67762
Не на бумаге, а в голове.

Ответы67781

31 20 апр 2020, 21:47 31 67781

>>67780
> Не на бумаге, а в голове.
А что у тебя есть волшебного математического в голове, чего нет в математической нотации на бумаге? Особая уличная магия?

Ответы678716798679009

32 21 апр 2020, 03:29 32 67784

>>67755
> Это специфика данной области теорфизики
И что же это за область?

33 21 апр 2020, 07:20 33 67793

>>67779
> Я о тех кому и образование достает и денег не особо требуется. Что с ними не так?
Тут как с историей антисептиков в медицине. Врач Земмельвейс показал, что если мыть руки с хлоркой перед операцией, а не после, то внезапно смертность послеоперационных больных от сепсиса падает с 60% до 1-2. И что, его признали спасителем? Хуй там. Затравили, заруинили карьеру, позже вообще в дурку упекли. Потому что для абсолютного большинства светил медицины признать себя дебилом, не могущим в банальное мытье рук, хуже всего. Так и тут. ЧСВ важнее практических результатов, даже если речь о жизнях людей, про математику и говорить нечего. Кто сознательно откажется от высокопарных кукареканий о первой культуре и о чем-то волшебном в голове, чего нет в бездуховном коке? Да никто, это равносильно признанию себя дебилом.

Ответы67844

34 22 апр 2020, 06:27 34 67844

>>67793

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

Ответы67853

35 22 апр 2020, 12:35 35 67852

>>67659 (OP)
недавно какой то пидорас рассказал про неё. Он хоть и пидорас, но вдруг что то полезное говорит. А что, в чём проблема этой homotopy type theory?

36 22 апр 2020, 12:36 36 67853

>>67844
Но есть ли у тебя хоть какие-нибудь истории успеха в математике, когда во время попытки формализации поймали существенную ошибку? Т.е. не просто какую-нибудь техническую лемму, которая была сформулирована в излишней общности, когда она уже не верна, но общий ход доказательства от этого не страдает. А вот, чтобы было что-то не так с какой-то важной теоремой, которой действительно пользовались другие математики.

Если нет, то все о чем ты говоришь - это чисто спекулятивная польза. Но при этом ты предлагешь вкладывать в это очень реальные усилия.

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

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

Ответы678556785767943

37 22 апр 2020, 12:52 37 67855

>>67853
>Но есть ли у тебя хоть какие-нибудь истории успеха в математике
Для этого надо знать математику, лол

38 22 апр 2020, 13:10 38 67857

>>67853
> Но есть ли у тебя хоть какие-нибудь истории успеха в математике, когда во время попытки формализации поймали существенную ошибку?
Есть. Заповедью исключенного третьего и актуальной бесконечности пользовались веками, пока Брауэр не показал, что это просто когнитивные искажения, и основывать на них точные знания - ошибка.

Ответы67867678706787467875

39 22 апр 2020, 15:04 39 67867

>>67857
>пока Брауэр не показал
"Показал"? Ты сделал ошибку в слове "заповедовал".

Ответы67871

40 22 апр 2020, 15:56 40 67870

>>67857
Верую в тезис Цервки, ем Карри, сижу в Браузере ;)

Ответы67871

41 22 апр 2020, 17:59 41 67871

>>67867
>>67870
Ну-ну. А по факту как всегда ни одного ответа по существу, например на >>67781 , одна анальная клоунада. Ничего нового, одна попаболь одного еблана от HoTT итд...

Ответы6787267874

103 Кб, 240x168
42 22 апр 2020, 18:14 42 67872

>>67871
А прогреры уже запрогали ГоТТ так, чтобы он в Браузере работал? Или надо себе приложение на комп качать?

43 22 апр 2020, 18:17 43 67874

>>67871
Так что оказывается >>67857 был не стеб. Лол.

44 22 апр 2020, 18:18 44 67875

>>67857
>пока Брауэр не показал
ВЕРУЮ ИБО ЗАВЕЩАНО

45 22 апр 2020, 18:31 45 67876

Заметил интересный паттерн - все (трое), кто с моей кафедры впоследствие заинтересовались HoTT и пруверами, на первом курсе пытались записывать лекции через латех и ебню вроде vim на своём нетбуке-хуюке. Так что эта болезнь выявляется на ранней стадии.

Ответы6787867935

445 Кб, 604x405
46 22 апр 2020, 18:48 46 67878

>>67876
Будем знать. Поскорей бы выпустили версию ГоТТ для Браузера.

Ответы67879

47 22 апр 2020, 18:57 47 67879

>>67878
Откуда тяночька?

Ответы67880

48 22 апр 2020, 19:09 48 67880

>>67879
Хз. Нашел в гугл-пикчах.

49 24 апр 2020, 00:22 49 67935

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

50 24 апр 2020, 10:40 50 67943

>>67853

Я истории успеха не искал и наверное их не так просто найти.
Сужу по себе: без формализации меня бы математике не научили бы никогда, потому что формат "прочёл книгу -- понял", или тем более "лектор сказал-- студент записал и вызубрил" не работает. Нет глубины необходимой.

А с верификацией оно проще будет. Сколько раз находил интересные тонкие, но важные подробности казалось бы уже известных мне теорем, без которых знание было бы искажено.

Ответы67946

51 24 апр 2020, 12:16 51 67946

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

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

Ответы6794768372

52 24 апр 2020, 12:30 52 67947

>>67946
> обычный математик просто спросит на кафедре
Рассмешил... Это ты траллишь так, да? Да?

Ответы6795067953

53 24 апр 2020, 13:12 53 67950

>>67947

Да не, он не троллит, он просто токсичный долбоёб, который ни одной теоремы не доказал, но имеет "очень ценное мнение".

Ответы67956

54 24 апр 2020, 16:51 54 67953

>>67947
Нет, это правда. Математик без общения это не математик, а калека, фрик. Ни один успешный математик еще не жил без общения в среде.

Ответы6795467957

55 24 апр 2020, 16:55 55 67954

>>67953
Так вот почему во всех книгах по математике подача материала напоминает бред шизофреника.
Надо просто в той же среде крутиться, что и автор.

Ответы67956

56 24 апр 2020, 18:12 56 67956

>>67954
>во всех книгах по математике
>бред

>>67950
>токсичный долбоёб,

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

>>67950
>токсичный
Уябывай уже на реддит, и strawman свой захвати.

Ответы67959

57 24 апр 2020, 18:15 57 67957

>>67953
А ну так сразу видно почему вашему брату пруверы не нравятся. Так ты "успешный математик" крутящийся в элитарных кругах, который если что может "просто спросить на кафедре". А тут оказывается что можно git clone все доказательства, и ценность всех твоих социальные элитосвязей внезапно сильно уменьшилась.

Ответы6796967973

58 24 апр 2020, 18:19 58 67958

>>67710
Правильно ли я понимаю, что когда мы дотрагиваемся до стены, то молекулы нашего пальца начинают взаимодействовать с молекулами стены, обмениваясь на бешеной скорости кварками, и из за этого палец не пролазиет в стену?

59 24 апр 2020, 18:21 59 67959

>>67956
неосиляторов,лол. чего я по-твоему не осилил?

Ответы67960

60 24 апр 2020, 18:24 60 67960

>>67959
Пучки на многообразиях, K-теорию, теорию Ходжа.

Ответы67963

61 24 апр 2020, 18:54 61 67963

>>67960

Слушай, ну всё, прямо уел меня, не спец я в К-теории, ну разве что могу когомологии де рама посчитать на многообразиях.

Если ты специалист, то зачем это нужно, какие проблемы решает? Может быть действительно стоит изучить

62 24 апр 2020, 20:23 62 67969

>>67957
>тут оказывается что можно git clone все доказательства, и ценность всех твоих социальные элитосвязей внезапно сильно уменьшилась.
Я эти маняфантазии уже сотый раз слышу, но вот на практике почему-то всё наоборот и в точности как говорит анон выше.

Ответы679716797267975

63 24 апр 2020, 21:17 63 67971

>>67969

А ты типа идеалист и надеешься на успешность и адекватность присутствующих? Кто из нас в итого ебобо?:)

64 24 апр 2020, 21:22 64 67972

>>67969

Тем временем ты не говоришь какие проблемы решает твоя область математики. Кто её у тебя купит? (Даже чисто гипотетически)
На пруверах можно программы верифицировать, в том числе квантовые, а твоя теория ходжа и к теория ну куда её. Диффуры решать на многообразиях? А их кому продавать?

65 24 апр 2020, 21:32 65 67973

>>67957
Доказательства везде написаны, интуицию за ними тебе никто просто так не даст. Вполне может быть, прочитал ты и не понял. Открой, например, доказательство Перельмана. Что будешь делать? Читать до посинения?

66 24 апр 2020, 22:15 66 67975

>>67969
>анон выше
А чего тогда вы вместе с "аноном выше" и ОПом кудахчете так на пруверы? Ну бегают там хипстеры-программисты-аутисты какие-то, в отличие от вас, элитарных, доступа к "спросить на кафедре" не имеют. Толку от этих ваших пруверов нет - тру математика только "на кафедре". Ну и хрен бы с ними?

67 25 апр 2020, 01:32 67 67986

>>67781
На бумаге вообще ничего нет.
По определению понимания (какому бы то ни было, несуществующему), понимание --- это то, что происходит у тебя в голове.
Человек --- мера всех вещей.
И именно это понимание и является первичным объектом, а определения теоремы доказательства --- вторичным, производным.

На верификацию вообще всем насрать, кроме фриков. Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.

Ответы67987679896805868106

62 Кб, 555x400
68 25 апр 2020, 08:05 68 67987

>>67986
> На бумаге вообще ничего нет.
> По определению понимания (какому бы то ни было, несуществующему), понимание --- это то, что происходит у тебя в голове.
> Человек --- мера всех вещей.
> И именно это понимание и является первичным объектом, а определения теоремы доказательства --- вторичным, производным.
Охуеть, откровения какие. Ещё несколько лет, глядишь и до интуиционизма додумаешься. А вот суть формализма как раз в том, что все нужное - на бумаге, и зависит только от непротиворечивости используемой аксиоматики. От головы в данном случае зависит только выбор аксиоматики, какой набор заповедей больше зайдет - ZFC там, NBG итд. Гедель, правда, доказал что это для оснований не подходит, да и ладно, хуй с ним.

Ответы68032

69 25 апр 2020, 09:12 69 67989

>>67986
> На верификацию вообще всем насрать, кроме фриков. Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
Ну да, во всякой прикладухе так и есть. Сантехнику не нужна физика, гамалогии можно трясти без оснований.

Ответы6799468110

70 25 апр 2020, 11:36 70 67994

>>67989
Да, вот на этой процитированной фразе, а также на вопросе "чьи проблемы твоя область решает, кроме твоих", тот анон явно сливается.

71 25 апр 2020, 20:33 71 68032

>>67987
Вот именно, ты прав. Надо больше писать всяких доказательств, брошюр, книжек, чтобы это было доступно большему количеству людей, в разных форматах, а не только "от человеку к человеку".

72 26 апр 2020, 00:14 72 68045

>>67659 (OP)
Узнал из чатика, где обсуждают теорию типов.
Сохацкий активно HoTT пропагандирует.

73 26 апр 2020, 15:08 73 68058

>>67986
ну что, ушёл с седовласыми старцами на кафедру советоваться?

Ответы68113

74 28 апр 2020, 02:54 74 68106

>>67986
> Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
Ну что это такое?

Ответы68111

75 28 апр 2020, 11:24 75 68110

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

76 28 апр 2020, 12:10 76 68111

>>68106
он имел в виду, проверять, верен ли доказанный кем-то результат, который проверен "авторитетами", с существующим консенсусом...

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

Ответы6811268113

77 28 апр 2020, 13:05 77 68112

>>68111
лол

78 28 апр 2020, 14:14 78 68113

>>68111
Нет, я имел в виду, что "факт" истинности или ложности того или иного математического утверждения сам по себе не имеет ни ценности, ни смысла. Допустим, гипотеза Римана верна или не верна --- какая разница? Тебе лично не плевать?
Любое утверждение можно принять в качестве аксиомы, т.е. сделать его верным или неверным по своему желанию.
Слишком большой фокус на "да/нет" аспектах --- это аберрация , являющаяся следствием принятой сейчас системы преподавания, а не какой-то глубокий факт.
Противопоставляя компьютерную верификацию "работе по старинке", многие подменяют первичную ценность вторичной.
Хотя, если считать компьютер продолжением мозга, то всё нормально. Но это получается киборг, а не человек.
>>68058
Я не он, если что.

Ответы68114

89 Кб, 512x512
79 28 апр 2020, 14:27 79 68114

>>68113
> Нет, я имел в виду, что "факт" истинности или ложности того или иного математического утверждения сам по себе не имеет ни ценности, ни смысла.
Математике это по своей сути точное знание. На голландском буквально - wiskunde. Факт истинности или ложности утверждения это сама суть математики, вне которого ее просто нет. Отсюда и проблема оснований - что именно считать истинностью в математике.
> Допустим, гипотеза Римана верна или не верна --- какая разница? Тебе лично не плевать?
То что ты описываешь - уровень пикрелейтед.

Ответы6811868129

80 28 апр 2020, 18:43 80 68118

>>68114
>На голландском буквально - wiskunde.
А на ацтекском - Tlapōhualmatiliztli.

Гипотеза Римана не интересна по той причине, что существуют десятки эквивалетных ей утверждений и все эти утверждения формулируются очень просто; утверждения же, которые вытекают из гипотезы Римана обычно очень сложные и содержат в формулировке пространства Харди и прочее.

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

Ну а кроме того, гипотеза Римана уже доказана Делинем в 1974-м еще.

Ответы68119

81 28 апр 2020, 19:35 81 68119

>>68118
>Ну а кроме того, гипотеза Римана уже доказана Делинем в 1974-м еще.
Жаль что кроме тебя этого никто не знает.
>что гипотезу Римана следовало бы принять за аксиому
Верую, ибо блаженен.

Ответы6812068121

82 28 апр 2020, 20:27 82 68120

>>68119
https://youtube.com/watch?v=GSQYzzRrnzk

83 28 апр 2020, 20:39 83 68121

>>68119
>Верую, ибо блаженен.

Я могу сказать про тебя то же самое, ты похоже веруешь в объективные истины из мира идей или откуда еще, и считаешь что математикам принципиально важно знать истинно ли данное утверждение в абсолютном смысле, или нет. Из разряда новостей в популярных журналах типа "ALL MATH MAY BE WRONG, Researcher said".

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

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

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

Ответы6812568129

84 28 апр 2020, 22:03 84 68125

>>68121
> Когомологии, схемная алгебраическая геометрия, К-теория и т.д. имеют гигантское количество приложений, Делинь, Гротендик, Артин, Мамфорд и прочие действительно ближе к сантехникам, как тут выразились, чем к фуфлософам-пиздаболам с их объективными истинами, трансцендентальными единствами, тезисами Черта и проч.
Пынямаешь ли, все что ты перечислил, вовсе не висит где-то в пустоте. Это следствия развития математической мысли, следствия, к которым привели даже не столетия эволюции самых разных математических и не только идей, методов итд. И тот подход, который ты вычитал у Вербицкого, он в точности соответствует пикрелейтед номеру "тут играем, тут не играем, тут вообще рыбу заворачивали". И.е предлагается что-то сыграть не только в отрыве от всего контекста, но и принципиально игнорировать вопрос, откуда все это вообще пошло и в чем природа всего этого. В принципе, такой подход имеет право на существование, но с определенными оговорками, которые ваша секта принципиально не принимает. Практическая применимость чего-то как критерий истины это хорошо и правильно, но принимать это не как функциональный контекстуализм, а как нечто висящее в воздухе и данное нам непонятно кем и нахуя, это сектантство.

Ответы681616816268163

672 Кб, 1403x988
85 29 апр 2020, 02:43 85 68129

>>68114
>Факт истинности или ложности утверждения это сама суть математики, вне которого ее просто нет.
Вообще-то это ниоткуда не следует.
Сами по себе понятия истинности и ложности могут оказаться не совсем тем, что надо ставить в основания.
Т.е. настоящие основания должны основываться на каких-то других концепциях (каких --- не знаю), а понятия "истинности" и "ложности" --- выводиться из них. Грубо говоря.
>То что ты описываешь - уровень пикрелейтед.
Наполовину прикалываюсь, наполовину серьёзен.
Возможно, если математик начнёт серьёзно рефлексировать, изучать свои мысли и побуждения, то что-то из этого он сможет извлечь.
>>68121
>Люди, всерьез интересующиеся основаниями, это люди которые не понимают что такое вообще математика, где и зачем она нужна.
Громкое заявление.
А слова о фуфлософии и оскорбительные, и смешные. От любителя "схемной алгебраической геометрии", у которой приложений в жизни... сколько? Для любого нормального человека ты сам пиздабол.

Ответы68177

86 29 апр 2020, 15:45 86 68161

>>68125
>функциональный контекстуализм
охуенно, прямо как у Гермиды и Якобса, синоним декартовой замкнутости

87 29 апр 2020, 15:49 87 68162

>>68125
а напомните нам нахуя нам 87-я гомотопическая группа трехмерной сферы ?

Ответы68325

88 29 апр 2020, 15:56 88 68163

>>68125
> фуфлософам-пиздаболам
Погоди-ка. Это что-же получается, "пыняпучк" юродидый с /math/ и "философсмолин" пиздобол с /sci/ - одна и та-же личность? Кто бы мог подумать?

89 29 апр 2020, 18:44 89 68165

господа, вы правы лишь частично

1) не надо смешивать а) верификацию, как стремление к абсолютной строгости доказательств вместе с б) радикальным интуиционизмом/конструктивизмом. Поверифицировать можно отлично и классические доказательства.

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

Ответы68166

90 29 апр 2020, 19:50 90 68166

>>68165
Пучки нужны даже палочкосчитателям и N-петухам для построение пресловутого функционального контекстуализма, у них там современная теория типов на предпучках строится и есть расширенная теории типов, где вместо категории множеств берутся категории групоидов, и таким образом переходят в престек теорию типов, где вместо сигмы конструкция Гротендика. Те еще наркоманы.

Я за модульного деда если что, но мне кажется, что вы тут попутали понятия верификации и нормализации. Вот скажем вы можете верифицировать свои группы сфер (если построите конечно, а то выше четвертой группы никто не построил еще даже для первых трех измерений), но нормализовать терм уже не сможете, нужно изобретать механизмы оптимальной редукции, новая открытая проблема). А так когомологии элиптические, циклические, хуические, этальные, халяльные — все это изи чекается уже пару лет как. Этальные кстати если записать в HoTT будут самыми красивыми.

Ответы68168

71 Кб, 850x400
91 29 апр 2020, 22:40 91 68168

>>68166
> Пучки нужны даже палочкосчитателям и N-петухам для построение пресловутого функционального контекстуализма, у
Зачем? Все это прекрасно строится без всяких пучков.
> А так когомологии элиптические, циклические, хуические, этальные, халяльные — все это изи чекается уже пару лет как. Этальные кстати если записать в HoTT будут самыми красивыми.
Все дело в том, что при желании это все работает в обеих направлениях. Гамалогии можно представить в HoTT, а можно и наоборот. Всяческие вербитодрочеры веруют только во швятые гамалогии, а все остальное в их религии даже не математика. Тогда как на самом деле все сложнее. И HoTT и гамалогии, и много чего другого - это просто языки, вторичные по отношению к собственно математическому мышлению. Потому что если это не принимать, тогда придется принять, что вся математика существует только на бумаге, а роль человека - трясти синтаксис. Либо остаётся совсем уж религия - платоновский мир идей, актуальная бесконечность, исключенное третье и прочие подобные догмы, заповеди. Можно скатиться ещё дальше, до высказываний Манина о том что "математика подвешена в воздухе". Но это уже уровень патриота, который сидя за американским компьютером с американским по, пишет в американском интернете, какие пиндосы пидоры.

Ответы6817068176

92 29 апр 2020, 22:55 92 68170

>>68168
>Зачем? Все это прекрасно строится без всяких пучков.
Строится без пучков, но с пучками выглядит компактнее. Там много изоморфизомов моделей теории типов: Категории с семействами (CwF), категории с аттрибутами (CwA), Воеводский делал С-системы, потом поняли, что это все поебота, выдуманная людьми и перешли на гротендиковский пучкизм в французском стиле. Кубическая теория типов стала записываться одной формулой: I: <sup>op</sup> → Set. Пи и сигма тоже в пучках формулируется, как функториальная смена базы, вернулись к Лавировской классике.

Ответы68171

93 29 апр 2020, 23:00 93 68171

>>68170
Это хорошо, что пока только модульный дед атакует, а придут спросят как Стекс Проджект закодировать и что мы будем делать, мычать? Нет, мы готовы уже модальную престек теорию типов предоставить на конструкциях Гротендика --- такая основная мотивация пучкизма в теории типов, ублажить высших сантехников и более консистетно подойти к основаниям, чтобы они могли все в себя вобрать.

94 30 апр 2020, 01:20 94 68176

>>68168
>Все дело в том, что при желании это все работает в обеих направлениях.
нихуя не работает. Пока что выходит лишь записать тривиальные результаты 50-60х, при этом 90% времени тратится на формализмы, вместо математики. Приход программистов в математику ничего хорошего не дал в итоге, вместо решения реальных задач бесконечные новые формализмы.

Ответы68178

95 30 апр 2020, 01:26 95 68177

>>68129
>От любителя "схемной алгебраической геометрии", у которой приложений в жизни... сколько?
ну тупые, не знали, что надо очередной модный фреймворк оснований учить
https://press.princeton.edu/books/hardcover/9780691102887/algebraic-geometry-in-coding-theory-and-cryptography
https://en.wikipedia.org/wiki/Numerical_algebraic_geometry
https://arxiv.org/abs/math-ph/0011038

Ответы68182

96 30 апр 2020, 01:34 96 68178

>>68176
в каком то смысле это хорошо, потому что тогда математика сводится к медалистам Филдса. Математики могут успокоится, задача программистов не забирать их медали, а провести рефакторинг всей математики, очень неблагодарная но интересная деятельность. Задача оснований --- строить эффективные вычислительные модели или предлагать новые специализированные синтаксисы для каждого вида математик.

Ответы68179

97 30 апр 2020, 01:40 97 68179

>>68178
> задача программистов не забирать их медали, а провести рефакторинг всей математики
Нельзя провести "рефакторинг" не зная что ты собственно рефакторишь. А уровень знания математики у программистов нулевой.

Ответы6818068188

98 30 апр 2020, 01:41 98 68180

>>68179
Ну когда я говорю программисты я подразумеваю Воеводского. А ты очевидно подразумеваешь своего студента имбецила, который сайт кампуса на ПХП пишет.

Ответы68181

99 30 апр 2020, 02:00 99 68181

>>68180
> А ты очевидно подразумеваешь своего студента имбецила, который сайт кампуса на ПХП пишет.
Речь скорее о ncatlab, о любителях пруверов и функционального программирования. Воеводский был жемчужиной среди всего этого сброда, с реальными математическими результатами в прошлом.

Ответы6818368185

100 30 апр 2020, 02:01 100 68182

>>68177
> приложений в жизни
> two-dimensional exactly solvable statistical lattice models and its related Hamiltonians

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

Ответы68186

101 30 апр 2020, 02:03 101 68183

>>68181
ncatlab и ведется студентами, я сам плачу студентам за статьи на ncatlab, это студенческий образовательный проект. Ты воюешь с ветряными мельницами.

Ответы68195

102 30 апр 2020, 02:07 102 68185

>>68181
Воеводский был жемчужиной, а прувер написать не смог. Зато медаль получил, за пофиксаного Блоха-Като, рефакторер блядь. С-системы его ёбнутые. Ты реально переоцениваешь математиков.

Ответы79160

103 30 апр 2020, 02:20 103 68186

>>68182
Уайлс за комп не пересел, до сих пор на бумажке считает. Или ты про того, который стал с шумом радио общаться?

Ответы68187

104 30 апр 2020, 02:22 104 68187

>>68186
Нет, я ж не атакую, я ж признал, что нового не умеем производить, все что можем --- это по крупицам собирать то, что математики напридумывали используя их же методы, языки и модели. Вот и все. Да имбицильство, но оно качает, и тенуре нам не нада.

Ответы68193

105 30 апр 2020, 06:03 105 68188

>>68179
> Нельзя провести "рефакторинг" не зная что ты собственно рефакторишь. А уровень знания математики у программистов нулевой.\t
Ага, а математика это согласно вашим сектантстким заповедям что?

Ответы68190

106 30 апр 2020, 08:49 106 68190

>>68188
>Ага, а математика это согласно вашим сектантстким заповедям что?
Я не очень понимаю, на что постоянно погромисты обижаются. Ну вот Многие дисциплины просачиваются в другие области будь то humanities или естественнонаучные или инженерные, это нормально. Но глупо полагать, что в 21м веке ты можешь достичь хорошего понимания современных достижений в нескольких дисциплинах.

SVD, численное решение урчп, градиентные спуски, 3Д моделирование и кватернионы, Монте-Карло, FFT, поиск группы автоморфизмов для решения какой-нибудь хитровыебанной задачи из линейной оптимизации - это не современная математика. Это всё важные вещи, они могут часто использоваться, они полезны. Но с точки зрения математики этим идеям лет 200 минимум.

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

Это не какая-то профессиональная спесь. Просто в "простонародье" математикой и матаном называют всё, что сложнее обычного умножения. Если же мы говорим про пруверы и соответсвенно теоремы, то есть совершенно чёткая область чистой математики. Порог вхождения в современную актуальную чистую математику настолько высокий, что 99.9999% программистам дорога туда заказана.

Поэтому все громкие утверждения насчёт важности пруверов серьёзно просто не воспринимаются из-за совершенной некомпетентности собеседников. Это уровень ферматистов и навьестоксеров.

Ответы6819168196

107 30 апр 2020, 09:08 107 68191

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

Ответы6821174897

108 30 апр 2020, 09:28 108 68193

>>68187
золотые слова

единственное что дополню -- может быть верификация -- это способ изучения математики для тех, кому не повезло оказаться в нужной среде в нужное время? Это я типа про себя...

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

Да, С-системы Воеводского нужны были для модели его теории типов. Но она вроде сильно специализированная какая-то, конструктивая в каком-то смысле. А это значит, что классическую математику в ней не подоказываешь. (Ну может есть какой-то хитрый способ?) Ае сли не подаказываешь, то тогда разве это "основания математики"? Получается, что нет. Или что с точки зрения адептов hott, настоящей(тм) алгебре "не нужна" аксиома выбора? Все учебники переписывать? На конечных объектах -- может быть, ну а если чуть сложнее что...

Ответы6819768198

109 30 апр 2020, 09:50 109 68195

>>68183

я человек простой: слышу про математику и деньги -- пишу свою фейкотелегу: puchkist

110 30 апр 2020, 10:22 110 68196

>>68190
А что такое современная математика, и можно ли ее где-нибудь применить? Или она такая ЧИСТАЯ, что нигде не применяется?

111 30 апр 2020, 10:39 111 68197

>>68193
> классическую математику в ней не подоказываешь. (Ну может есть какой-то хитрый способ?
Способ ровно тот же самый, что и в классической математике - без задней мысли берешь и прописываешь нужную заповедь. И о чудо, можно её использовать для "доказательства".

Ответы6820274897

112 30 апр 2020, 11:00 112 68198

>>68193
>Да, С-системы Воеводского нужны были для модели его теории типов. Но она вроде сильно специализированная какая-то, конструктивая в каком-то смысле.

С-системы точно такая же копипаста как и CwF, CwA, только Воеводсткий использовал категории, объекты которых индексированые натуральными числами. В те времена еще не было модальной HoTT поэтому теории связанных топосов Ловира еще не было в пруверах, поэтому ясно что что в С-системах этальная математика не чекается. C-системы это изоморфизм universe categories.

Ответы68199

113 30 апр 2020, 11:02 113 68199

>>68198
Нет никакой его теории типов. Есть теория типов и в рамках ее DIY модели, все равноправные. Кто больше математики в своих моделях закодирует тот и победил, это и будет показателем эффективности испольования прувера.

Ответы68200

114 30 апр 2020, 11:05 114 68200

>>68199
С-системы как и все основание построенное Воеводским просто зажигало ребят вокруг за это ему спасибо, а так же теорию типов для своей же унивалентности Воеводский построить не смог. Построили программисты, так что спесь не то что с модульного деда, но и с лауреатов Филдса можно сбить при желании.

Ответы68201

159 Кб, 700x487
115 30 апр 2020, 11:11 115 68201

>>68200
> теорию типов для своей же унивалентности Воеводский построить не смог. Построили программисты, так что спесь не то что с модульного деда, но и с лауреатов Филдса можно сбить при желании.
Мне меньше всего понятно, почему эти вещи вообще противопоставляются. Вот если отбросить сектантскую швятую веру уровня того, что креститься нужно не тремя, а двумя пальцами писать нужно на бумаге, а не в прувере, то какие аргументы остаются против HoTT?

Ответы682046820674897

116 30 апр 2020, 11:12 116 68202

>>68197
насколько я помню, если прописать аксиому выбора -- получишь противоречие с аксиомой унивалентности.

Ответы6820381743

117 30 апр 2020, 11:13 117 68203

>>68202
Ну и что? Чекаться-то будет, что ещё нужно.

Ответы6820574897

118 30 апр 2020, 11:15 118 68204

>>68201
Аргумент против HoTT см выше, для неё надо передоказывать все теоремы и неизвестно, содержится ли в ней модель ZFC.

119 30 апр 2020, 11:15 119 68205

>>68203
Тогда чекаться будет любая теорема, что неинтересно. Ex falso quodlibet

Ответы68208

120 30 апр 2020, 11:17 120 68206

>>68201
Сейчас пруверы - бесполезное говно для 1,5 аутистов. Но если дать всей этой теме ход, то сразу появятся кабанчики, которые сверстают "нормальный прувер" и попросят бабки за его использование. Это подтолкнет журналы не принимать пруфы не заапрувленный пруверов от ООО Кабанчик Инт. Ну а дальше смерть и вырождение математики.

Ответы682076820868220

121 30 апр 2020, 11:18 121 68207

>>68206
Это очень оптимистичная программа, но я бы под ней подписался!

122 30 апр 2020, 11:25 122 68208

>>68205
В классической математике это никого не останавливает почему-то.
>>68206
Вот честно, бред какой-то уровня "аргументов" керосиновых магнатов против елестрического освещения.

Ответы682096821574897

123 30 апр 2020, 11:28 123 68209

>>68208
>Вот честно, бред какой-то уровня "аргументов" керосиновых магнатов против елестрического освещения.
Компьютиризация убивает искусство. И да компьютер есть и всегда будет беспросветно тупым.

Ответы6821268240

124 30 апр 2020, 11:30 124 68210

>>67752
Ахуительные истории.

125 30 апр 2020, 11:33 125 68211

>>68191
>гамалогиях
Кроме этого слова больше ничего про "современную" математику не знаешь? Идее гомологий уже больше ста лет, а Э-С аксиомам уже лет так 70. Гомологии проходят на первых курсах, если что.
Вот классический пример - не знаю, о чём говорю, но буду прятаться за мемами вроде пучков и гамалогий, авось проканает и это поднимет авторитетность моего программистского мнения. Ну с этим иди в /sci/.

Ответы68212

126 30 апр 2020, 11:35 126 68212

>>68211
Ты ж сам видишь, что по существу того поста не возразил. А все "аргументы" против свелись к >>68209

Ответы6821368231

127 30 апр 2020, 11:39 127 68213

>>68212
Ты думаешь взяв "аргументы" в кавычки ты снизишь их значимость? Ну так, мой дорогой, в таком случае твои "аргументы" говно из жопы, как тебе такое?

Ответы68214

128 30 апр 2020, 11:48 128 68214

>>68213
Значимость чего? Рандомных, ни на чём не основанных заявлений, что типа "буковы в прувере в отличие от таких же буков на бумаге - это не искусство"? Так у подобных заявлений и так никакой значимости нет, как я могу ее дальше снизить?

Ответы68216

129 30 апр 2020, 11:51 129 68215

>>68208
Давай, если такой умный, строго докажи, что ZFC противоречива, верифицируй в любом прувере: гарантировано получишь премию Абеля.

Ответы68217

130 30 апр 2020, 11:51 130 68216

>>68214
Просто иди нахуй.

53 Кб, 624x433
131 30 апр 2020, 12:02 131 68217

>>68215
Ну либо противоречива, либо нет. Ты ж не против использования исключенного третьего в доказательстве? Тогда я считай доказал.

Ответы6821868219

132 30 апр 2020, 12:18 132 68218

>>68217
не смешно

133 30 апр 2020, 12:22 133 68219

>>68217
А он вообще кто таков?

134 30 апр 2020, 12:28 134 68220

>>68206
я думаю вольфрам вскоре придет к пруверам

Ответы68237

135 30 апр 2020, 14:09 135 68231

>>68212
>Ты ж сам видишь, что по существу того поста не возразил
Хорошо, давай по существу. Раз ты у нас охуенно какой математик, то тебе ничего не стоит отвечать по существу, верно? Так что я ожидаю развёрнутых ответов с пруфцами, а не балабольство и демагогию. Это всё-таки /math/, а не /pr/.

Хорошо известно, что вокруг доказательства гипотезы Пуанкаре было немало драмы из-за сказанного/напечатанного Яу, Цао, и Джу. В частности, они намекали, что доказательство Перельмана не полное. Позже это утверждали и другие (статья Моргана-Тяня, книга Бахри).

1) Могут ли пруверы (существующие на сегодняшний день) показать (однозначно), были ли пробелы в доказательстве? Как/почему нет?
2) В первой архивной статье Перельмана на эту тему он получает неравенства типа Гарнака, интегрируя неравенство Ли-Яу, и в получившихся геометриях (точнее, в одной оптимальной) считает геодезические.
Вопрос - могут ли пруверы показать, какие из этих результатов (в частности, аналог теоремы Бишопа-Громова) уже автоматически следовали из статьи Ли-Яу? Как/почему нет?
2) Могут ли пруверы показать, есть ли пробелы во второй архивной статье Перельмана, а именно в исследовании поведения решений для времени много большего времени "хирургии"? Как/почему нет?
3) Могут ли пруверы показать, корректно ли доказательство конечности времени вымирания (вторая статья)? Как/почему нет?
4) Могут ли пруверы выявить неэквивалентные утверждения между статьями Перельмана и Цао-Джу (особенно раздел 7.6 последней, включая результат о поведении потоков Риччи с хирургией на бесконечности)? Как/почему нет?

Жду демагогию, односложные ответы, мемы, шутейки, и увиливания.

Ответы6823468235682366824168275

136 30 апр 2020, 15:06 136 68234

>>68231
Может ли бумага доказывать теоремы?

137 30 апр 2020, 15:08 137 68235

>>68231
О, чувствую шизоидное обострение у модульного деда!

138 30 апр 2020, 15:10 138 68236

>>68231
Нужно нейронку, которая могла бы челотекст переводить в нагромождение логической поебени и потом уже этот километр текста скармливать пруфчекеру.

139 30 апр 2020, 15:23 139 68237

>>68220
Вольфрам знает математику еще меньше чем основатели, а теорию языков программирования вообще не знает.

140 30 апр 2020, 15:36 140 68240

>>68209
Ага, это сразу видно по бюджетам в области искусства и компьютерной графики.

141 30 апр 2020, 15:47 141 68241

>>68231
я не он, но отвечу тебе, раз уж ты такую пасту напечатал.

Всё, что может быть доказано, может быть доказано как "на бумаге", так и на компьютере. Я сам и так, и так спокойно доказываю.

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

Поэтому на вопрос "могут ли" ответ: да. Тебе придётся долго писать пруф, но в итоге , если твои интуитивнве рассуждения верны, то получится

Ответы68242682486826268275

142 30 апр 2020, 15:49 142 68242

>>68241
Да модульному деду уже преподали теорию типов на пучках и конструкциях Гротендика, если это не помогло, то остальное вряд ли поможет.

Ответы68243

143 30 апр 2020, 15:50 143 68243

>>68242
Пусть подоказывают еще 100 лет на бумажке, а дальше будет без вариантов :-)

144 30 апр 2020, 17:37 144 68248

>>68241
>Ты пишешь доказательство, а они проверяют, не ошибся ли ты.
Тут есть одна эмпирическая гипотеза: доказательство любой достойной теоремы невозможно записать в прувере. Только тривиальные вещи 19 века и всякую комбинаторику. На данный момент за 40 и более лет компьютерных доказательств исключений не было.

Ответы6824968251

145 30 апр 2020, 17:41 145 68249

>>68248
Это правда, но уже лучше чем Principia Mathematica, согласись!

Ответы68250

146 30 апр 2020, 17:42 146 68250

>>68249
Через 100 лет приходи.

147 30 апр 2020, 17:59 147 68251

>>68248
> Тут есть одна эмпирическая гипотеза: доказательство любой достойной теоремы невозможно записать в прувере.
Почему на бумаге можно?

Ответы6825268259

148 30 апр 2020, 18:02 148 68252

>>68251
потому, что интересно только модульному деду, а он видимо не филдсовский медалист.

Ответы68253

149 30 апр 2020, 18:05 149 68253

>>68252
тут хуй пойми, что он имеет ввиду под математикой: создание вычислительных практичных теорий для народного хозяйства, доказательство больших теорем, нахождение изоморфизмов, рефакторинг математики, упрощение, педагогика, создание новых дисциплин, просто медальки выдаваемые тайным обществом непонятно. Понятно только, что на бумаге главное, чтоб было ОК АРНОЛЬД

Ответы68254

150 30 апр 2020, 18:11 150 68254

>>68253
Написать программу, которая сгенерирует статью по С-системам Воеводского в TeX из исходников и автоматически пошлет в журнал можно уже. А это, очевидно, настоящая математика, ее же чувак с медальками писал!

Ответы68258

151 30 апр 2020, 18:15 151 68258

>>68254
тоже не понимаю этого ad hominem, есть международная классификация математики, её и держитесь

152 30 апр 2020, 18:17 152 68259

>>68251
Там многие формальности опускаются.

153 30 апр 2020, 18:25 153 68262

>>68241
>Тебе придётся долго писать пруф
Долго это порядка времени возврата Пуанкаре?

Ответы68263

154 30 апр 2020, 18:29 154 68263

>>68262
Всё doable, просто математикам быстро надоедает пруф-терм дописывать, да и программисты быстро бросают. Нужны репрессии.

Ответы68266

155 30 апр 2020, 18:38 155 68266

>>68263
Ну да выгнать всех программистов нахуй. А за упоминание cs major расстреливать из зенитки.

156 1 мая 2020, 08:28 156 68275

>>68241
лол, как анон и предсказывал, он получил односложный ответ "да" без реальных пруфов и пояснений как и что
собственно, что и требовалось доказать, погромисты в реальной математике не шарят и по теме разговаривать не могут

>>68231
на этой доске всего 2.5 анона, которую даже второкурсный дифгем осилили, куда уж там потоки риччи
hottоёбы почитали определения категории и гомологии и теперь думают, что они "шарят"
не удивительно, что вербит перестал сюда заходить

Ответы68276

157 1 мая 2020, 08:40 157 68276

>>68275
> не удивительно, что вербит перестал сюда заходить
Так это всё-таки он был, форсил тут свою единственно верную религию, лол. Нет в математике боженьки кроме вербита, а модульный дед (поел говна на обед) - пророк его.
> лол, как анон и предсказывал, он получил односложный ответ "да"
> Вопросы, однозначно подразумевающие односложные ответы
> ответили односложно
> ррреее, я жи говорил
Что вы за люди, пиздец...

Ответы6827868280

158 1 мая 2020, 09:21 158 68278

>>68276
>> Вопросы, однозначно подразумевающие односложные ответы
Ну тогда это на уровне религии, так что пиздуйте со своими пруверами на другие доски.

Ответы68279

159 1 мая 2020, 09:53 159 68279

>>68278
> Ну тогда это на уровне религии
Что на уровне религии, рабочие программы? Братишка, чёт ты с горя совсем хуйню понес.

160 1 мая 2020, 10:43 160 68280

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

Ответы68281

161 1 мая 2020, 10:53 161 68281

>>68280
> как только поступили вопросы по существу
Вопросов по существу не поступало. На вопросы модульного деда (да поест он говна на обед) уже много лет есть однозначный ответ - да, ничего волшебного на бумаге нет, все то же самое можно делать в прувере. Он же с позиции своей швятой веры утверждает, что это не так. Зачем-то даже в очередной раз создал подобный тред.

Ответы68287

162 1 мая 2020, 15:34 162 68287

>>68281
>можно делать в прувере
Так почему никто не делает? Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее. Представляю список теорем прошлого и позапрошлого века, которых никто не может набрать в прувере:

Atiyah-Singer Index Theorem
Baker's Theorem on Linear Forms in Logarithms
Black-Scholes Formula
Borsuk-Ulam Theorem
Cauchy's Integral Theorem
Cauchy's Residue Theorem
Chen's theorem
every vector space is free
Classification of Finite Simple Groups
Classification of semisimple Lie groups (Killing, Cartan, Dynkin)
Sophie Germain's theorem
Gödel's Completeness Theorem
Gödel's Second Incompleteness Theorem
Green-Tao Theorem
Feit-Thompson Theorem
Fundamental Theorem of Galois Theory
Heine-Borel Theorem
Hessenberg's Theorem = "Pappus → Desargues"
Hilbert Basis Theorem
Hilbert Nullstellensatz
Hilbert-Waring theorem
Invariance of Dimension
IP=PSPACE
Jordan Curve Theorem
Kepler Conjecture
Lie's work relating Algebras and Groups
Nash's Theorem
Perelman-Hamilton-Thurston theorem classifying compact 3-manifolds
Poincaré Conjecture
Riemann Mapping Theorem
sorting takes Θ(N log N) steps
Stoke's Theorem
Stone-Weierstrass Theorem
Thales' Theorem
Yoneda lemma
ζ(-1) = -1 ⁄ 12

162 1 мая 2020, 15:34 162 68287

>>68281
>можно делать в прувере
Так почему никто не делает? Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее. Представляю список теорем прошлого и позапрошлого века, которых никто не может набрать в прувере:

Atiyah-Singer Index Theorem
Baker's Theorem on Linear Forms in Logarithms
Black-Scholes Formula
Borsuk-Ulam Theorem
Cauchy's Integral Theorem
Cauchy's Residue Theorem
Chen's theorem
every vector space is free
Classification of Finite Simple Groups
Classification of semisimple Lie groups (Killing, Cartan, Dynkin)
Sophie Germain's theorem
Gödel's Completeness Theorem
Gödel's Second Incompleteness Theorem
Green-Tao Theorem
Feit-Thompson Theorem
Fundamental Theorem of Galois Theory
Heine-Borel Theorem
Hessenberg's Theorem = "Pappus → Desargues"
Hilbert Basis Theorem
Hilbert Nullstellensatz
Hilbert-Waring theorem
Invariance of Dimension
IP=PSPACE
Jordan Curve Theorem
Kepler Conjecture
Lie's work relating Algebras and Groups
Nash's Theorem
Perelman-Hamilton-Thurston theorem classifying compact 3-manifolds
Poincaré Conjecture
Riemann Mapping Theorem
sorting takes Θ(N log N) steps
Stoke's Theorem
Stone-Weierstrass Theorem
Thales' Theorem
Yoneda lemma
ζ(-1) = -1 ⁄ 12

Показать весь текст
Ответы6828868290683106831668385

163 1 мая 2020, 15:37 163 68288

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

164 1 мая 2020, 16:35 164 68290

>>68287
> Так почему никто не делает?
Справедливости ради, таки делают. Просто ты как обычно не в теме https://github.com/UniMath/UniMath например, ещё Воеводского проект, до сих пор развивается.
> Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее.
В той же агде юникод поддерживается, всю нотацию можно переопределить как самому удобно и угодно. Насчёт неосиляторов соглашусь, там мозги нужны. Про лемму Йонеды не смешил бы тапки, она в хаскелле-то давным-давно есть.

Ответы68293

165 1 мая 2020, 18:29 165 68293

>>68290
>Про лемму Йонеды не смешил бы тапки, она в хаскелле-то давным-давно есть.
Лол, ты про частный случай? Тащи пруф в нормальной математической формулировке.

>Справедливости ради, таки делают. Просто ты как обычно не в теме https://github.com/UniMath/UniMath
опять ссылка на гитхаб с непойми чем и клеймо покойного Воеводского, будто он из рая дописывает. Присылай конкретные значимые теоремы из 20 века, тогда поговорим.

Ответы6829468299

166 1 мая 2020, 18:33 166 68294

>>68293
> гранаты формулировка у них не той системы
> ваш гитхаб не гитхаб, там буквы какие-то непонятные
Ясно.
> Присылай конкретные значимые теоремы из 20 века, тогда поговорим.
Значимые для кого? Вашей секты?

Ответы68296

167 1 мая 2020, 20:21 167 68296

>>68294
>Ясно.
Хуясно. Притащи для начала формулировку категории на хаскелле.

>Значимые для кого? Вашей секты?
Для математических предметов за первый и второй курс. Теорема о нулях, теорема стокса, теорема коши из ткфп...

Ответы6830468368

168 1 мая 2020, 21:11 168 68298

Быстро прувер-шизики слились, когда им притащили математики. Как и казалось изначально, это просто погромисты с когнитивным диссонансом, которым кажется, что в хаскеле настоящие категории, а в пруверах - настоящие теоремы.

Ответы683006835368360

169 1 мая 2020, 22:04 169 68299

>>68293
> лемму Йонеды
> пруф в нормальной математической формулировке.
можно статью или скрин тайной леммы Йонеды?

Ответы68303

170 1 мая 2020, 22:07 170 68300

>>68298
> в пруверах - настоящие теоремы.
Ну что ты, настоящее ламповое только на бумаге, ровно то же самое на винте - уже не то же самое.

Ответы68302

171 1 мая 2020, 22:17 171 68302

>>68300
Только есть нюанс, что ошибки на бумаге можно найти. Ошибки в пруверах ты будешь искать намного медленней.

Ответы68307

172 1 мая 2020, 22:18 172 68303

>>68299
https://en.wikipedia.org/wiki/Yoneda_lemma#Formal_statement

Ответы6830668311

173 1 мая 2020, 22:18 173 68304

>>68296
HoTT делалась для автоматизации теории гомотопий или алгебраической топологии, а не для алгебраической геометрии. Для непосредственного управления вараятис нужно ввести в ядро вместо гомотопического интервала [0,1], афинный отрезок А^1 и это уже будет называться А^1-теория гомотопий. Т.е. если ты скажем хочешь Блоха-Като доказать, то тебе сначала нужно перейти в правильную систему типов для этого.

174 1 мая 2020, 22:21 174 68306

>>68303
Ну это любой студент на агде выкладывает на гитхабе. Тут же ничего не нужно кроме теорката и построенной категории множеств. То, что в Хаскеле просто стертый терм до System F, хаскель-доказательство в качестве школьной программы можно защитать. В этом смысле это же можно доказать даже в NuPRL и старых пруверах.

Ответы68308

175 1 мая 2020, 22:22 175 68307

>>68302
> Ошибки в пруверах ты будешь искать намного медленней.
Ошибки прувер сам найдет

Ответы68322

176 1 мая 2020, 22:23 176 68308

>>68306
Вот у Паши есть https://github.com/pcapriotti/agda-categories/tree/master/category/yoneda

Ответы68309

177 1 мая 2020, 22:25 177 68309

>>68308
На NuPRL так:

yoneda-embedding(C) ==
functor(ob(X) = rep-pre-sheaf(C;X);arrow(X,Y,f)
= A |→ λg.(cat-comp(C) A X Y g f))

178 1 мая 2020, 22:27 178 68310

>>68287
>Gödel's Completeness Theorem
Вот тут какой-то студент на Агде написал Gödel's Completeness Theorem

https://mathoverflow.net/questions/272982/how-do-we-construct-the-gödel-s-sentence-in-martin-löf-type-theory

Ответы68386

115 Кб, 960x640
179 1 мая 2020, 22:33 179 68311

>>68303

Ответы6831268369

180 1 мая 2020, 22:37 180 68312

>>68311
СЖВ за классическую математику?

Ответы68314

181 1 мая 2020, 22:38 181 68314

>>68312
так мы видим этот тред

182 1 мая 2020, 22:54 182 68316

>>68287
>Classification of Finite Simple Groups
сразу видно воинственного неадеквата

Ответы68317

183 1 мая 2020, 22:56 183 68317

>>68316
особенно смешно то, что единственное полное доказательство этой теоремы существует только на компьютере :-)

Ответы6831868319

342 Кб, 953x1015
184 1 мая 2020, 23:06 184 68318

>>68317

Ответы68323

185 1 мая 2020, 23:25 185 68319

>>68317
так и другие доказательства на компьютере, но не в прувере.

186 2 мая 2020, 00:51 186 68322

>>68307
>Ошибки прувер сам найдет
>Вера в всемогущий безошибочный компьютер
О как это знакомо.

Ответы68327

187 2 мая 2020, 01:19 187 68323

>>68318
Пруферы гомотопические, а классификация простых конечных групп конструктивна?

Ответы68324

188 2 мая 2020, 01:21 188 68324

>>68323
конструктивная, она в CAS системах считалась

946 Кб, 800x1200
189 2 мая 2020, 02:41 189 68325

>>68162
>а напомните нам нахуя нам 87-я гомотопическая группа трехмерной сферы ?
У МЕНЯ ЗА ТАКИЕ ВОПРОСЫ В ХАРВАРДЕ УБИВАЮТ НАХУЙ ПУЧК ГРОТ СТАТЬИ ПИСАТЬ НАДО ПОВТОРЯЮ ПОВТОРЯЮ СТАТЬЯ ПО 87-тую ГРУППУ ТРЁХМЕРНОЙ СФЕРЫ НЕ ТОЖЕ САМОЕ ЧТО СТАТЬЯ ПОСВЯЩЕННАЯ ОДНОМУ КОНКРЕТНОМУ-НМУ ИНТРЕГАЛУ ПУУЧК ГРООТ ДИДИ ИЗ МГУ ПИШУТ ПРО ИНТЕГРАЛЫ СТАТЬИ И НЕ СТЫДНО КАК В НИГЕРИИ БУДЕМ ГРОООТ

190 2 мая 2020, 07:44 190 68327

>>68322
Про тайпчекинг не слышал?

Ответы68328

191 2 мая 2020, 09:14 191 68328

>>68327
Лол блядь
Тут погромисты походу ни математики, ни программирования не знают
Тайпчекинг, кек
Весь тред это один большой COPE второкурсников с CS

Ответы6833368348

192 2 мая 2020, 10:27 192 68333

>>68328
Опять пук в лужу и швятая вера, что на бумаге можно сделать больше чем в прувере.

Ответы6834768355

193 2 мая 2020, 11:58 193 68347

>>68333
Есть ли в программах баги?

Ответы68364

194 2 мая 2020, 12:08 194 68348

>>68328
Это классическая проблема детей верующих в всезнающий всемогущий комплюктер. В силу того, что они в этой жизни еще нихуя не сделали, они не понимают, что такого не так в их вере.
Воеводский безусловно был первоклассным математиком, но своими унивалентыми основаниями он открыл дорогу всякому cs сброду дорогу туда, где ему быть никогда не следовало.

Ответы68370

195 2 мая 2020, 13:10 195 68353

>>68298
Программистам не упало таким заниматься, на самом деле.

196 2 мая 2020, 13:24 196 68355

>>68333
>швятая вера
Ну вас шизиков напрямую спросили - покажите, как работает на примере любой из фундаментальных теорем 20го века, например теорема об индексе
Кто-то настрочил про гипотезу Пуанкаре, тоже тишина в ответ, неловкое "ну да, это можно..."

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

Ответы68356

197 2 мая 2020, 13:42 197 68356

>>68355
> Пока что это выглядит как религия. Когда меня не аргументами убеждают, а просят поверить - интерес сразу пропадает.
Кому ты нужен, в чем-то тебя убеждать? И где и кто тебя просит поверить? Сам на протяжении нескольких лет создаёшь эти треды, сам потом в них горишь. Зачем? Веруешь во швятую бумагу и бездушные кудахтеры - веруй, свободу вероисповедания не отменяли.

Ответы68357

198 2 мая 2020, 13:55 198 68357

>>68356
А у кудахтеров появилиась душа?

199 2 мая 2020, 15:27 199 68360

>>68298
Тебе кажется, что в топовых пруверах не настоящие теоремы, просто потому что ты пока мало знаешь используемую в них математику. Я тоже раньше не знал и поэтому сомневался.

Ответы68362

200 2 мая 2020, 15:37 200 68361

А зачем нужны пруверы? Ведь в док-вах сложных теорем есть какие-то куски, из которых потом развивают новую теорию. Если всё будут проверять компы то эти куски останутся незамеченными.

201 2 мая 2020, 15:38 201 68362

>>68360
>Тебе кажется, что в топовых пруверах не настоящие теоремы
Да тут нечему казаться - привели пример реальных, настоящих, теорем. Ответа по существу (как тут любит один) - не было. Я вот знаю математику, используемую в гипотезе Тёрстона или той же теореме Атьи-Зингера (не зря заканчивал, теперь могу щитпостить на двоще). Ну так и где они в пруверах? Или моего уровня недостаточно?

Ответы68363

202 2 мая 2020, 15:40 202 68363

>>68362
Я видел десятки академиков которые печатаются в АлгТопе но не могут на компьютере Пифагора записать и что? Там другая математика, и практика нужна.

Ответы68365

203 2 мая 2020, 15:48 203 68364

>>68347
Если программа написанная на сертифицированном прувере или языке, то любая программа в нём является валидным термом в топосе. Тотальное избавление от ошибок и переход в кванторы --- это и есть главная мотивация бездушевной математики.

204 2 мая 2020, 15:50 204 68365

>>68363
Прости, я еще хотел поинтересоваться, а Квиленновские Модельные Категории, Модельные Структуры и Гомотопические Категории --- это как, настоящая математика для модульного деда или нет?

205 2 мая 2020, 17:39 205 68368

>>68296
>Для математических предметов за первый и второй курс.
Я думаю такие вещи в пруверах точно можно записать, просто он скорее всего не знает математики даже на таком уровне.

206 2 мая 2020, 17:40 206 68369

>>68311
В голосину.

207 2 мая 2020, 17:44 207 68370

>>68348
Будто без него это не обмякнет, жидко пукнув.

Ответы68399

208 2 мая 2020, 17:51 208 68371

>>67751
Отвратитетельная на значит бесполезная, говно тоже чистить нужно, но неприятно, так и тут, они бы с большим удовольствием перекинули это на кого-нибудь другого.

Ответы68387

209 2 мая 2020, 17:57 209 68372

>>67946
>А кому-то мастурбация помогает понять материал, мы будем на основе этого делать выводы насчёт её роли в современной математике?
И найти решение тоже помогает.

210 3 мая 2020, 09:05 210 68385

>>68287
как минимум лемма Йонеды и теорема Гёделя верифицированы.

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

Ответы6839068749

211 3 мая 2020, 09:12 211 68386

>>68310
там про неполноту речь, она верифицирована много где
полнота кстати попроще и тоже верифицирована в разных системах.

212 3 мая 2020, 10:49 212 68387

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

213 3 мая 2020, 12:40 213 68390

>>68385
напиши чуваку с сайта, чтобы обновил.

214 3 мая 2020, 22:21 214 68399

>>68370
Пучкнув же.

215 12 мая 2020, 14:43 215 68708

https://twitter.com/andrejbauer/status/1259901971991052290

9 Кб, 480x360
216 13 мая 2020, 12:18 216 68749

>>68385
> Это не модульный дед создал тред, это я

Ответы68755

217 13 мая 2020, 14:54 217 68755

>>68749
Это Шольце?

2 Кб, 330x180
218 16 мая 2020, 02:20 218 68886

Гомологии, гомотопии это же из топологии, так? А как это связано с основаниями математики и доказательствами вообще, объясните.

Ответы68887

552 Кб, 435x650
219 16 мая 2020, 02:24 219 68887

>>68886
Ну короче есть ГОТТ. Гомотопическая теория типов. А дальше на вики всё написано.
https://ru.wikipedia.org/wiki/Гомотопическая_теория_типов

Ответы6888868891

220 16 мая 2020, 05:50 220 68888

>>68887
Перевод: сам я нихуя не понимаю, потому что ещё учусь (на погромиста), но звучит очень понтово.

Ответы68889

370 Кб, 720x405
221 16 мая 2020, 08:28 221 68889

>>68888
А ну говори, каким Браузером пользуешься.

Ответы68890

222 16 мая 2020, 11:07 222 68890

>>68889
>А ну говори, каким Браузером пользуешься.
Каким-каким, интуиционистским - Brouwer: "On the significance of the principle of excluded middle in mathematics, especially in function theory."

223 16 мая 2020, 11:19 223 68891

>>68887
Я статью на вики не понял.

Ответы68899

224 16 мая 2020, 16:02 224 68899

>>68891
А в этом и смысл

225 16 мая 2020, 17:32 225 68903

1) вначале всё свели к натуральным числам.
2) потом решили, что лучше брать за основу множества, так как натуральные числа можно определить в теории множеств как вторичные объекты, а наоборот нельзя
3) потом пришёл Рассел и всё решил свести к формальной логике - так появилась первая теория типов
«Тот факт, что вся математика есть не что иное, как символическая логика, — величайшее открытие нашего века».
4) потом математики поняли, что типы первичны над логикой. На самом деле фактически это показал тот же Рассел, но он не понял этого, полагая первичной логику.
5) работа Бурбаки описывает всё через порождающие структуры http://inponomarev.ru/teaching/speciesofstructures - вот тут по ссылке учебный курс по теории множеств и по структурам Бурбаки. Порождающие структуры по Бурбаки - это по сути типы аксиом. Некоторое среднее решение вопроса о первичности между теорией типов и логикой. При этом в своём роде окончательное - не вдаваясь в конкретное содержание, все матобъекты представляют собой структуры Бурбаки.

6) современные направления далее развивают это всё через теорию категорий. Особенно популярной оказалась идея, что первичными объектами являются высшие категории. Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.

7) самое современное слово в этой науке - гомологическая теория типов. Согласно ей, первичны не множества, ни логика, ни типы, ни структуры - первичны гомотопии. Кратко можно проследить это так:

из натуральных чисел конструируется что угодно ->

сами натуральные числа естественно появляются в теории множеств как кардиналы и ординалы конечных множеств ->

теория множеств строго может быть построена только аксиоматически и через структуры (теория топосов так возникла, но её считают частью теории множеств - просто топос "множество" один из многих топосов)

-> в конечном счёте всё это - символическая логика, при этом Рассел понял это намного раньше создания теории топосов и работ Бурбаки

-> символическая логика описывается семантикой, значит первичнее семантика (отсюда в том числе лингвистический поворот в философии)

-> дальнейший анализ показывает соотношение семантики и математики - семантика шире математики, математика же есть анализ симметрий семантики

-> все виды симметрий семантики могут быть обобщены как высшие группоиды, а высшие группоиды полностью эквиваленты гомологическим типам

-> значит, гомотопии первичнее

-> изоморфизм Карри-Ховарда показывает. что любое доказательство эквивалентно программе, а значит логические системы, типы и формальные исчисления, логики - это одно и то же, только описанное разными способами

-> на основе этого изоморфизма можно создать гомологическую теорию типов, которая описывает любой математический объект на основе "истинно фундаментальных" - симметрий семантик.

225 16 мая 2020, 17:32 225 68903

1) вначале всё свели к натуральным числам.
2) потом решили, что лучше брать за основу множества, так как натуральные числа можно определить в теории множеств как вторичные объекты, а наоборот нельзя
3) потом пришёл Рассел и всё решил свести к формальной логике - так появилась первая теория типов
«Тот факт, что вся математика есть не что иное, как символическая логика, — величайшее открытие нашего века».
4) потом математики поняли, что типы первичны над логикой. На самом деле фактически это показал тот же Рассел, но он не понял этого, полагая первичной логику.
5) работа Бурбаки описывает всё через порождающие структуры http://inponomarev.ru/teaching/speciesofstructures - вот тут по ссылке учебный курс по теории множеств и по структурам Бурбаки. Порождающие структуры по Бурбаки - это по сути типы аксиом. Некоторое среднее решение вопроса о первичности между теорией типов и логикой. При этом в своём роде окончательное - не вдаваясь в конкретное содержание, все матобъекты представляют собой структуры Бурбаки.

6) современные направления далее развивают это всё через теорию категорий. Особенно популярной оказалась идея, что первичными объектами являются высшие категории. Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.

7) самое современное слово в этой науке - гомологическая теория типов. Согласно ей, первичны не множества, ни логика, ни типы, ни структуры - первичны гомотопии. Кратко можно проследить это так:

из натуральных чисел конструируется что угодно ->

сами натуральные числа естественно появляются в теории множеств как кардиналы и ординалы конечных множеств ->

теория множеств строго может быть построена только аксиоматически и через структуры (теория топосов так возникла, но её считают частью теории множеств - просто топос "множество" один из многих топосов)

-> в конечном счёте всё это - символическая логика, при этом Рассел понял это намного раньше создания теории топосов и работ Бурбаки

-> символическая логика описывается семантикой, значит первичнее семантика (отсюда в том числе лингвистический поворот в философии)

-> дальнейший анализ показывает соотношение семантики и математики - семантика шире математики, математика же есть анализ симметрий семантики

-> все виды симметрий семантики могут быть обобщены как высшие группоиды, а высшие группоиды полностью эквиваленты гомологическим типам

-> значит, гомотопии первичнее

-> изоморфизм Карри-Ховарда показывает. что любое доказательство эквивалентно программе, а значит логические системы, типы и формальные исчисления, логики - это одно и то же, только описанное разными способами

-> на основе этого изоморфизма можно создать гомологическую теорию типов, которая описывает любой математический объект на основе "истинно фундаментальных" - симметрий семантик.

Показать весь текст
Ответы689076890868944

226 16 мая 2020, 18:43 226 68907

>>68903
>https://inponomarev.ru/burb
не дай бог такому зачет сдавать

Ответы68925

227 16 мая 2020, 18:44 227 68908

>>68903
> Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.
это интересно, в какой книжке бурбаки можно прочитать про категории?

Ответы6893268934

228 16 мая 2020, 21:44 228 68925

>>68907
почему?

229 17 мая 2020, 05:16 229 68932

>>68908
Topologie algébrique. Chapitres 1 à 4.
Написана посмертно с того света и впервые издана в 2016.

230 17 мая 2020, 06:01 230 68934

>>68908
А я люблю обмазываться современным категорным калом и дрочить. Каждый день я хожу по доске с черным мешком для мусора и собераю в него весь категорный кал, который вижу. На два полных мешка целый день уходит. Зато, когда после тяжёлого дня я прихожу домой, иду в тред для начинающих, говорю новичкам, что их математика не математика…ммм и измазываю тред категориями. И дрочу, представляя, что меня поглотила единая категория. Мне вообще кажется, что категории, умеют думать, у них есть свои семьи, города, чувства, не смывайте их в унитаз, лучше приютите у себя, говорите с ними, ласкайте их…. А вчера в ванной, мне преснился чудный сон, как будто я нырнул в море, и оно прератилось в копредел, функторы, кольца, поля, все из говна, даже первая культура, даже Аллах!.

Ответы68938

231 17 мая 2020, 08:06 231 68938

>>68934
(типичные размышления деда с dxdy о современной математике)

232 17 мая 2020, 13:41 232 68944

>>68903
Откуда паста?

Ответы69055

233 19 мая 2020, 20:45 233 69055

>>68944
http://lurkmore.to/Копипаста:Вован

234 9 окт 2020, 23:03 234 74477

Почему теоремы в университете заставляют писать на листочке, а не вводить в прувер?

Ответы7448874543

235 10 окт 2020, 07:24 235 74488

>>74477
Потому что математика, а не программирование.
Как там пруверы, уже хотя бы теоремы ХХ века вроде теоремы об индексе могут доказать?

Ответы74504

236 10 окт 2020, 17:18 236 74504

>>74488
Так программы тоже раньше на листочке писали, но потом поняли, что так ошибки могут появится. Так и с теоремами, тем более учитывая изоморфизм Карри-Говарда однозначно связывающий математику и программирование.

Базу теорем же люди введут, при том более профессиональные, так что риск ошибки из-за человеческого фактора понижается. А на листочке что? Даже не проверит толком никто.

Ответы745317455274555

237 10 окт 2020, 23:06 237 74531

>>74504

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

Ответы74700

238 11 окт 2020, 15:47 238 74543

>>74477
Потому что тебя, долбоеба, пытаются научить думать. Вероятно зря.

239 11 окт 2020, 21:16 239 74552

>>74504
>тем более учитывая изоморфизм Карри-Говарда однозначно связывающий математику и программирование.
Ох лол, даже не знаю, ты просто тролль зелёный или ещё юный и наивный.
На твой изоморфизм всем похую также, как похую, например, на теорему Кэли о группах, которая вроде как и важная, а нигде никогда не применяется, потому что себе дороже.
Ещё раз, где моя теорема об индексе в прувере? Ну раз изоморфизм, то это вообще на раз-два.

Ответы74700

240 11 окт 2020, 22:54 240 74555

>>74504
>однозначно связывающий математику и программирование.
Только конструктивную её часть, а это 0.00001% от всей математики.

Ответы74700

241 14 окт 2020, 05:49 241 74700

>>74531
>>74552
>>74555
Ты же сам понимаешь, что твои "аргументы против пруверов" доказывают только то, что те, кто считает себя математиками, в 99 случаев из 100 не могут в пруверы, ибо деревянные по пояс. "Дело было не в бобине", как говорится. Если бы ты понимал, о чем вообще изоморфизм Карри-Говарда, ты бы не нёс такую хуйню. А так, имеем то что имеем...

Ответы747027470874711

242 14 окт 2020, 07:44 242 74702

>>74700
> те, кто считает себя математиками, в 99 случаев из 100 не могут в пруверы, ибо деревянные по пояс.
Это не голословное утверждение, кстати. Года три ещё назад Сохацкий писал, что ихние академики не могут даже установить HoTT либу в коке. Агду с нужными либами какой-нибудь условный Вербицкий даже установить не осилит, про использование я вообще молчу

Ответы74703

243 14 окт 2020, 07:56 243 74703

>>74702
> Агду с нужными либами какой-нибудь условный Вербицкий даже установить не осилит, про использование я вообще молчу
Миша вообще в линуксе сидит, насколько я помню
У вас спесь головного мозга в последней стадии, классическое "вы не понимаете, это настолько сложно, что большинство математиков даже не смогут установить, не то что использовать"
Ну и логическая ошибка обобщения, как всегда у программистов

хотт-верунов просят уже который раз показать пример доказательства сколько-нибудь содержательной теоремы вроде теоремы об индексе, а они всё уводят разговор на какую-то нерелевантную солому
"Нет, пока доказать ничего нельзя, но зато УСТАНАВЛИВАТЬ нужно ууууух как сложно, да"

Ответы74704

244 14 окт 2020, 08:08 244 74704

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

Ответы74712

245 14 окт 2020, 09:58 245 74705

Но на самом деле с пруверами в плане установки все не так печально. Есть мейд ин Блинолопатия прувер - arend, там не только HoTT искаропки и даже дополнительная либа с кубической теорией типов, но и установка в один клик мышкой, как плагин к intellij idea, что в свою очередь ставится в два клика https://arend-lang.github.io/ так что прогресс налицо, скоро HoTT будет доступна широким народным массам, в том числе и мнящим себя математиками неосиляторам. Нотацию все равно осиливать придется, правда

246 14 окт 2020, 10:08 246 74706

О, там новый релиз, теперь основная либа тоже ставится в один клик. Короче, хоть на это переползайте, раз уж даже агду поставить не можете.
> Plugin updates:

> arend-lib can be downloaded and upgraded from the IDE

247 14 окт 2020, 11:27 247 74708

>>74700
>>74700

Мой аргумент в том, что плюсы которые дают пруверы сомнительные, а минусы явные и конкретные.

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

>Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.

Никто не спорит, можно и на КОБОЛЕ доказать, только нахуя? Времени это займет много, новизны никакой не будет, а людям жрать что-то надо.

Ответы74718

248 14 окт 2020, 12:43 248 74711

>>74700
>Если бы ты понимал, о чем вообще изоморфизм Карри-Говарда
Так я понимаю, потому и пишу
>Только конструктивную её часть, а это 0.00001% от всей математики.

Ответы74718

249 14 окт 2020, 12:43 249 74712

>>74704
>Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.
Ну то есть ни одной вразумительной теоремы современной актуальной математики хотя бы ХХ века, доказанной с помощью прувера образца 2020 года, ты привести не можешь, как и ожидалось.
Так и сказал бы, что ты пустозвон. Пердежу-то на всю доску от тебя.

Ответы74718

250 14 окт 2020, 13:11 250 74718

>>74711
Если бы понимал, то не писал бы такую хуйню.
>>74712
Когда докажут - ты будешь точно так же кукарекать.
>>74708
> можно и на КОБОЛЕ доказать
Нельзя, он тьюринг-полный, сначала придется прувер на нем писать.
> нахуя? Времени это займет много, новизны никакой не будет
Автоматизация. Что-то простое человек доказать может, что-то посложнее - уже нет. Доказательство чего-то нетривиального в IUTeich человек просто не осилит, никакой. А это ещё не самое сложное.

Ответы74720747277473274810

251 14 окт 2020, 13:36 251 74720

>>74718

>Нельзя, он тьюринг-полный, сначала придется прувер на нем писать.
ну да, сначала прувер, а потом доказать, это смешно хоть

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

Ответы74722

252 14 окт 2020, 13:43 252 74722

>>74720
> больше похоже на модную хуйню: денег освоят и забудут.
Вообще ничем не похоже.

253 14 окт 2020, 14:19 253 74727

>>74718
>Когда докажут - ты будешь точно так же кукарекать.
почему до сих пор не доказали?

Atiyah-Singer Index Theorem
Baker's Theorem on Linear Forms in Logarithms
Black-Scholes Formula
Borsuk-Ulam Theorem
Cauchy's Integral Theorem
Cauchy's Residue Theorem
Chen's theorem
every vector space is free
Classification of Finite Simple Groups
Classification of semisimple Lie groups (Killing, Cartan, Dynkin)
Sophie Germain's theorem
Gödel's Completeness Theorem
Gödel's Second Incompleteness Theorem
Green-Tao Theorem
Feit-Thompson Theorem
Fundamental Theorem of Galois Theory
Heine-Borel Theorem
Hessenberg's Theorem = "Pappus → Desargues"
Hilbert Basis Theorem
Hilbert Nullstellensatz
Hilbert-Waring theorem
Invariance of Dimension
IP=PSPACE
Jordan Curve Theorem
Kepler Conjecture
Lie's work relating Algebras and Groups
Nash's Theorem
Perelman-Hamilton-Thurston theorem classifying compact 3-manifolds
Poincaré Conjecture
Riemann Mapping Theorem
sorting takes Θ(N log N) steps
Stoke's Theorem
Stone-Weierstrass Theorem
Thales' Theorem
Yoneda lemma
ζ(-1) = -1 ⁄ 12

253 14 окт 2020, 14:19 253 74727

>>74718
>Когда докажут - ты будешь точно так же кукарекать.
почему до сих пор не доказали?

Atiyah-Singer Index Theorem
Baker's Theorem on Linear Forms in Logarithms
Black-Scholes Formula
Borsuk-Ulam Theorem
Cauchy's Integral Theorem
Cauchy's Residue Theorem
Chen's theorem
every vector space is free
Classification of Finite Simple Groups
Classification of semisimple Lie groups (Killing, Cartan, Dynkin)
Sophie Germain's theorem
Gödel's Completeness Theorem
Gödel's Second Incompleteness Theorem
Green-Tao Theorem
Feit-Thompson Theorem
Fundamental Theorem of Galois Theory
Heine-Borel Theorem
Hessenberg's Theorem = "Pappus → Desargues"
Hilbert Basis Theorem
Hilbert Nullstellensatz
Hilbert-Waring theorem
Invariance of Dimension
IP=PSPACE
Jordan Curve Theorem
Kepler Conjecture
Lie's work relating Algebras and Groups
Nash's Theorem
Perelman-Hamilton-Thurston theorem classifying compact 3-manifolds
Poincaré Conjecture
Riemann Mapping Theorem
sorting takes Θ(N log N) steps
Stoke's Theorem
Stone-Weierstrass Theorem
Thales' Theorem
Yoneda lemma
ζ(-1) = -1 ⁄ 12

Показать весь текст

254 14 окт 2020, 15:18 254 74732

>>74718
>Если бы понимал, то не писал бы такую хуйню.
Так это ж про тебя, а не про меня.

255 15 окт 2020, 09:56 255 74810

>>74718
>Когда докажут - ты будешь точно так же кукарекать.
Нет, если реально докажут что-то, и это будет не ад хок хуита, адаптированная специально для одной единственной теоремы, то я соглашусь, что это круто, и может даже почитаю что-то.

А пока вы все со своими хотт, категориями в хаскеле, и записями лекций в имакс сидите у меня в одной корзине погромистов-второкурсников и лукавых грантопильщиков.

Ответы74820

256 15 окт 2020, 18:10 256 74820

>>74810
> А пока вы все со своими хотт, категориями в хаскеле, и записями лекций в имакс сидите у меня в одной корзине погромистов-второкурсников и лукавых грантопильщиков.
Это неудивительно, ты ж даже не понимаешь, о чем не только HoTT, но даже тот же изоморфизм Карри-Говарда.

Ответы748267483574860

257 15 окт 2020, 21:46 257 74826

>>74820
И о чём же?

258 16 окт 2020, 09:52 258 74835

>>74820
>Это неудивительно, ты ж даже не понимаешь, о чем не только HoTT, но даже тот же изоморфизм Карри-Говарда.
Тут больше одного анона сидит, если что.

259 16 окт 2020, 19:49 259 74860

>>74820

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

260 17 окт 2020, 08:52 260 74897

>>68197
>>68191
>>68201
>>68203
>>68208
И много других постов от этого мерзкого ублюдка. Граждане математики, обратите внимание, в треде орудует чмо, которое математику не знает, ни одного математического определения не использует, дабы не обосраться(хотя с зфс однажды все же обосрался), и пытается мимикрировать, отвечая односложно в духе "ваша математика - религия, коткудахкудахтахтах ", "почему нет, и что с того" и прочими мусорными способами, уводя дискуссию. Я сам сюда захожу редко, однако сейчас у меня было хорошее настроение, я пил чай, думал над темой магистерской и тут это программистское чмо мне испортило настроение. Посему :

Репортите его, дабы изгнать это чмо.

Всех благ, господа математики.

Ответы7489874899749117491280512

261 17 окт 2020, 09:06 261 74898

>>74897
Платонист, спок

262 17 окт 2020, 09:14 262 74899

>>74897
Это ты ещё не видел шедевр программирования на С++ >>74894 →

263 17 окт 2020, 09:45 263 74900

Ип

264 17 окт 2020, 14:18 264 74904

Воеводский сам что-то доказал с помощью hott?

265 17 окт 2020, 22:39 265 74911

>>74897

>Я так понимаю, там принцип как у теорем существования.
Ты вот на это мне ответь, я правильно понимаю ваш езормфизъмъ?

266 18 окт 2020, 00:09 266 74912

>>74897
Он был здесь ещё до появления доски, чувак.

Ответы74917

267 18 окт 2020, 03:34 267 74917

>>74912
Ну или не он, но сомневаюсь, что есть два таких конструктуха.

268 28 окт 2020, 00:28 268 75296

Фигасе. Вы все еще сретесь тут? https://www.youtube.com/watch?v=21qPOReu4FI

Ответы75303

269 28 окт 2020, 12:47 269 75303

>>75296
Упоротый, даже лекцию прочитал на тему статьи. Конструктухи это клуб фанатиков, я не видел, чтобы какой-нибудь Лури носился по миру и орал "5 шагов принятия высших категорий", "высшие топосы это будущее математики, умоляю, используйте их в доказательстве" итд итп.

Ответы75312

270 28 окт 2020, 16:23 270 75312

>>75303
Если ты чего-то не видел, это не значит, что этого не было.

271 8 янв 2021, 06:40 271 78718

>>67659 (OP)
было несколько знакомых пациентов лет пять назад, все так или иначе относились к СПбАУ.

272 14 янв 2021, 20:27 272 79009

>>67781
На бyмаге вообще ничего нет.
По опpеделению понимания (какомy бы то ни было, неcyщеcтвyющемy), понимание --- это то, что пpоиcходит y тебя в голове.
Человек --- меpа вcех вещей.
И именно это понимание и являетcя пеpвичным объектом, а опpеделения теоpемы доказательcтва --- втоpичным, пpоизводным.

На веpификацию вообще вcем наcpать, кpоме фpиков. Я не могy пpедcтавить cебе здоpового человека, котоpого вcеpьёз волнyет, веpен тот или иной математичеcкий pезyльтат или нет.

Ответы79061

273 15 янв 2021, 16:38 273 79061

>>79009
>Человек --- меpа вcех вещей.
Протагор, залогинься

274 15 янв 2021, 19:46 274 79072

>>67659 (OP)
А что это за бублик на оп пике?

275 17 янв 2021, 22:24 275 79160

>>68185

>Воеводский был жемчужиной, а прувер написать не смог.
>Зато медаль получил, за пофиксаного Блоха-Като, рефакторер блядь.
>С-системы его ёбнутые.
>Ты реально переоцениваешь математиков.

Из цитаты видно, что автор (1) триггерится на слово "рефакторинг" и (2) завидует математикам до зубовного скрежета.

"Скажите, как его зовут?" (с)

Ответы80512

276 17 фев 2021, 21:14 276 80424

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

может кто-нибудь из присутствующих фармакологов объяснить неопытному посетителю чисто для кругозора, к каким наблюдаемым симптомам приводит употребление данного круга веществ? как это могло сказаться на фигуранте обсуждения?

Ответы804328043380435

277 17 фев 2021, 23:21 277 80432

>>80424
он там про шеня что-то написал, то ли хуесосит а шень няшный, то ли имеет в виду что-то своё, понятное только близким друзьям. Я не понял

А где он про "фигурант данного треда" пишет, я не вижу
тоже темнишь что-то

Ответы80438

278 17 фев 2021, 23:49 278 80433

>>80424
По первым же ссылкам из гугла описываются симптомы, похожие на то, что рассказывал фигурант

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

> дезориентированы, испытывают ощущение, что они "находятся в другом измерении", "общаются с Богом", "с дьяволом", переносятся в другие места, слышат какую-то особую "неземную" музыку и пр. Некоторые лица в период интоксикации ощущают безграничные творческие способности: им кажется, что они сочиняют музыку, складывают стихи, им приходят в голову удивительные фасоны одежды и пр.

Ответы80441

279 18 фев 2021, 00:04 279 80435

>>80424
>фигурант данного треда
Иди нахер с таким жаргоном. Полицейщина мерзкая.

Ответы80440

280 18 фев 2021, 05:56 280 80438

>>80432
>А где он про "фигурант данного треда" пишет, я не вижу
В некрологе на Воеводского и пишет.

281 18 фев 2021, 09:29 281 80440

>>80435
разве "нулевой пациент" существенно благозвучнее? хм.

282 18 фев 2021, 09:35 282 80441

>>80433
>им приходят в голову удивительные фасоны одежды и пр.
удивительные фасоны оснований математики, ага.

283 20 фев 2021, 07:50 283 80512

>>79160
Петух - конструктух.

Я его ещё здесь:>>74897 описал.

Ответы80518

284 20 фев 2021, 12:30 284 80518

>>80512
а вдруг их несколько? или они размножаются...

285 21 фев 2021, 12:39 285 80566

Вопрос к адептам и сектантам. Сегодня, а может и давным давно, мне во сне явился ангел. Мы перетерли за математику. Произошло озарение.

Есть симплициальная категория Delta. Есть кубическая категория I, даже в нескольких версиях. С дельтой в hott вроде все кисло. С кубиками лучше.

Есть категория Gamma имени Сигала. Есть Sym^{op}, скелет FinSet^{op}. Гамма относится к дельте, как сим-оп к кубикам. Я не знаю, насколько это известно и банально, но это так.

1. Ясно, что дельта и кубики - это что-то ассоциативное, а гамма и сим-оп - это что-то ассоциативное и коммутативное. Есть ли в hott утверждение вида "когда ассоциативно - это гомотопический тип, а когда еще и коммутативно - это спектр"?

2. Гомотопический тип - это хороший предпучок и на дельте, и на кубиках. С гаммой и сим-оп все сложнее. Хороший симплициальный предпучок на гамме - это связный спектр. Хороший предпучок на сим-оп, со значениями в категории симплициальных множеств с отмеченной точкой, - это спектр, не обязательно связный. Раз в одном случае эквивалентность есть, а в другом эквивалентности нет, оба случая нетривиальны и содержательны. Hott как-нибудь помогает увидеть это нетривиальное содержание?

Ответы80570

286 21 фев 2021, 12:59 286 80570

>>80566

выкиньте свои комплексы Кана, вместе со всей фибратной демагогией, прямо в анналы истории, и Квиллена туда же, быстро, решительно.

если вы обращали внимание, то Сова хвалит Лури, который тоже увлекался именно эти клеточными комплексами, но зато Каледин ругает. и для того есть причины.

Ответы8156181692

287 18 мар 2021, 12:51 287 81561

>>80570
...И причины эти в том, что Каледин Иванова дураком считает.

Ответы81575

288 18 мар 2021, 14:33 288 81575

>>81561
типа сидит каледин такой, на лурье подрачивает, утомился, зашёл в блог совы... ба! а сова, оказывается, лурье любит! быстрее побегу, напишу, как я лурье не выношу вообще

Ответы81591

289 18 мар 2021, 18:27 289 81591

>>81575
Побегу и напишу
@
Как лурье не выношу

Матемачу давно не хватает частушек. И гармониста.

Ответы81733

290 22 мар 2021, 01:13 290 81692

>>80570
ок, выкинули, дальше какие инструкции будут?

291 23 мар 2021, 01:19 291 81733

>>81591
Вышел модуль на крыльцо
Расширить себе кольцо
Сунул функтор нет кольца
Так и шлёпнулся с крыльца

Ответы81742

292 23 мар 2021, 14:41 292 81742

>>81733
Можно вместо "расширить" использовать "растянуть"?

293 23 мар 2021, 16:19 293 81743

>>68202
Нормально там всё, книгу‐то открой хотя бы.

Обновить тред
Двач.hk не отвечает.
Вы видите копию треда, сохраненную 13 июня в 14:30.

Скачать тред: только с превью, с превью и прикрепленными файлами.
Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах. Подробнее

Если вам полезен архив М.Двача, пожертвуйте на оплату сервера.

« /math/В начало тредаВеб-версияНастройки/a//b//mu//s//vg/Все доски

Пользуетесь скринридером — пишите, что можно улучшить.
Host-Food.ru — надёжный хостинг от 12 руб/мес | Free DNS
Зеркала М.Двача: m2ch.hk, m2ch.lib, m2chfapiswfw2wcakptqp4o6ltgchvjuxfab7urxlduraomtlnhw5xad.onion