Математика

Ответить в тред Ответить в тред
Check this out!
ОПРОСИК Господа и дамы, сообщите хотя бы частичную Аноним 19/04/20 Вск 16:42:11 676591
image.png 81Кб, 480x360
480x360
ОПРОСИК

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

Аноним 20/04/20 Пнд 00:07:46 677082
На двачах. Несколько лет назад, ещё когда не было этой доски и маттетреды были в /sci. От местного конструктивиста.
Аноним 20/04/20 Пнд 00:34:14 677093
>>67659 (OP)
Что в ней плохого, объясните?
Аноним 20/04/20 Пнд 00:39:23 677104
Учился на физика @ кафедра физики частиц @ хочу быть теоретиком @ КТП @ БРСТ @ когомологии @ топология...
Трактор @ хочешь остаться - давай считай количественный результат @ компьютер программировать @ Haskell @ Ocaml @ Coq @ Воеводский @ HoTT
Как-то так.
Аноним 20/04/20 Пнд 07:46:28 677175
>>67659 (OP)
> (понятно кого)
Кого? Понятно кому?
Аноним 20/04/20 Пнд 11:04:11 677296
>>67710
Эх, друже, после нормальной математики хаскелом занялся...

остальное - клёвые вещи, так держать
Аноним 20/04/20 Пнд 12:10:34 677317
>>67729
>нормальной математики хаскелом занялся
Почему математики такие высокомерные?

>>67710
А ты, физик, сам как считаешь, то что ты докатился до хаскеля, это деградация?
Аноним 20/04/20 Пнд 12:36:35 677328
>>67731
>Почему математики такие высокомерные?
не увидел в его посте высокомерия, честно говоря
что нравится, тем и занимайся
но сравнивать хаскелл с математикой, скажем, брст вполне себе можно объективно
то, что она в разы или даже на целые порядки проще в первом случае, тебя волновать не должно, если тебя интересует эта область

>деградация
не он, но брст я проходил
если под деградацией понимать уменьшение сложности, то да
это как учиться лет 10 в музыкалке и консерватории, чтобы потом играть собачий вальс одним пальцем
Аноним 20/04/20 Пнд 13:18:39 677339
>>67731
Хаскель это грааль теории категорий, которая в свою очередь является программироваем и второй культурой.
Аноним 20/04/20 Пнд 13:28:33 6773410
>>67733
>Хаскель это грааль теории категорий
Ну не то, чтобы там была какая-то особо замысловатая теория категорий.
>>67659 (OP)
Уже довольно давно (лет 8 назад), когда я учил логику.


Аноним 20/04/20 Пнд 14:14:59 6773611
>>67733
Что такое вторая культура?
Аноним 20/04/20 Пнд 14:33:00 6773812
Почему среди математиков так много верующих?
Аноним 20/04/20 Пнд 14:50:52 6774013
>>67738
Если ты уже веришь в реальность вне-временных бесконечных объектов, что очень естественно для математиков, то почему бы еще не принять бога.
Аноним 20/04/20 Пнд 14:51:02 6774114
>>67731
>А ты, физик, сам как считаешь, то что ты докатился до хаскеля,

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

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

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

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

это >>67733 не я

Аноним 20/04/20 Пнд 15:04:21 6774415
>>67659 (OP)
>, а главное - где и/или от кого вы узнали про homotopy type theory?
Интервью с Воеводским.
Аноним 20/04/20 Пнд 15:07:01 6774516
>>67741
Просто пограмирование отвратительный аутизм и тупость, вполне понятно, что адеквату неприятно марать этим мозг.
Аноним 20/04/20 Пнд 15:24:19 6774717
>>67741
Не понял, на что конкретно физики раздражаются и почему злятся на тебя?
Аноним 20/04/20 Пнд 16:05:57 6775118
>>67745
>Просто пограмирование отвратительный аутизм и тупость, вполне понятно, что адеквату неприятно марать этим мозг.
Ты правда считаешь, что программирование хуже чем та деятельность, которую оно автоматизирует?

Как по мне, автоматизация нудных выкладок, о которой пишет >>67741, это безусловно позитивная вещь.
Аноним 20/04/20 Пнд 16:10:02 6775219
>>67747
> на что конкретно
Деталей не хочу говорить, слишком деанон.

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

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

> почему злятся на тебя?
Яж почем знаю...
Аноним 20/04/20 Пнд 16:15:13 6775320
>>67752
Похоже, высокоинтеллектуальные круги - тот еще гадюшник. Слышал, что шахматисты тоже люто, бешено ненавидят друг друга.
Аноним 20/04/20 Пнд 16:18:16 6775421
>>67752
Ради любопытства, в чем бонус Coq в такого рода деятельности? Казалось бы для обсчета моделей куда проще было бы использовать систему символических вычислений. Понятно, что так не получишь формального доказательства; но обычно в физике никто и не ставит таких критериев строгости. При этом получение именно формального доказательства вещь явно не бесплатная и требует кучи дополнительных усилий.
Аноним 20/04/20 Пнд 16:33:37 6775522
>>67754
>Ради любопытства, в чем бонус Coq в такого рода деятельности?
Опять детали не скажу. Это специфика данной области теорфизики - тут Coq очень хорошо подходит.
Аноним 20/04/20 Пнд 17:21:59 6776223
15871007236432.png 540Кб, 680x621
680x621
Я правильно понимаю, что хейт в сторону кока и всего такого основан на суеверии, что на бумаге ручкой можно сделать больше, чем в коке, и типа как ручка с бумагой это высокий штиль, а кок - презренный бездушный быдлокодинг?
Аноним 20/04/20 Пнд 17:48:54 6776524
Аноним 20/04/20 Пнд 18:01:03 6776725
>>67762
Нет. Хейта к коку нет, есть хейт к его слепым последователям, которые утверждают, что маняматика нинужна и автоматизированные пруверы - будущее. У таких вот "экспертов" просто не хватает образования, чтобы понять, о чём вообще современная математика, но они её уже "решили".
Аноним 20/04/20 Пнд 19:57:28 6777326
>>67762
Да, но большинство в этом не признается и будет рационализировать>>67767
Аноним 20/04/20 Пнд 20:41:14 6777727
>>67773
В чем преймущество проверки на бумаге?
Аноним 20/04/20 Пнд 21:03:18 6777828
>>67777
Тебеж >>67752 объяснил -- по статье в год на каждое натуральное число. И получ, что ты не хуйней страдаешь, а ресерч.
Аноним 20/04/20 Пнд 21:17:20 6777929
>>67778
Это практическое виденье.
Я о тех кому и образование достает и денег не особо требуется. Что с ними не так?
Аноним 20/04/20 Пнд 21:20:47 6778030
>>67762
Не на бумаге, а в голове.
Аноним 20/04/20 Пнд 21:47:53 6778131
>>67780
> Не на бумаге, а в голове.
А что у тебя есть волшебного математического в голове, чего нет в математической нотации на бумаге? Особая уличная магия?
Аноним 21/04/20 Втр 03:29:04 6778432
>>67755
> Это специфика данной области теорфизики
И что же это за область?
Аноним 21/04/20 Втр 07:20:34 6779333
>>67779
> Я о тех кому и образование достает и денег не особо требуется. Что с ними не так?
Тут как с историей антисептиков в медицине. Врач Земмельвейс показал, что если мыть руки с хлоркой перед операцией, а не после, то внезапно смертность послеоперационных больных от сепсиса падает с 60% до 1-2. И что, его признали спасителем? Хуй там. Затравили, заруинили карьеру, позже вообще в дурку упекли. Потому что для абсолютного большинства светил медицины признать себя дебилом, не могущим в банальное мытье рук, хуже всего. Так и тут. ЧСВ важнее практических результатов, даже если речь о жизнях людей, про математику и говорить нечего. Кто сознательно откажется от высокопарных кукареканий о первой культуре и о чем-то волшебном в голове, чего нет в бездуховном коке? Да никто, это равносильно признанию себя дебилом.
Аноним 22/04/20 Срд 06:27:45 6784434
>>67793

Есть такая гипотеза, что чтобы что-то доказать, убедить другого математика(и себя тоже) в некоторой теореме, не нужно делать все выкладки. Если её принимать как истину, тогда "верификация -- это дополнительная работа". Но тогда получается, что один раз её сделал автор и её сделал каждый читатель. Зачем перекладывать? Верифицировать -- просто, приятно и кучу ошибок и интересных нюансов можно найти. Ответ прост: ещё нет устоявшихся стандартов верификации: всяким нормальным кокам и хорошим аналогам обычно около 30 лет разработки. И они синтаксис меняют.
Аноним 22/04/20 Срд 12:35:10 6785235
>>67659 (OP)
недавно какой то пидорас рассказал про неё. Он хоть и пидорас, но вдруг что то полезное говорит. А что, в чём проблема этой homotopy type theory?
Аноним 22/04/20 Срд 12:36:54 6785336
>>67844
Но есть ли у тебя хоть какие-нибудь истории успеха в математике, когда во время попытки формализации поймали существенную ошибку? Т.е. не просто какую-нибудь техническую лемму, которая была сформулирована в излишней общности, когда она уже не верна, но общий ход доказательства от этого не страдает. А вот, чтобы было что-то не так с какой-то важной теоремой, которой действительно пользовались другие математики.

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

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

>Но тогда получается, что один раз её сделал автор и её сделал каждый читатель
Это неадекватный взгляд на то, как и почему читают математические статьи. Собственно верификацией читатели занимаются не так часто; обычно или если читатель это ответственный рецензент или если заявлен интересный результат, но есть подозрения в наличие ошибки (кстати и в таком случае искать ошибки тотально построчной проверкой - это контр-продуктивно, куда лучше искать в статье подозрительные утверждения и таким образом локализовать свое внимание на фрагментах где есть серьезные основания ожидать ошибку). Иначе цель состоит в том, чтобы понять, в чем состоят результаты и извлечь идеи доказательств/конструкций. И для последнего формализация никак не поможет. Скорее наоборот, если кто-то только произведет верификацию в Коке, но не напишет нормальную статью, то разобраться в доказательстве станет труднее.
Аноним 22/04/20 Срд 12:52:49 6785537
>>67853
>Но есть ли у тебя хоть какие-нибудь истории успеха в математике
Для этого надо знать математику, лол
Аноним 22/04/20 Срд 13:10:30 6785738
>>67853
> Но есть ли у тебя хоть какие-нибудь истории успеха в математике, когда во время попытки формализации поймали существенную ошибку?
Есть. Заповедью исключенного третьего и актуальной бесконечности пользовались веками, пока Брауэр не показал, что это просто когнитивные искажения, и основывать на них точные знания - ошибка.
Аноним 22/04/20 Срд 15:04:16 6786739
>>67857
>пока Брауэр не показал
"Показал"? Ты сделал ошибку в слове "заповедовал".
Аноним 22/04/20 Срд 15:56:54 6787040
>>67857
Верую в тезис Цервки, ем Карри, сижу в Браузере ;)
Аноним 22/04/20 Срд 17:59:00 6787141
>>67867
>>67870
Ну-ну. А по факту как всегда ни одного ответа по существу, например на >>67781 , одна анальная клоунада. Ничего нового, одна попаболь одного еблана от HoTT итд...
Аноним 22/04/20 Срд 18:14:10 6787242
image.png 103Кб, 240x168
240x168
>>67871
А прогреры уже запрогали ГоТТ так, чтобы он в Браузере работал? Или надо себе приложение на комп качать?
Аноним 22/04/20 Срд 18:17:27 6787443
>>67871
Так что оказывается >>67857 был не стеб. Лол.
Аноним 22/04/20 Срд 18:18:45 6787544
>>67857
>пока Брауэр не показал
ВЕРУЮ ИБО ЗАВЕЩАНО
Аноним 22/04/20 Срд 18:31:07 6787645
Заметил интересный паттерн - все (трое), кто с моей кафедры впоследствие заинтересовались HoTT и пруверами, на первом курсе пытались записывать лекции через латех и ебню вроде vim на своём нетбуке-хуюке. Так что эта болезнь выявляется на ранней стадии.
Аноним 22/04/20 Срд 18:48:51 6787846
image.png 445Кб, 604x405
604x405
>>67876
Будем знать. Поскорей бы выпустили версию ГоТТ для Браузера.
Аноним 22/04/20 Срд 18:57:15 6787947
>>67878
Откуда тяночька?
Аноним 22/04/20 Срд 19:09:10 6788048
>>67879
Хз. Нашел в гугл-пикчах.
Аноним 24/04/20 Птн 00:22:40 6793549
>>67876
я тоже угораю по пруверам, и тоже в латехе сначала писал, лекции все конспектировал дотошно, хоттом переболел успешно(хуйня, не ведитесь, классическая математика в миллион раз круче)
Аноним 24/04/20 Птн 10:40:31 6794350
>>67853

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

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

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

Анекдотический пример, вобщем. Ну а мне в понимании книг помогает чтение других книг.
До кучи ещё и ложная эквивалентность - формализация и верификация. Как будто блядь до пруверов все математики на пальцах всё доказывали, а потом пришли матлогики и хачкеллоёбы и понеслась.
Аноним 24/04/20 Птн 12:30:49 6794752
>>67946
> обычный математик просто спросит на кафедре
Рассмешил... Это ты траллишь так, да? Да?
Аноним 24/04/20 Птн 13:12:27 6795053
>>67947

Да не, он не троллит, он просто токсичный долбоёб, который ни одной теоремы не доказал, но имеет "очень ценное мнение".
Аноним 24/04/20 Птн 16:51:19 6795354
>>67947
Нет, это правда. Математик без общения это не математик, а калека, фрик. Ни один успешный математик еще не жил без общения в среде.
Аноним 24/04/20 Птн 16:55:54 6795455
>>67953
Так вот почему во всех книгах по математике подача материала напоминает бред шизофреника.
Надо просто в той же среде крутиться, что и автор.
Аноним 24/04/20 Птн 18:12:07 6795656
>>67954
>во всех книгах по математике
>бред

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

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

>>67950
>токсичный
Уябывай уже на реддит, и strawman свой захвати.
Аноним 24/04/20 Птн 18:15:37 6795757
>>67953
А ну так сразу видно почему вашему брату пруверы не нравятся. Так ты "успешный математик" крутящийся в элитарных кругах, который если что может "просто спросить на кафедре". А тут оказывается что можно git clone все доказательства, и ценность всех твоих социальные элитосвязей внезапно сильно уменьшилась.
Аноним 24/04/20 Птн 18:19:27 6795858
>>67710
Правильно ли я понимаю, что когда мы дотрагиваемся до стены, то молекулы нашего пальца начинают взаимодействовать с молекулами стены, обмениваясь на бешеной скорости кварками, и из за этого палец не пролазиет в стену?
Аноним 24/04/20 Птн 18:21:39 6795959
>>67956
неосиляторов,лол. чего я по-твоему не осилил?
Аноним 24/04/20 Птн 18:24:16 6796060
>>67959
Пучки на многообразиях, K-теорию, теорию Ходжа.
Аноним 24/04/20 Птн 18:54:32 6796361
>>67960

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

Если ты специалист, то зачем это нужно, какие проблемы решает? Может быть действительно стоит изучить
Аноним 24/04/20 Птн 20:23:14 6796962
>>67957
>тут оказывается что можно git clone все доказательства, и ценность всех твоих социальные элитосвязей внезапно сильно уменьшилась.
Я эти маняфантазии уже сотый раз слышу, но вот на практике почему-то всё наоборот и в точности как говорит анон выше.
Аноним 24/04/20 Птн 21:17:30 6797163
>>67969

А ты типа идеалист и надеешься на успешность и адекватность присутствующих? Кто из нас в итого ебобо?:)
Аноним 24/04/20 Птн 21:22:59 6797264
>>67969

Тем временем ты не говоришь какие проблемы решает твоя область математики. Кто её у тебя купит? (Даже чисто гипотетически)
На пруверах можно программы верифицировать, в том числе квантовые, а твоя теория ходжа и к теория ну куда её. Диффуры решать на многообразиях? А их кому продавать?
Аноним 24/04/20 Птн 21:32:33 6797365
>>67957
Доказательства везде написаны, интуицию за ними тебе никто просто так не даст. Вполне может быть, прочитал ты и не понял. Открой, например, доказательство Перельмана. Что будешь делать? Читать до посинения?
Аноним 24/04/20 Птн 22:15:24 6797566
>>67969
>анон выше
А чего тогда вы вместе с "аноном выше" и ОПом кудахчете так на пруверы? Ну бегают там хипстеры-программисты-аутисты какие-то, в отличие от вас, элитарных, доступа к "спросить на кафедре" не имеют. Толку от этих ваших пруверов нет - тру математика только "на кафедре". Ну и хрен бы с ними?
Аноним 25/04/20 Суб 01:32:52 6798667
>>67781
На бумаге вообще ничего нет.
По определению понимания (какому бы то ни было, несуществующему), понимание --- это то, что происходит у тебя в голове.
Человек --- мера всех вещей.
И именно это понимание и является первичным объектом, а определения теоремы доказательства --- вторичным, производным.

На верификацию вообще всем насрать, кроме фриков. Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
Аноним 25/04/20 Суб 08:05:37 6798768
27000033.366680[...].jpeg 62Кб, 555x400
555x400
>>67986
> На бумаге вообще ничего нет.
> По определению понимания (какому бы то ни было, несуществующему), понимание --- это то, что происходит у тебя в голове.
> Человек --- мера всех вещей.
> И именно это понимание и является первичным объектом, а определения теоремы доказательства --- вторичным, производным.
Охуеть, откровения какие. Ещё несколько лет, глядишь и до интуиционизма додумаешься. А вот суть формализма как раз в том, что все нужное - на бумаге, и зависит только от непротиворечивости используемой аксиоматики. От головы в данном случае зависит только выбор аксиоматики, какой набор заповедей больше зайдет - ZFC там, NBG итд. Гедель, правда, доказал что это для оснований не подходит, да и ладно, хуй с ним.
Аноним 25/04/20 Суб 09:12:35 6798969
>>67986
> На верификацию вообще всем насрать, кроме фриков. Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
Ну да, во всякой прикладухе так и есть. Сантехнику не нужна физика, гамалогии можно трясти без оснований.
Аноним 25/04/20 Суб 11:36:02 6799470
>>67989
Да, вот на этой процитированной фразе, а также на вопросе "чьи проблемы твоя область решает, кроме твоих", тот анон явно сливается.
Аноним 25/04/20 Суб 20:33:47 6803271
>>67987
Вот именно, ты прав. Надо больше писать всяких доказательств, брошюр, книжек, чтобы это было доступно большему количеству людей, в разных форматах, а не только "от человеку к человеку".
Аноним 26/04/20 Вск 00:14:36 6804572
>>67659 (OP)
Узнал из чатика, где обсуждают теорию типов.
Сохацкий активно HoTT пропагандирует.
Аноним 26/04/20 Вск 15:08:20 6805873
>>67986
ну что, ушёл с седовласыми старцами на кафедру советоваться?
Аноним 28/04/20 Втр 02:54:39 6810674
>>67986
> Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
Ну что это такое?
Аноним 28/04/20 Втр 11:24:29 6811075
>>67989
ну ты прав, основания имеют такое же отношения к математике, как обсуждение интерпретаций квантовой механики к починке сан. узла, никакое то есть
Аноним 28/04/20 Втр 12:10:12 6811176
>>68106
он имел в виду, проверять, верен ли доказанный кем-то результат, который проверен "авторитетами", с существующим консенсусом...

Сомнительное утверждение, так как твоё понимание может отличаться от объективной реальности. Игра в рулетку тут. Верификация позволяет нивелировать подобные неточности. (у многих серьёзных результатов есть набор неэквивалентных формулировок)
Аноним 28/04/20 Втр 13:05:21 6811277
Аноним 28/04/20 Втр 14:14:13 6811378
>>68111
Нет, я имел в виду, что "факт" истинности или ложности того или иного математического утверждения сам по себе не имеет ни ценности, ни смысла. Допустим, гипотеза Римана верна или не верна --- какая разница? Тебе лично не плевать?
Любое утверждение можно принять в качестве аксиомы, т.е. сделать его верным или неверным по своему желанию.
Слишком большой фокус на "да/нет" аспектах --- это аберрация , являющаяся следствием принятой сейчас системы преподавания, а не какой-то глубокий факт.
Противопоставляя компьютерную верификацию "работе по старинке", многие подменяют первичную ценность вторичной.
Хотя, если считать компьютер продолжением мозга, то всё нормально. Но это получается киборг, а не человек.
>>68058
Я не он, если что.
Аноним 28/04/20 Втр 14:27:04 6811479
1.png 89Кб, 512x512
512x512
>>68113
> Нет, я имел в виду, что "факт" истинности или ложности того или иного математического утверждения сам по себе не имеет ни ценности, ни смысла.
Математике это по своей сути точное знание. На голландском буквально - wiskunde. Факт истинности или ложности утверждения это сама суть математики, вне которого ее просто нет. Отсюда и проблема оснований - что именно считать истинностью в математике.
> Допустим, гипотеза Римана верна или не верна --- какая разница? Тебе лично не плевать?
То что ты описываешь - уровень пикрелейтед.
Аноним 28/04/20 Втр 18:43:56 6811880
>>68114
>На голландском буквально - wiskunde.
А на ацтекском - Tlapōhualmatiliztli.

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

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

Ну а кроме того, гипотеза Римана уже доказана Делинем в 1974-м еще.
Аноним 28/04/20 Втр 19:35:32 6811981
>>68118
>Ну а кроме того, гипотеза Римана уже доказана Делинем в 1974-м еще.
Жаль что кроме тебя этого никто не знает.
>что гипотезу Римана следовало бы принять за аксиому
Верую, ибо блаженен.
Аноним 28/04/20 Втр 20:27:09 6812082
Аноним 28/04/20 Втр 20:39:42 6812183
>>68119
>Верую, ибо блаженен.

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

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

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

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

>>68121
> Когомологии, схемная алгебраическая геометрия, К-теория и т.д. имеют гигантское количество приложений, Делинь, Гротендик, Артин, Мамфорд и прочие действительно ближе к сантехникам, как тут выразились, чем к фуфлософам-пиздаболам с их объективными истинами, трансцендентальными единствами, тезисами Черта и проч.
Пынямаешь ли, все что ты перечислил, вовсе не висит где-то в пустоте. Это следствия развития математической мысли, следствия, к которым привели даже не столетия эволюции самых разных математических и не только идей, методов итд. И тот подход, который ты вычитал у Вербицкого, он в точности соответствует пикрелейтед номеру "тут играем, тут не играем, тут вообще рыбу заворачивали". И.е предлагается что-то сыграть не только в отрыве от всего контекста, но и принципиально игнорировать вопрос, откуда все это вообще пошло и в чем природа всего этого. В принципе, такой подход имеет право на существование, но с определенными оговорками, которые ваша секта принципиально не принимает. Практическая применимость чего-то как критерий истины это хорошо и правильно, но принимать это не как функциональный контекстуализм, а как нечто висящее в воздухе и данное нам непонятно кем и нахуя, это сектантство.
Аноним 29/04/20 Срд 02:43:20 6812985
A01C5427-205B-4[...].jpeg 672Кб, 1403x988
1403x988
>>68114
>Факт истинности или ложности утверждения это сама суть математики, вне которого ее просто нет.
Вообще-то это ниоткуда не следует.
Сами по себе понятия истинности и ложности могут оказаться не совсем тем, что надо ставить в основания.
Т.е. настоящие основания должны основываться на каких-то других концепциях (каких --- не знаю), а понятия "истинности" и "ложности" --- выводиться из них. Грубо говоря.
>То что ты описываешь - уровень пикрелейтед.
Наполовину прикалываюсь, наполовину серьёзен.
Возможно, если математик начнёт серьёзно рефлексировать, изучать свои мысли и побуждения, то что-то из этого он сможет извлечь.
>>68121
>Люди, всерьез интересующиеся основаниями, это люди которые не понимают что такое вообще математика, где и зачем она нужна.
Громкое заявление.
А слова о фуфлософии и оскорбительные, и смешные. От любителя "схемной алгебраической геометрии", у которой приложений в жизни... сколько? Для любого нормального человека ты сам пиздабол.
Аноним 29/04/20 Срд 15:45:27 6816186
>>68125
>функциональный контекстуализм
охуенно, прямо как у Гермиды и Якобса, синоним декартовой замкнутости
Аноним 29/04/20 Срд 15:49:57 6816287
>>68125
а напомните нам нахуя нам 87-я гомотопическая группа трехмерной сферы ?
Аноним 29/04/20 Срд 15:56:55 6816388
>>68125
> фуфлософам-пиздаболам
Погоди-ка. Это что-же получается, "пыняпучк" юродидый с /math/ и "философсмолин" пиздобол с /sci/ - одна и та-же личность? Кто бы мог подумать?
Аноним 29/04/20 Срд 18:44:09 6816589
господа, вы правы лишь частично

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

2) я присоединяюсь к требованию обоснования изучения алгебраической геометрии, гиперкелеровых многообразий, пучков и прочего. Покажите покупателей! Пруф или не было!
Аноним 29/04/20 Срд 19:50:40 6816690
>>68165
Пучки нужны даже палочкосчитателям и N-петухам для построение пресловутого функционального контекстуализма, у них там современная теория типов на предпучках строится и есть расширенная теории типов, где вместо категории множеств берутся категории групоидов, и таким образом переходят в престек теорию типов, где вместо сигмы конструкция Гротендика. Те еще наркоманы.

Я за модульного деда если что, но мне кажется, что вы тут попутали понятия верификации и нормализации. Вот скажем вы можете верифицировать свои группы сфер (если построите конечно, а то выше четвертой группы никто не построил еще даже для первых трех измерений), но нормализовать терм уже не сможете, нужно изобретать механизмы оптимальной редукции, новая открытая проблема). А так когомологии элиптические, циклические, хуические, этальные, халяльные — все это изи чекается уже пару лет как. Этальные кстати если записать в HoTT будут самыми красивыми.
Аноним 29/04/20 Срд 22:40:13 6816891
quote-one-canno[...].jpg 71Кб, 850x400
850x400
>>68166
> Пучки нужны даже палочкосчитателям и N-петухам для построение пресловутого функционального контекстуализма, у
Зачем? Все это прекрасно строится без всяких пучков.
> А так когомологии элиптические, циклические, хуические, этальные, халяльные — все это изи чекается уже пару лет как. Этальные кстати если записать в HoTT будут самыми красивыми.
Все дело в том, что при желании это все работает в обеих направлениях. Гамалогии можно представить в HoTT, а можно и наоборот. Всяческие вербитодрочеры веруют только во швятые гамалогии, а все остальное в их религии даже не математика. Тогда как на самом деле все сложнее. И HoTT и гамалогии, и много чего другого - это просто языки, вторичные по отношению к собственно математическому мышлению. Потому что если это не принимать, тогда придется принять, что вся математика существует только на бумаге, а роль человека - трясти синтаксис. Либо остаётся совсем уж религия - платоновский мир идей, актуальная бесконечность, исключенное третье и прочие подобные догмы, заповеди. Можно скатиться ещё дальше, до высказываний Манина о том что "математика подвешена в воздухе". Но это уже уровень патриота, который сидя за американским компьютером с американским по, пишет в американском интернете, какие пиндосы пидоры.
Аноним 29/04/20 Срд 22:55:03 6817092
>>68168
>Зачем? Все это прекрасно строится без всяких пучков.
Строится без пучков, но с пучками выглядит компактнее. Там много изоморфизомов моделей теории типов: Категории с семействами (CwF), категории с аттрибутами (CwA), Воеводский делал С-системы, потом поняли, что это все поебота, выдуманная людьми и перешли на гротендиковский пучкизм в французском стиле. Кубическая теория типов стала записываться одной формулой: I: <sup>op</sup> → Set. Пи и сигма тоже в пучках формулируется, как функториальная смена базы, вернулись к Лавировской классике.
Аноним 29/04/20 Срд 23:00:20 6817193
>>68170
Это хорошо, что пока только модульный дед атакует, а придут спросят как Стекс Проджект закодировать и что мы будем делать, мычать? Нет, мы готовы уже модальную престек теорию типов предоставить на конструкциях Гротендика --- такая основная мотивация пучкизма в теории типов, ублажить высших сантехников и более консистетно подойти к основаниям, чтобы они могли все в себя вобрать.
Аноним 30/04/20 Чтв 01:20:43 6817694
>>68168
>Все дело в том, что при желании это все работает в обеих направлениях.
нихуя не работает. Пока что выходит лишь записать тривиальные результаты 50-60х, при этом 90% времени тратится на формализмы, вместо математики. Приход программистов в математику ничего хорошего не дал в итоге, вместо решения реальных задач бесконечные новые формализмы.
Аноним 30/04/20 Чтв 01:26:04 6817795
>>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
Аноним 30/04/20 Чтв 01:34:16 6817896
>>68176
в каком то смысле это хорошо, потому что тогда математика сводится к медалистам Филдса. Математики могут успокоится, задача программистов не забирать их медали, а провести рефакторинг всей математики, очень неблагодарная но интересная деятельность. Задача оснований --- строить эффективные вычислительные модели или предлагать новые специализированные синтаксисы для каждого вида математик.
Аноним 30/04/20 Чтв 01:40:40 6817997
>>68178
> задача программистов не забирать их медали, а провести рефакторинг всей математики
Нельзя провести "рефакторинг" не зная что ты собственно рефакторишь. А уровень знания математики у программистов нулевой.
Аноним 30/04/20 Чтв 01:41:50 6818098
>>68179
Ну когда я говорю программисты я подразумеваю Воеводского. А ты очевидно подразумеваешь своего студента имбецила, который сайт кампуса на ПХП пишет.
Аноним 30/04/20 Чтв 02:00:14 6818199
>>68180
> А ты очевидно подразумеваешь своего студента имбецила, который сайт кампуса на ПХП пишет.
Речь скорее о ncatlab, о любителях пруверов и функционального программирования. Воеводский был жемчужиной среди всего этого сброда, с реальными математическими результатами в прошлом.
Аноним 30/04/20 Чтв 02:01:26 68182100
>>68177
> приложений в жизни
> two-dimensional exactly solvable statistical lattice models and its related Hamiltonians

Тебя спросили про приложение алгебраической геометрии в жизни, а ты приводишь статью на википедию, где перечислено программное обеспечение, интересно. Не хочешь задуматься, почему медалист Филдса пересел за комп?
Аноним 30/04/20 Чтв 02:03:45 68183101
>>68181
ncatlab и ведется студентами, я сам плачу студентам за статьи на ncatlab, это студенческий образовательный проект. Ты воюешь с ветряными мельницами.
Аноним 30/04/20 Чтв 02:07:25 68185102
>>68181
Воеводский был жемчужиной, а прувер написать не смог. Зато медаль получил, за пофиксаного Блоха-Като, рефакторер блядь. С-системы его ёбнутые. Ты реально переоцениваешь математиков.
Аноним 30/04/20 Чтв 02:20:06 68186103
>>68182
Уайлс за комп не пересел, до сих пор на бумажке считает. Или ты про того, который стал с шумом радио общаться?
Аноним 30/04/20 Чтв 02:22:43 68187104
>>68186
Нет, я ж не атакую, я ж признал, что нового не умеем производить, все что можем --- это по крупицам собирать то, что математики напридумывали используя их же методы, языки и модели. Вот и все. Да имбицильство, но оно качает, и тенуре нам не нада.
Аноним 30/04/20 Чтв 06:03:11 68188105
>>68179
> Нельзя провести "рефакторинг" не зная что ты собственно рефакторишь. А уровень знания математики у программистов нулевой.\t
Ага, а математика это согласно вашим сектантстким заповедям что?
Аноним 30/04/20 Чтв 08:49:54 68190106
>>68188
>Ага, а математика это согласно вашим сектантстким заповедям что?
Я не очень понимаю, на что постоянно погромисты обижаются. Ну вот Многие дисциплины просачиваются в другие области будь то humanities или естественнонаучные или инженерные, это нормально. Но глупо полагать, что в 21м веке ты можешь достичь хорошего понимания современных достижений в нескольких дисциплинах.

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

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

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

Поэтому все громкие утверждения насчёт важности пруверов серьёзно просто не воспринимаются из-за совершенной некомпетентности собеседников. Это уровень ферматистов и навьестоксеров.
Аноним 30/04/20 Чтв 09:08:19 68191107
>>68190
> есть совершенно чёткая область чистой математики.
Которая точно так же, как и любая другая, представима в HoTT. Ничего волшебного в чистых гамалогиях нет. Но, с точки зрения сектанта, писать гамалогии в прувере, а не на бумаге - это пиздец харам и неко мпетентность. Почему? Да вот потомучто.
Аноним 30/04/20 Чтв 09:28:30 68193108
>>68187
золотые слова

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

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

Да, С-системы Воеводского нужны были для модели его теории типов. Но она вроде сильно специализированная какая-то, конструктивая в каком-то смысле. А это значит, что классическую математику в ней не подоказываешь. (Ну может есть какой-то хитрый способ?) Ае сли не подаказываешь, то тогда разве это "основания математики"? Получается, что нет. Или что с точки зрения адептов hott, настоящей(тм) алгебре "не нужна" аксиома выбора? Все учебники переписывать? На конечных объектах -- может быть, ну а если чуть сложнее что...
Аноним 30/04/20 Чтв 09:50:39 68195109
>>68183

я человек простой: слышу про математику и деньги -- пишу свою фейкотелегу: puchkist
Аноним 30/04/20 Чтв 10:22:43 68196110
>>68190
А что такое современная математика, и можно ли ее где-нибудь применить? Или она такая ЧИСТАЯ, что нигде не применяется?
Аноним 30/04/20 Чтв 10:39:39 68197111
>>68193
> классическую математику в ней не подоказываешь. (Ну может есть какой-то хитрый способ?
Способ ровно тот же самый, что и в классической математике - без задней мысли берешь и прописываешь нужную заповедь. И о чудо, можно её использовать для "доказательства".
Аноним 30/04/20 Чтв 11:00:01 68198112
>>68193
>Да, С-системы Воеводского нужны были для модели его теории типов. Но она вроде сильно специализированная какая-то, конструктивая в каком-то смысле.

С-системы точно такая же копипаста как и CwF, CwA, только Воеводсткий использовал категории, объекты которых индексированые натуральными числами. В те времена еще не было модальной HoTT поэтому теории связанных топосов Ловира еще не было в пруверах, поэтому ясно что что в С-системах этальная математика не чекается. C-системы это изоморфизм universe categories.
Аноним 30/04/20 Чтв 11:02:12 68199113
>>68198
Нет никакой его теории типов. Есть теория типов и в рамках ее DIY модели, все равноправные. Кто больше математики в своих моделях закодирует тот и победил, это и будет показателем эффективности испольования прувера.
Аноним 30/04/20 Чтв 11:05:11 68200114
>>68199
С-системы как и все основание построенное Воеводским просто зажигало ребят вокруг за это ему спасибо, а так же теорию типов для своей же унивалентности Воеводский построить не смог. Построили программисты, так что спесь не то что с модульного деда, но и с лауреатов Филдса можно сбить при желании.
Аноним 30/04/20 Чтв 11:11:40 68201115
Boyarinya-moroz[...].jpg 159Кб, 700x487
700x487
>>68200
> теорию типов для своей же унивалентности Воеводский построить не смог. Построили программисты, так что спесь не то что с модульного деда, но и с лауреатов Филдса можно сбить при желании.
Мне меньше всего понятно, почему эти вещи вообще противопоставляются. Вот если отбросить сектантскую швятую веру уровня того, что креститься нужно не тремя, а двумя пальцами писать нужно на бумаге, а не в прувере, то какие аргументы остаются против HoTT?
Аноним 30/04/20 Чтв 11:12:47 68202116
>>68197
насколько я помню, если прописать аксиому выбора -- получишь противоречие с аксиомой унивалентности.
Аноним 30/04/20 Чтв 11:13:32 68203117
>>68202
Ну и что? Чекаться-то будет, что ещё нужно.
Аноним 30/04/20 Чтв 11:15:04 68204118
>>68201
Аргумент против HoTT см выше, для неё надо передоказывать все теоремы и неизвестно, содержится ли в ней модель ZFC.
Аноним 30/04/20 Чтв 11:15:58 68205119
>>68203
Тогда чекаться будет любая теорема, что неинтересно. Ex falso quodlibet
Аноним 30/04/20 Чтв 11:17:09 68206120
>>68201
Сейчас пруверы - бесполезное говно для 1,5 аутистов. Но если дать всей этой теме ход, то сразу появятся кабанчики, которые сверстают "нормальный прувер" и попросят бабки за его использование. Это подтолкнет журналы не принимать пруфы не заапрувленный пруверов от ООО Кабанчик Инт. Ну а дальше смерть и вырождение математики.
Аноним 30/04/20 Чтв 11:18:39 68207121
>>68206
Это очень оптимистичная программа, но я бы под ней подписался!
Аноним 30/04/20 Чтв 11:25:10 68208122
>>68205
В классической математике это никого не останавливает почему-то.
>>68206
Вот честно, бред какой-то уровня "аргументов" керосиновых магнатов против елестрического освещения.
Аноним 30/04/20 Чтв 11:28:19 68209123
>>68208
>Вот честно, бред какой-то уровня "аргументов" керосиновых магнатов против елестрического освещения.
Компьютиризация убивает искусство. И да компьютер есть и всегда будет беспросветно тупым.
Аноним 30/04/20 Чтв 11:30:10 68210124
>>67752
Ахуительные истории.
Аноним 30/04/20 Чтв 11:33:00 68211125
>>68191
>гамалогиях
Кроме этого слова больше ничего про "современную" математику не знаешь? Идее гомологий уже больше ста лет, а Э-С аксиомам уже лет так 70. Гомологии проходят на первых курсах, если что.
Вот классический пример - не знаю, о чём говорю, но буду прятаться за мемами вроде пучков и гамалогий, авось проканает и это поднимет авторитетность моего программистского мнения. Ну с этим иди в /sci/.
Аноним 30/04/20 Чтв 11:35:12 68212126
>>68211
Ты ж сам видишь, что по существу того поста не возразил. А все "аргументы" против свелись к >>68209
Аноним 30/04/20 Чтв 11:39:53 68213127
>>68212
Ты думаешь взяв "аргументы" в кавычки ты снизишь их значимость? Ну так, мой дорогой, в таком случае твои "аргументы" говно из жопы, как тебе такое?
Аноним 30/04/20 Чтв 11:48:40 68214128
>>68213
Значимость чего? Рандомных, ни на чём не основанных заявлений, что типа "буковы в прувере в отличие от таких же буков на бумаге - это не искусство"? Так у подобных заявлений и так никакой значимости нет, как я могу ее дальше снизить?
Аноним 30/04/20 Чтв 11:51:12 68215129
>>68208
Давай, если такой умный, строго докажи, что ZFC противоречива, верифицируй в любом прувере: гарантировано получишь премию Абеля.
Аноним 30/04/20 Чтв 11:51:49 68216130
>>68214
Просто иди нахуй.
Аноним 30/04/20 Чтв 12:02:36 68217131
schet-drevnih-s[...].jpg 53Кб, 624x433
624x433
>>68215
Ну либо противоречива, либо нет. Ты ж не против использования исключенного третьего в доказательстве? Тогда я считай доказал.
Аноним 30/04/20 Чтв 12:18:23 68218132
Аноним 30/04/20 Чтв 12:22:06 68219133
>>68217
А он вообще кто таков?
Аноним 30/04/20 Чтв 12:28:43 68220134
>>68206
я думаю вольфрам вскоре придет к пруверам
Аноним 30/04/20 Чтв 14:09:40 68231135
>>68212
>Ты ж сам видишь, что по существу того поста не возразил
Хорошо, давай по существу. Раз ты у нас охуенно какой математик, то тебе ничего не стоит отвечать по существу, верно? Так что я ожидаю развёрнутых ответов с пруфцами, а не балабольство и демагогию. Это всё-таки /math/, а не /pr/.

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

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

Жду демагогию, односложные ответы, мемы, шутейки, и увиливания.
Аноним 30/04/20 Чтв 15:06:26 68234136
>>68231
Может ли бумага доказывать теоремы?
Аноним 30/04/20 Чтв 15:08:33 68235137
>>68231
О, чувствую шизоидное обострение у модульного деда!
Аноним 30/04/20 Чтв 15:10:58 68236138
>>68231
Нужно нейронку, которая могла бы челотекст переводить в нагромождение логической поебени и потом уже этот километр текста скармливать пруфчекеру.
Аноним 30/04/20 Чтв 15:23:24 68237139
>>68220
Вольфрам знает математику еще меньше чем основатели, а теорию языков программирования вообще не знает.
Аноним 30/04/20 Чтв 15:36:36 68240140
>>68209
Ага, это сразу видно по бюджетам в области искусства и компьютерной графики.
Аноним 30/04/20 Чтв 15:47:22 68241141
>>68231
я не он, но отвечу тебе, раз уж ты такую пасту напечатал.

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

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

Поэтому на вопрос "могут ли" ответ: да. Тебе придётся долго писать пруф, но в итоге , если твои интуитивнве рассуждения верны, то получится
Аноним 30/04/20 Чтв 15:49:50 68242142
>>68241
Да модульному деду уже преподали теорию типов на пучках и конструкциях Гротендика, если это не помогло, то остальное вряд ли поможет.
Аноним 30/04/20 Чтв 15:50:48 68243143
>>68242
Пусть подоказывают еще 100 лет на бумажке, а дальше будет без вариантов :-)
Аноним 30/04/20 Чтв 17:37:17 68248144
>>68241
>Ты пишешь доказательство, а они проверяют, не ошибся ли ты.
Тут есть одна эмпирическая гипотеза: доказательство любой достойной теоремы невозможно записать в прувере. Только тривиальные вещи 19 века и всякую комбинаторику. На данный момент за 40 и более лет компьютерных доказательств исключений не было.
Аноним 30/04/20 Чтв 17:41:06 68249145
>>68248
Это правда, но уже лучше чем Principia Mathematica, согласись!
Аноним 30/04/20 Чтв 17:42:15 68250146
>>68249
Через 100 лет приходи.
Аноним 30/04/20 Чтв 17:59:08 68251147
>>68248
> Тут есть одна эмпирическая гипотеза: доказательство любой достойной теоремы невозможно записать в прувере.
Почему на бумаге можно?
Аноним 30/04/20 Чтв 18:02:54 68252148
>>68251
потому, что интересно только модульному деду, а он видимо не филдсовский медалист.
Аноним 30/04/20 Чтв 18:05:46 68253149
>>68252
тут хуй пойми, что он имеет ввиду под математикой: создание вычислительных практичных теорий для народного хозяйства, доказательство больших теорем, нахождение изоморфизмов, рефакторинг математики, упрощение, педагогика, создание новых дисциплин, просто медальки выдаваемые тайным обществом непонятно. Понятно только, что на бумаге главное, чтоб было ОК АРНОЛЬД
Аноним 30/04/20 Чтв 18:11:57 68254150
>>68253
Написать программу, которая сгенерирует статью по С-системам Воеводского в TeX из исходников и автоматически пошлет в журнал можно уже. А это, очевидно, настоящая математика, ее же чувак с медальками писал!
Аноним 30/04/20 Чтв 18:15:14 68258151
>>68254
тоже не понимаю этого ad hominem, есть международная классификация математики, её и держитесь
Аноним 30/04/20 Чтв 18:17:14 68259152
>>68251
Там многие формальности опускаются.
Аноним 30/04/20 Чтв 18:25:20 68262153
>>68241
>Тебе придётся долго писать пруф
Долго это порядка времени возврата Пуанкаре?
Аноним 30/04/20 Чтв 18:29:21 68263154
>>68262
Всё doable, просто математикам быстро надоедает пруф-терм дописывать, да и программисты быстро бросают. Нужны репрессии.
Аноним 30/04/20 Чтв 18:38:42 68266155
>>68263
Ну да выгнать всех программистов нахуй. А за упоминание cs major расстреливать из зенитки.
Аноним 01/05/20 Птн 08:28:17 68275156
>>68241
лол, как анон и предсказывал, он получил односложный ответ "да" без реальных пруфов и пояснений как и что
собственно, что и требовалось доказать, погромисты в реальной математике не шарят и по теме разговаривать не могут

>>68231
на этой доске всего 2.5 анона, которую даже второкурсный дифгем осилили, куда уж там потоки риччи
hottоёбы почитали определения категории и гомологии и теперь думают, что они "шарят"
не удивительно, что вербит перестал сюда заходить
Аноним 01/05/20 Птн 08:40:57 68276157
>>68275
> не удивительно, что вербит перестал сюда заходить
Так это всё-таки он был, форсил тут свою единственно верную религию, лол. Нет в математике боженьки кроме вербита, а модульный дед (поел говна на обед) - пророк его.
> лол, как анон и предсказывал, он получил односложный ответ "да"
> Вопросы, однозначно подразумевающие односложные ответы
> ответили односложно
> ррреее, я жи говорил
Что вы за люди, пиздец...
Аноним 01/05/20 Птн 09:21:49 68278158
>>68276
>> Вопросы, однозначно подразумевающие односложные ответы
Ну тогда это на уровне религии, так что пиздуйте со своими пруверами на другие доски.
Аноним 01/05/20 Птн 09:53:50 68279159
>>68278
> Ну тогда это на уровне религии
Что на уровне религии, рабочие программы? Братишка, чёт ты с горя совсем хуйню понес.
Аноним 01/05/20 Птн 10:43:08 68280160
>>68276
>> Вопросы, однозначно подразумевающие односложные ответы
>> ответили односложно
Так а зачем тогда было говорить, что, мол, анон по существу не ответил? А как только поступили вопросы по существу - оказывается, что это секта и по существу-то никто и отвечать не может, потому что программисты ничего не знают ни о дифференциальной геометрии, ни о пруверах.
Аноним 01/05/20 Птн 10:53:24 68281161
>>68280
> как только поступили вопросы по существу
Вопросов по существу не поступало. На вопросы модульного деда (да поест он говна на обед) уже много лет есть однозначный ответ - да, ничего волшебного на бумаге нет, все то же самое можно делать в прувере. Он же с позиции своей швятой веры утверждает, что это не так. Зачем-то даже в очередной раз создал подобный тред.
Аноним 01/05/20 Птн 15:34:56 68287162
>>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

Аноним 01/05/20 Птн 15:37:06 68288163
>>68287
>Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее.
Двачую, математика это прежде всего язык, все стремятся к ёмкости понятий, чтобы какую-нибудь сложную хуйню можно было выразить небольшим количеством символов, а тут всё наоборот.
Аноним 01/05/20 Птн 16:35:35 68290164
>>68287
> Так почему никто не делает?
Справедливости ради, таки делают. Просто ты как обычно не в теме https://github.com/UniMath/UniMath например, ещё Воеводского проект, до сих пор развивается.
> Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее.
В той же агде юникод поддерживается, всю нотацию можно переопределить как самому удобно и угодно. Насчёт неосиляторов соглашусь, там мозги нужны. Про лемму Йонеды не смешил бы тапки, она в хаскелле-то давным-давно есть.
Аноним 01/05/20 Птн 18:29:12 68293165
>>68290
>Про лемму Йонеды не смешил бы тапки, она в хаскелле-то давным-давно есть.
Лол, ты про частный случай? Тащи пруф в нормальной математической формулировке.

>Справедливости ради, таки делают. Просто ты как обычно не в теме https://github.com/UniMath/UniMath
опять ссылка на гитхаб с непойми чем и клеймо покойного Воеводского, будто он из рая дописывает. Присылай конкретные значимые теоремы из 20 века, тогда поговорим.
Аноним 01/05/20 Птн 18:33:54 68294166
>>68293
> гранаты формулировка у них не той системы
> ваш гитхаб не гитхаб, там буквы какие-то непонятные
Ясно.
> Присылай конкретные значимые теоремы из 20 века, тогда поговорим.
Значимые для кого? Вашей секты?
Аноним 01/05/20 Птн 20:21:15 68296167
>>68294
>Ясно.
Хуясно. Притащи для начала формулировку категории на хаскелле.

>Значимые для кого? Вашей секты?
Для математических предметов за первый и второй курс. Теорема о нулях, теорема стокса, теорема коши из ткфп...
Аноним 01/05/20 Птн 21:11:34 68298168
Быстро прувер-шизики слились, когда им притащили математики. Как и казалось изначально, это просто погромисты с когнитивным диссонансом, которым кажется, что в хаскеле настоящие категории, а в пруверах - настоящие теоремы.
Аноним 01/05/20 Птн 22:04:06 68299169
>>68293
> лемму Йонеды
> пруф в нормальной математической формулировке.
можно статью или скрин тайной леммы Йонеды?
Аноним 01/05/20 Птн 22:07:42 68300170
>>68298
> в пруверах - настоящие теоремы.
Ну что ты, настоящее ламповое только на бумаге, ровно то же самое на винте - уже не то же самое.
Аноним 01/05/20 Птн 22:17:48 68302171
>>68300
Только есть нюанс, что ошибки на бумаге можно найти. Ошибки в пруверах ты будешь искать намного медленней.
Аноним 01/05/20 Птн 22:18:15 68303172
Аноним 01/05/20 Птн 22:18:35 68304173
>>68296
HoTT делалась для автоматизации теории гомотопий или алгебраической топологии, а не для алгебраической геометрии. Для непосредственного управления вараятис нужно ввести в ядро вместо гомотопического интервала [0,1], афинный отрезок А^1 и это уже будет называться А^1-теория гомотопий. Т.е. если ты скажем хочешь Блоха-Като доказать, то тебе сначала нужно перейти в правильную систему типов для этого.
Аноним 01/05/20 Птн 22:21:02 68306174
>>68303
Ну это любой студент на агде выкладывает на гитхабе. Тут же ничего не нужно кроме теорката и построенной категории множеств. То, что в Хаскеле просто стертый терм до System F, хаскель-доказательство в качестве школьной программы можно защитать. В этом смысле это же можно доказать даже в NuPRL и старых пруверах.
Аноним 01/05/20 Птн 22:22:48 68307175
>>68302
> Ошибки в пруверах ты будешь искать намного медленней.
Ошибки прувер сам найдет
Аноним 01/05/20 Птн 22:23:35 68308176
Аноним 01/05/20 Птн 22:25:14 68309177
>>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))
Аноним 01/05/20 Птн 22:27:36 68310178
Аноним 01/05/20 Птн 22:33:14 68311179
DprDVb3UUAEdUzB.jpg 115Кб, 960x640
960x640
Аноним 01/05/20 Птн 22:37:21 68312180
>>68311
СЖВ за классическую математику?
Аноним 01/05/20 Птн 22:38:23 68314181
>>68312
так мы видим этот тред
Аноним 01/05/20 Птн 22:54:27 68316182
>>68287
>Classification of Finite Simple Groups
сразу видно воинственного неадеквата
Аноним 01/05/20 Птн 22:56:12 68317183
>>68316
особенно смешно то, что единственное полное доказательство этой теоремы существует только на компьютере :-)
Аноним 01/05/20 Птн 23:06:50 68318184
248207644333307[...].jpg 342Кб, 953x1015
953x1015
Аноним 01/05/20 Птн 23:25:35 68319185
>>68317
так и другие доказательства на компьютере, но не в прувере.
Аноним 02/05/20 Суб 00:51:20 68322186
>>68307
>Ошибки прувер сам найдет
>Вера в всемогущий безошибочный компьютер
О как это знакомо.
Аноним 02/05/20 Суб 01:19:39 68323187
>>68318
Пруферы гомотопические, а классификация простых конечных групп конструктивна?
Аноним 02/05/20 Суб 01:21:03 68324188
>>68323
конструктивная, она в CAS системах считалась
Аноним 02/05/20 Суб 02:41:15 68325189
image.png 946Кб, 800x1200
800x1200
>>68162
>а напомните нам нахуя нам 87-я гомотопическая группа трехмерной сферы ?
У МЕНЯ ЗА ТАКИЕ ВОПРОСЫ В ХАРВАРДЕ УБИВАЮТ НАХУЙ ПУЧК ГРОТ СТАТЬИ ПИСАТЬ НАДО ПОВТОРЯЮ ПОВТОРЯЮ СТАТЬЯ ПО 87-тую ГРУППУ ТРЁХМЕРНОЙ СФЕРЫ НЕ ТОЖЕ САМОЕ ЧТО СТАТЬЯ ПОСВЯЩЕННАЯ ОДНОМУ КОНКРЕТНОМУ-НМУ ИНТРЕГАЛУ ПУУЧК ГРООТ ДИДИ ИЗ МГУ ПИШУТ ПРО ИНТЕГРАЛЫ СТАТЬИ И НЕ СТЫДНО КАК В НИГЕРИИ БУДЕМ ГРОООТ
Аноним 02/05/20 Суб 07:44:20 68327190
>>68322
Про тайпчекинг не слышал?
Аноним 02/05/20 Суб 09:14:34 68328191
>>68327
Лол блядь
Тут погромисты походу ни математики, ни программирования не знают
Тайпчекинг, кек
Весь тред это один большой COPE второкурсников с CS
Аноним 02/05/20 Суб 10:27:47 68333192
>>68328
Опять пук в лужу и швятая вера, что на бумаге можно сделать больше чем в прувере.
Аноним 02/05/20 Суб 11:58:35 68347193
>>68333
Есть ли в программах баги?
Аноним 02/05/20 Суб 12:08:17 68348194
>>68328
Это классическая проблема детей верующих в всезнающий всемогущий комплюктер. В силу того, что они в этой жизни еще нихуя не сделали, они не понимают, что такого не так в их вере.
Воеводский безусловно был первоклассным математиком, но своими унивалентыми основаниями он открыл дорогу всякому cs сброду дорогу туда, где ему быть никогда не следовало.
Аноним 02/05/20 Суб 13:10:40 68353195
>>68298
Программистам не упало таким заниматься, на самом деле.
Аноним 02/05/20 Суб 13:24:27 68355196
>>68333
>швятая вера
Ну вас шизиков напрямую спросили - покажите, как работает на примере любой из фундаментальных теорем 20го века, например теорема об индексе
Кто-то настрочил про гипотезу Пуанкаре, тоже тишина в ответ, неловкое "ну да, это можно..."

Пока что это выглядит как религия. Когда меня не аргументами убеждают, а просят поверить - интерес сразу пропадает. Может, поэтому в этой области нормальных математиков нет, и привлекает она одних только горе-питонистов.
Аноним 02/05/20 Суб 13:42:52 68356197
>>68355
> Пока что это выглядит как религия. Когда меня не аргументами убеждают, а просят поверить - интерес сразу пропадает.
Кому ты нужен, в чем-то тебя убеждать? И где и кто тебя просит поверить? Сам на протяжении нескольких лет создаёшь эти треды, сам потом в них горишь. Зачем? Веруешь во швятую бумагу и бездушные кудахтеры - веруй, свободу вероисповедания не отменяли.
Аноним 02/05/20 Суб 13:55:17 68357198
>>68356
А у кудахтеров появилиась душа?
Аноним 02/05/20 Суб 15:27:08 68360199
>>68298
Тебе кажется, что в топовых пруверах не настоящие теоремы, просто потому что ты пока мало знаешь используемую в них математику. Я тоже раньше не знал и поэтому сомневался.
Аноним 02/05/20 Суб 15:37:17 68361200
А зачем нужны пруверы? Ведь в док-вах сложных теорем есть какие-то куски, из которых потом развивают новую теорию. Если всё будут проверять компы то эти куски останутся незамеченными.
Аноним 02/05/20 Суб 15:38:27 68362201
>>68360
>Тебе кажется, что в топовых пруверах не настоящие теоремы
Да тут нечему казаться - привели пример реальных, настоящих, теорем. Ответа по существу (как тут любит один) - не было. Я вот знаю математику, используемую в гипотезе Тёрстона или той же теореме Атьи-Зингера (не зря заканчивал, теперь могу щитпостить на двоще). Ну так и где они в пруверах? Или моего уровня недостаточно?
Аноним 02/05/20 Суб 15:40:41 68363202
>>68362
Я видел десятки академиков которые печатаются в АлгТопе но не могут на компьютере Пифагора записать и что? Там другая математика, и практика нужна.
Аноним 02/05/20 Суб 15:48:19 68364203
>>68347
Если программа написанная на сертифицированном прувере или языке, то любая программа в нём является валидным термом в топосе. Тотальное избавление от ошибок и переход в кванторы --- это и есть главная мотивация бездушевной математики.
Аноним 02/05/20 Суб 15:50:20 68365204
>>68363
Прости, я еще хотел поинтересоваться, а Квиленновские Модельные Категории, Модельные Структуры и Гомотопические Категории --- это как, настоящая математика для модульного деда или нет?
Аноним 02/05/20 Суб 17:39:00 68368205
>>68296
>Для математических предметов за первый и второй курс.
Я думаю такие вещи в пруверах точно можно записать, просто он скорее всего не знает математики даже на таком уровне.
Аноним 02/05/20 Суб 17:40:50 68369206
Аноним 02/05/20 Суб 17:44:06 68370207
>>68348
Будто без него это не обмякнет, жидко пукнув.
Аноним 02/05/20 Суб 17:51:17 68371208
>>67751
Отвратитетельная на значит бесполезная, говно тоже чистить нужно, но неприятно, так и тут, они бы с большим удовольствием перекинули это на кого-нибудь другого.
Аноним 02/05/20 Суб 17:57:43 68372209
>>67946
>А кому-то мастурбация помогает понять материал, мы будем на основе этого делать выводы насчёт её роли в современной математике?
И найти решение тоже помогает.
Аноним 03/05/20 Вск 09:05:32 68385210
>>68287
как минимум лемма Йонеды и теорема Гёделя верифицированы.

Это не модульный дед создал тред, это я, просто гораздо лучше было бы, если бы классические основания математики были такими вирусными. Верифицировать долго, но реально: и чем дальше, тем быстрее получается
Аноним 03/05/20 Вск 09:12:17 68386211


>>68310
там про неполноту речь, она верифицирована много где
полнота кстати попроще и тоже верифицирована в разных системах.
Аноним 03/05/20 Вск 10:49:56 68387212
>>68371
На всякий случай, я лично не люблю ни программировать, ни делать тяжеловесных выкладок (и, слава Аллаху, в той математике которой я занимаюсь можно обойтись без обоих). Но если сравнивать такие активности и речь идет о выкладках которые настолько механическая и трудоемкая ерунда, что их рационально автоматизировать, то запрограммировать эту автоматизацию явно привлекательнее.
Аноним 03/05/20 Вск 12:40:25 68390213
>>68385
напиши чуваку с сайта, чтобы обновил.
Аноним 03/05/20 Вск 22:21:19 68399214
Аноним 12/05/20 Втр 14:43:10 68708215
Аноним 13/05/20 Срд 12:18:28 68749216
df825d725ceb0de[...].jpg 9Кб, 480x360
480x360
>>68385
> Это не модульный дед создал тред, это я
Аноним 13/05/20 Срд 14:54:48 68755217
Аноним 16/05/20 Суб 02:20:38 68886218
Homotopy.gif 2Кб, 330x180
330x180
Гомологии, гомотопии это же из топологии, так? А как это связано с основаниями математики и доказательствами вообще, объясните.
Аноним 16/05/20 Суб 02:24:46 68887219
image.png 552Кб, 435x650
435x650
Аноним 16/05/20 Суб 05:50:41 68888220
>>68887
Перевод: сам я нихуя не понимаю, потому что ещё учусь (на погромиста), но звучит очень понтово.
Аноним 16/05/20 Суб 08:28:48 68889221
image.png 370Кб, 720x405
720x405
>>68888
А ну говори, каким Браузером пользуешься.
Аноним 16/05/20 Суб 11:07:03 68890222
>>68889
>А ну говори, каким Браузером пользуешься.
Каким-каким, интуиционистским - Brouwer: "On the significance of the principle of excluded middle in mathematics, especially in function theory."
Аноним 16/05/20 Суб 11:19:52 68891223
>>68887
Я статью на вики не понял.
Аноним 16/05/20 Суб 16:02:08 68899224
>>68891
А в этом и смысл
Аноним 16/05/20 Суб 17:32:08 68903225
1) вначале всё свели к натуральным числам.
2) потом решили, что лучше брать за основу множества, так как натуральные числа можно определить в теории множеств как вторичные объекты, а наоборот нельзя
3) потом пришёл Рассел и всё решил свести к формальной логике - так появилась первая теория типов
«Тот факт, что вся математика есть не что иное, как символическая логика, — величайшее открытие нашего века».
4) потом математики поняли, что типы первичны над логикой. На самом деле фактически это показал тот же Рассел, но он не понял этого, полагая первичной логику.
5) работа Бурбаки описывает всё через порождающие структуры http://inponomarev.ru/teaching/speciesofstructures - вот тут по ссылке учебный курс по теории множеств и по структурам Бурбаки. Порождающие структуры по Бурбаки - это по сути типы аксиом. Некоторое среднее решение вопроса о первичности между теорией типов и логикой. При этом в своём роде окончательное - не вдаваясь в конкретное содержание, все матобъекты представляют собой структуры Бурбаки.

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

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

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

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

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

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

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

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

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

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

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

-> на основе этого изоморфизма можно создать гомологическую теорию типов, которая описывает любой математический объект на основе "истинно фундаментальных" - симметрий семантик.
Аноним 16/05/20 Суб 18:43:33 68907226
Аноним 16/05/20 Суб 18:44:43 68908227
>>68903
> Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.
это интересно, в какой книжке бурбаки можно прочитать про категории?
Аноним 16/05/20 Суб 21:44:36 68925228
Аноним 17/05/20 Вск 05:16:51 68932229
>>68908
Topologie algébrique. Chapitres 1 à 4.
Написана посмертно с того света и впервые издана в 2016.
Аноним 17/05/20 Вск 06:01:25 68934230
>>68908
А я люблю обмазываться современным категорным калом и дрочить. Каждый день я хожу по доске с черным мешком для мусора и собераю в него весь категорный кал, который вижу. На два полных мешка целый день уходит. Зато, когда после тяжёлого дня я прихожу домой, иду в тред для начинающих, говорю новичкам, что их математика не математика…ммм и измазываю тред категориями. И дрочу, представляя, что меня поглотила единая категория. Мне вообще кажется, что категории, умеют думать, у них есть свои семьи, города, чувства, не смывайте их в унитаз, лучше приютите у себя, говорите с ними, ласкайте их…. А вчера в ванной, мне преснился чудный сон, как будто я нырнул в море, и оно прератилось в копредел, функторы, кольца, поля, все из говна, даже первая культура, даже Аллах!.
Аноним 17/05/20 Вск 08:06:17 68938231
>>68934
(типичные размышления деда с dxdy о современной математике)
Аноним 17/05/20 Вск 13:41:26 68944232
Аноним 19/05/20 Втр 20:45:55 69055233
Аноним 09/10/20 Птн 23:03:17 74477234
Почему теоремы в университете заставляют писать на листочке, а не вводить в прувер?
Аноним 10/10/20 Суб 07:24:06 74488235
>>74477
Потому что математика, а не программирование.
Как там пруверы, уже хотя бы теоремы ХХ века вроде теоремы об индексе могут доказать?
Аноним 10/10/20 Суб 17:18:28 74504236
>>74488
Так программы тоже раньше на листочке писали, но потом поняли, что так ошибки могут появится. Так и с теоремами, тем более учитывая изоморфизм Карри-Говарда однозначно связывающий математику и программирование.

Базу теорем же люди введут, при том более профессиональные, так что риск ошибки из-за человеческого фактора понижается. А на листочке что? Даже не проверит толком никто.
Аноним 10/10/20 Суб 23:06:44 74531237
>>74504

а) В пруверах ничего внятного и интересно не доказано.
б) Читать пруверские доказательства это просто пиздец, а то что их проверил компилятор не дает никакого приемущества, все и так знают про большинство гипотез верные они или нет. Это то же самое, что музыку играть в миди проигрывателях, можно, если тебе лично это нужно зачем-то.
Аноним 11/10/20 Вск 15:47:29 74543238
>>74477
Потому что тебя, долбоеба, пытаются научить думать. Вероятно зря.
Аноним 11/10/20 Вск 21:16:32 74552239
>>74504
>тем более учитывая изоморфизм Карри-Говарда однозначно связывающий математику и программирование.
Ох лол, даже не знаю, ты просто тролль зелёный или ещё юный и наивный.
На твой изоморфизм всем похую также, как похую, например, на теорему Кэли о группах, которая вроде как и важная, а нигде никогда не применяется, потому что себе дороже.
Ещё раз, где моя теорема об индексе в прувере? Ну раз изоморфизм, то это вообще на раз-два.
Аноним 11/10/20 Вск 22:54:32 74555240
>>74504
>однозначно связывающий математику и программирование.
Только конструктивную её часть, а это 0.00001% от всей математики.
Аноним 14/10/20 Срд 05:49:41 74700241
>>74531
>>74552
>>74555
Ты же сам понимаешь, что твои "аргументы против пруверов" доказывают только то, что те, кто считает себя математиками, в 99 случаев из 100 не могут в пруверы, ибо деревянные по пояс. "Дело было не в бобине", как говорится. Если бы ты понимал, о чем вообще изоморфизм Карри-Говарда, ты бы не нёс такую хуйню. А так, имеем то что имеем...
Аноним 14/10/20 Срд 07:44:42 74702242
>>74700
> те, кто считает себя математиками, в 99 случаев из 100 не могут в пруверы, ибо деревянные по пояс.
Это не голословное утверждение, кстати. Года три ещё назад Сохацкий писал, что ихние академики не могут даже установить HoTT либу в коке. Агду с нужными либами какой-нибудь условный Вербицкий даже установить не осилит, про использование я вообще молчу
Аноним 14/10/20 Срд 07:56:23 74703243
>>74702
> Агду с нужными либами какой-нибудь условный Вербицкий даже установить не осилит, про использование я вообще молчу
Миша вообще в линуксе сидит, насколько я помню
У вас спесь головного мозга в последней стадии, классическое "вы не понимаете, это настолько сложно, что большинство математиков даже не смогут установить, не то что использовать"
Ну и логическая ошибка обобщения, как всегда у программистов

хотт-верунов просят уже который раз показать пример доказательства сколько-нибудь содержательной теоремы вроде теоремы об индексе, а они всё уводят разговор на какую-то нерелевантную солому
"Нет, пока доказать ничего нельзя, но зато УСТАНАВЛИВАТЬ нужно ууууух как сложно, да"
Аноним 14/10/20 Срд 08:08:29 74704244
>>74703
> Миша вообще в линуксе сидит, насколько я помню
Сейчас каждый первый нитакойкаквсе зумер в линуксе сидит.
Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.
Аноним 14/10/20 Срд 09:58:58 74705245
Но на самом деле с пруверами в плане установки все не так печально. Есть мейд ин Блинолопатия прувер - arend, там не только HoTT искаропки и даже дополнительная либа с кубической теорией типов, но и установка в один клик мышкой, как плагин к intellij idea, что в свою очередь ставится в два клика https://arend-lang.github.io/ так что прогресс налицо, скоро HoTT будет доступна широким народным массам, в том числе и мнящим себя математиками неосиляторам. Нотацию все равно осиливать придется, правда
Аноним 14/10/20 Срд 10:08:12 74706246
О, там новый релиз, теперь основная либа тоже ставится в один клик. Короче, хоть на это переползайте, раз уж даже агду поставить не можете.
> Plugin updates:

> arend-lib can be downloaded and upgraded from the IDE
Аноним 14/10/20 Срд 11:27:10 74708247
>>74700
>>74700

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

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

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

Никто не спорит, можно и на КОБОЛЕ доказать, только нахуя? Времени это займет много, новизны никакой не будет, а людям жрать что-то надо.
Аноним 14/10/20 Срд 12:43:11 74711248
>>74700
>Если бы ты понимал, о чем вообще изоморфизм Карри-Говарда
Так я понимаю, потому и пишу
>Только конструктивную её часть, а это 0.00001% от всей математики.
Аноним 14/10/20 Срд 12:43:38 74712249
>>74704
>Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.
Ну то есть ни одной вразумительной теоремы современной актуальной математики хотя бы ХХ века, доказанной с помощью прувера образца 2020 года, ты привести не можешь, как и ожидалось.
Так и сказал бы, что ты пустозвон. Пердежу-то на всю доску от тебя.
Аноним 14/10/20 Срд 13:11:54 74718250
>>74711
Если бы понимал, то не писал бы такую хуйню.
>>74712
Когда докажут - ты будешь точно так же кукарекать.
>>74708
> можно и на КОБОЛЕ доказать
Нельзя, он тьюринг-полный, сначала придется прувер на нем писать.
> нахуя? Времени это займет много, новизны никакой не будет
Автоматизация. Что-то простое человек доказать может, что-то посложнее - уже нет. Доказательство чего-то нетривиального в IUTeich человек просто не осилит, никакой. А это ещё не самое сложное.
Аноним 14/10/20 Срд 13:36:35 74720251
>>74718

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

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


Аноним 14/10/20 Срд 13:43:13 74722252
>>74720
> больше похоже на модную хуйню: денег освоят и забудут.
Вообще ничем не похоже.
Аноним 14/10/20 Срд 14:19:47 74727253
>>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

Аноним 14/10/20 Срд 15:18:10 74732254
>>74718
>Если бы понимал, то не писал бы такую хуйню.
Так это ж про тебя, а не про меня.
Аноним 15/10/20 Чтв 09:56:31 74810255
>>74718
>Когда докажут - ты будешь точно так же кукарекать.
Нет, если реально докажут что-то, и это будет не ад хок хуита, адаптированная специально для одной единственной теоремы, то я соглашусь, что это круто, и может даже почитаю что-то.

А пока вы все со своими хотт, категориями в хаскеле, и записями лекций в имакс сидите у меня в одной корзине погромистов-второкурсников и лукавых грантопильщиков.
Аноним 15/10/20 Чтв 18:10:53 74820256
>>74810
> А пока вы все со своими хотт, категориями в хаскеле, и записями лекций в имакс сидите у меня в одной корзине погромистов-второкурсников и лукавых грантопильщиков.
Это неудивительно, ты ж даже не понимаешь, о чем не только HoTT, но даже тот же изоморфизм Карри-Говарда.
Аноним 15/10/20 Чтв 21:46:38 74826257
Аноним 16/10/20 Птн 09:52:44 74835258
>>74820
>Это неудивительно, ты ж даже не понимаешь, о чем не только HoTT, но даже тот же изоморфизм Карри-Говарда.
Тут больше одного анона сидит, если что.
Аноним 16/10/20 Птн 19:49:11 74860259
>>74820

Я так понимаю, там принцип как у теорем существования. В случае, если есть доказательство обычное, то существует и на прувере и можно его написать. Последний шаг, разумеется, остается как упражнение для любопытных студентов и пенсионеров.
Аноним 17/10/20 Суб 08:52:42 74897260
>>68197
>>68191
>>68201
>>68203
>>68208
И много других постов от этого мерзкого ублюдка. Граждане математики, обратите внимание, в треде орудует чмо, которое математику не знает, ни одного математического определения не использует, дабы не обосраться(хотя с зфс однажды все же обосрался), и пытается мимикрировать, отвечая односложно в духе "ваша математика - религия, коткудахкудахтахтах ", "почему нет, и что с того" и прочими мусорными способами, уводя дискуссию. Я сам сюда захожу редко, однако сейчас у меня было хорошее настроение, я пил чай, думал над темой магистерской и тут это программистское чмо мне испортило настроение. Посему :

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

Всех благ, господа математики.
Аноним 17/10/20 Суб 09:06:50 74898261
>>74897
Платонист, спок
Аноним 17/10/20 Суб 09:14:39 74899262
>>74897
Это ты ещё не видел шедевр программирования на С++ >>74894 →
Аноним 17/10/20 Суб 09:45:48 74900263
Ип
Аноним 17/10/20 Суб 14:18:54 74904264
Воеводский сам что-то доказал с помощью hott?
Аноним 17/10/20 Суб 22:39:22 74911265
>>74897

>Я так понимаю, там принцип как у теорем существования.
Ты вот на это мне ответь, я правильно понимаю ваш езормфизъмъ?
Аноним 18/10/20 Вск 00:09:29 74912266
>>74897
Он был здесь ещё до появления доски, чувак.
Аноним 18/10/20 Вск 03:34:27 74917267
>>74912
Ну или не он, но сомневаюсь, что есть два таких конструктуха.
Аноним 28/10/20 Срд 00:28:28 75296268
Аноним 28/10/20 Срд 12:47:24 75303269
>>75296
Упоротый, даже лекцию прочитал на тему статьи. Конструктухи это клуб фанатиков, я не видел, чтобы какой-нибудь Лури носился по миру и орал "5 шагов принятия высших категорий", "высшие топосы это будущее математики, умоляю, используйте их в доказательстве" итд итп.
Аноним 28/10/20 Срд 16:23:01 75312270
>>75303
Если ты чего-то не видел, это не значит, что этого не было.
Аноним 08/01/21 Птн 06:40:08 78718271
>>67659 (OP)
было несколько знакомых пациентов лет пять назад, все так или иначе относились к СПбАУ.
Аноним 14/01/21 Чтв 20:27:31 79009272
>>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льтат или нет.
Аноним 15/01/21 Птн 16:38:12 79061273
>>79009
>Человек --- меpа вcех вещей.
Протагор, залогинься
Аноним 15/01/21 Птн 19:46:21 79072274
>>67659 (OP)
А что это за бублик на оп пике?
Аноним 17/01/21 Вск 22:24:23 79160275
>>68185

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

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

"Скажите, как его зовут?" (с)
Аноним 17/02/21 Срд 21:14:59 80424276
Господа, а вот там Тифарет в своем тифаретнике пишет, что фигурант данного треда продолжительно продолжал употреблять вещества группы диссоциативов, в частности на букву К.

может кто-нибудь из присутствующих фармакологов объяснить неопытному посетителю чисто для кругозора, к каким наблюдаемым симптомам приводит употребление данного круга веществ? как это могло сказаться на фигуранте обсуждения?
Аноним 17/02/21 Срд 23:21:52 80432277
>>80424
он там про шеня что-то написал, то ли хуесосит а шень няшный, то ли имеет в виду что-то своё, понятное только близким друзьям. Я не понял

А где он про "фигурант данного треда" пишет, я не вижу
тоже темнишь что-то
Аноним 17/02/21 Срд 23:49:37 80433278
>>80424
По первым же ссылкам из гугла описываются симптомы, похожие на то, что рассказывал фигурант

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

> дезориентированы, испытывают ощущение, что они "находятся в другом измерении", "общаются с Богом", "с дьяволом", переносятся в другие места, слышат какую-то особую "неземную" музыку и пр. Некоторые лица в период интоксикации ощущают безграничные творческие способности: им кажется, что они сочиняют музыку, складывают стихи, им приходят в голову удивительные фасоны одежды и пр.
Аноним 18/02/21 Чтв 00:04:14 80435279
>>80424
>фигурант данного треда
Иди нахер с таким жаргоном. Полицейщина мерзкая.
Аноним 18/02/21 Чтв 05:56:32 80438280
>>80432
>А где он про "фигурант данного треда" пишет, я не вижу
В некрологе на Воеводского и пишет.
Аноним 18/02/21 Чтв 09:29:31 80440281
>>80435
разве "нулевой пациент" существенно благозвучнее? хм.
Аноним 18/02/21 Чтв 09:35:32 80441282
>>80433
>им приходят в голову удивительные фасоны одежды и пр.
удивительные фасоны оснований математики, ага.
Аноним 20/02/21 Суб 07:50:01 80512283
>>79160
Петух - конструктух.

Я его ещё здесь:>>74897 описал.
Аноним 20/02/21 Суб 12:30:42 80518284
>>80512
а вдруг их несколько? или они размножаются...
Аноним 21/02/21 Вск 12:39:37 80566285
Вопрос к адептам и сектантам. Сегодня, а может и давным давно, мне во сне явился ангел. Мы перетерли за математику. Произошло озарение.

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

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

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

2. Гомотопический тип - это хороший предпучок и на дельте, и на кубиках. С гаммой и сим-оп все сложнее. Хороший симплициальный предпучок на гамме - это связный спектр. Хороший предпучок на сим-оп, со значениями в категории симплициальных множеств с отмеченной точкой, - это спектр, не обязательно связный. Раз в одном случае эквивалентность есть, а в другом эквивалентности нет, оба случая нетривиальны и содержательны. Hott как-нибудь помогает увидеть это нетривиальное содержание?
Аноним 21/02/21 Вск 12:59:55 80570286
>>80566

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

если вы обращали внимание, то Сова хвалит Лури, который тоже увлекался именно эти клеточными комплексами, но зато Каледин ругает. и для того есть причины.
Аноним 18/03/21 Чтв 12:51:22 81561287
>>80570
...И причины эти в том, что Каледин Иванова дураком считает.
Аноним 18/03/21 Чтв 14:33:11 81575288
>>81561
типа сидит каледин такой, на лурье подрачивает, утомился, зашёл в блог совы... ба! а сова, оказывается, лурье любит! быстрее побегу, напишу, как я лурье не выношу вообще
Аноним 18/03/21 Чтв 18:27:40 81591289
>>81575
Побегу и напишу
@
Как лурье не выношу

Матемачу давно не хватает частушек. И гармониста.
Аноним 22/03/21 Пнд 01:13:58 81692290
>>80570
ок, выкинули, дальше какие инструкции будут?
Аноним 23/03/21 Втр 01:19:23 81733291
>>81591
Вышел модуль на крыльцо
Расширить себе кольцо
Сунул функтор нет кольца
Так и шлёпнулся с крыльца
Аноним 23/03/21 Втр 14:41:00 81742292
>>81733
Можно вместо "расширить" использовать "растянуть"?
Аноним 23/03/21 Втр 16:19:13 81743293
>>68202
Нормально там всё, книгу‐то открой хотя бы.
Настройки X
Ответить в тред X
15000
Макс объем: 40Mб, макс кол-во файлов: 4
Кликни/брось файл/ctrl-v
Стикеры X
Избранное / Топ тредов