81 Кб, 480x360ОПРОСИК
Господа и дамы, сообщите хотя бы частичную информацию: когда, а главное - где и/или от кого вы узнали про homotopy type theory? Нужно отследить цепочку распространения заразы вплоть до нулевого пациента. (понятно кого)
Господа и дамы, сообщите хотя бы частичную информацию: когда, а главное - где и/или от кого вы узнали про homotopy type theory? Нужно отследить цепочку распространения заразы вплоть до нулевого пациента. (понятно кого)
На двачах. Несколько лет назад, ещё когда не было этой доски и маттетреды были в /sci. От местного конструктивиста.
>>67659 (OP)
Что в ней плохого, объясните?
Что в ней плохого, объясните?
Учился на физика @ кафедра физики частиц @ хочу быть теоретиком @ КТП @ БРСТ @ когомологии @ топология...
Трактор @ хочешь остаться - давай считай количественный результат @ компьютер программировать @ Haskell @ Ocaml @ Coq @ Воеводский @ HoTT
Как-то так.
Трактор @ хочешь остаться - давай считай количественный результат @ компьютер программировать @ Haskell @ Ocaml @ Coq @ Воеводский @ HoTT
Как-то так.
>>67710
Эх, друже, после нормальной математики хаскелом занялся...
остальное - клёвые вещи, так держать
Эх, друже, после нормальной математики хаскелом занялся...
остальное - клёвые вещи, так держать
>>67731
не увидел в его посте высокомерия, честно говоря
что нравится, тем и занимайся
но сравнивать хаскелл с математикой, скажем, брст вполне себе можно объективно
то, что она в разы или даже на целые порядки проще в первом случае, тебя волновать не должно, если тебя интересует эта область
не он, но брст я проходил
если под деградацией понимать уменьшение сложности, то да
это как учиться лет 10 в музыкалке и консерватории, чтобы потом играть собачий вальс одним пальцем
>Почему математики такие высокомерные?
не увидел в его посте высокомерия, честно говоря
что нравится, тем и занимайся
но сравнивать хаскелл с математикой, скажем, брст вполне себе можно объективно
то, что она в разы или даже на целые порядки проще в первом случае, тебя волновать не должно, если тебя интересует эта область
>деградация
не он, но брст я проходил
если под деградацией понимать уменьшение сложности, то да
это как учиться лет 10 в музыкалке и консерватории, чтобы потом играть собачий вальс одним пальцем
>>67731
Хаскель это грааль теории категорий, которая в свою очередь является программироваем и второй культурой.
Хаскель это грааль теории категорий, которая в свою очередь является программироваем и второй культурой.
>>67733
Ну не то, чтобы там была какая-то особо замысловатая теория категорий.
>>67659 (OP)
Уже довольно давно (лет 8 назад), когда я учил логику.
>Хаскель это грааль теории категорий
Ну не то, чтобы там была какая-то особо замысловатая теория категорий.
>>67659 (OP)
Уже довольно давно (лет 8 назад), когда я учил логику.
>>67733
Что такое вторая культура?
Что такое вторая культура?
>>67738
Если ты уже веришь в реальность вне-временных бесконечных объектов, что очень естественно для математиков, то почему бы еще не принять бога.
Если ты уже веришь в реальность вне-временных бесконечных объектов, что очень естественно для математиков, то почему бы еще не принять бога.
>>67731
На самом деле я больше по Coq / OCaml, а не по Хаскелю.
Соглашусь, что занятие теорией/математикой, так сказать, "на бумажке" -- это чуть более "возвышенная" деятельность, чем запрограммировывание пусть и того-же самого. С другой стороны, мне, как физику, приятно видеть как мои идеи реализовываются "в железе". Кроме того, у меня довольно хаотичное мышление - физически не могу исписывать 40 листовые тетрадки выкладками как некоторые коллеги. Компьютер помогает организовывать и проверять -- Coq мне находил пару нетривиальных ошибок в моих построениях.
Т.е. я бы на "это деградация?" ответил что это вопрос вкуса и личных предпочтений, но... Не знаю как оно у математиков, но среди физиков наблюдал неоднократно что навык программирования вызывает у многих чувство некоего такого испуганного раздражения. Особенно если автоматизировать какую-нибудь муторную символьную выкладку - могут почти открыто злиться на тебя. И вот это довольно сложно объяснить только тем, что это им "не интересно".
это >>67733 не я
>А ты, физик, сам как считаешь, то что ты докатился до хаскеля,
На самом деле я больше по Coq / OCaml, а не по Хаскелю.
> это деградация?
Соглашусь, что занятие теорией/математикой, так сказать, "на бумажке" -- это чуть более "возвышенная" деятельность, чем запрограммировывание пусть и того-же самого. С другой стороны, мне, как физику, приятно видеть как мои идеи реализовываются "в железе". Кроме того, у меня довольно хаотичное мышление - физически не могу исписывать 40 листовые тетрадки выкладками как некоторые коллеги. Компьютер помогает организовывать и проверять -- Coq мне находил пару нетривиальных ошибок в моих построениях.
Т.е. я бы на "это деградация?" ответил что это вопрос вкуса и личных предпочтений, но... Не знаю как оно у математиков, но среди физиков наблюдал неоднократно что навык программирования вызывает у многих чувство некоего такого испуганного раздражения. Особенно если автоматизировать какую-нибудь муторную символьную выкладку - могут почти открыто злиться на тебя. И вот это довольно сложно объяснить только тем, что это им "не интересно".
это >>67733 не я
>>67659 (OP)
Интервью с Воеводским.
>, а главное - где и/или от кого вы узнали про homotopy type theory?
Интервью с Воеводским.
>>67741
Просто пограмирование отвратительный аутизм и тупость, вполне понятно, что адеквату неприятно марать этим мозг.
Просто пограмирование отвратительный аутизм и тупость, вполне понятно, что адеквату неприятно марать этим мозг.
>>67745
Ты правда считаешь, что программирование хуже чем та деятельность, которую оно автоматизирует?
Как по мне, автоматизация нудных выкладок, о которой пишет >>67741, это безусловно позитивная вещь.
>Просто пограмирование отвратительный аутизм и тупость, вполне понятно, что адеквату неприятно марать этим мозг.
Ты правда считаешь, что программирование хуже чем та деятельность, которую оно автоматизирует?
Как по мне, автоматизация нудных выкладок, о которой пишет >>67741, это безусловно позитивная вещь.
>>67747
Деталей не хочу говорить, слишком деанон.
Пример 1: докладываю семинар @ вот модель, вот пара нетривиальных свойств модели, все формально доказано @ у дядечки вопрос "а вот если такой параметр то это контрпример" @ аlt-tab вбиваю параметр в конфиг, запускаю Coq @ за две секунды готово доказательство что все ок @ дядечка остался злой и недовольный.
Пример 2: есть несколько классов моделей, скажем A,B,C и у каждой параметр - натуральное число. Коллега взял модель B2, сказал, что она наиболее интересная из " соображений натуральности" и навыводил ее свойств, опубликовав статью с полотнами выкладок. Взялся делать то-же самое для С1. А тут я со своим Coq - вбиваешь класс модели и параметр - через секунду получаешь ту самую портянку со всеми доказательствами. Коллега со мной с тех пор не разговаривает.
Яж почем знаю...
> на что конкретно
Деталей не хочу говорить, слишком деанон.
Пример 1: докладываю семинар @ вот модель, вот пара нетривиальных свойств модели, все формально доказано @ у дядечки вопрос "а вот если такой параметр то это контрпример" @ аlt-tab вбиваю параметр в конфиг, запускаю Coq @ за две секунды готово доказательство что все ок @ дядечка остался злой и недовольный.
Пример 2: есть несколько классов моделей, скажем A,B,C и у каждой параметр - натуральное число. Коллега взял модель B2, сказал, что она наиболее интересная из " соображений натуральности" и навыводил ее свойств, опубликовав статью с полотнами выкладок. Взялся делать то-же самое для С1. А тут я со своим Coq - вбиваешь класс модели и параметр - через секунду получаешь ту самую портянку со всеми доказательствами. Коллега со мной с тех пор не разговаривает.
> почему злятся на тебя?
Яж почем знаю...
>>67752
Похоже, высокоинтеллектуальные круги - тот еще гадюшник. Слышал, что шахматисты тоже люто, бешено ненавидят друг друга.
Похоже, высокоинтеллектуальные круги - тот еще гадюшник. Слышал, что шахматисты тоже люто, бешено ненавидят друг друга.
>>67752
Ради любопытства, в чем бонус Coq в такого рода деятельности? Казалось бы для обсчета моделей куда проще было бы использовать систему символических вычислений. Понятно, что так не получишь формального доказательства; но обычно в физике никто и не ставит таких критериев строгости. При этом получение именно формального доказательства вещь явно не бесплатная и требует кучи дополнительных усилий.
Ради любопытства, в чем бонус Coq в такого рода деятельности? Казалось бы для обсчета моделей куда проще было бы использовать систему символических вычислений. Понятно, что так не получишь формального доказательства; но обычно в физике никто и не ставит таких критериев строгости. При этом получение именно формального доказательства вещь явно не бесплатная и требует кучи дополнительных усилий.
>>67754
Опять детали не скажу. Это специфика данной области теорфизики - тут Coq очень хорошо подходит.
>Ради любопытства, в чем бонус Coq в такого рода деятельности?
Опять детали не скажу. Это специфика данной области теорфизики - тут Coq очень хорошо подходит.
540 Кб, 680x621Я правильно понимаю, что хейт в сторону кока и всего такого основан на суеверии, что на бумаге ручкой можно сделать больше, чем в коке, и типа как ручка с бумагой это высокий штиль, а кок - презренный бездушный быдлокодинг?
>>67762
Да
Да
>>67762
Нет. Хейта к коку нет, есть хейт к его слепым последователям, которые утверждают, что маняматика нинужна и автоматизированные пруверы - будущее. У таких вот "экспертов" просто не хватает образования, чтобы понять, о чём вообще современная математика, но они её уже "решили".
Нет. Хейта к коку нет, есть хейт к его слепым последователям, которые утверждают, что маняматика нинужна и автоматизированные пруверы - будущее. У таких вот "экспертов" просто не хватает образования, чтобы понять, о чём вообще современная математика, но они её уже "решили".
>>67778
Это практическое виденье.
Я о тех кому и образование достает и денег не особо требуется. Что с ними не так?
Это практическое виденье.
Я о тех кому и образование достает и денег не особо требуется. Что с ними не так?
>>67780
А что у тебя есть волшебного математического в голове, чего нет в математической нотации на бумаге? Особая уличная магия?
> Не на бумаге, а в голове.
А что у тебя есть волшебного математического в голове, чего нет в математической нотации на бумаге? Особая уличная магия?
>>67779
Тут как с историей антисептиков в медицине. Врач Земмельвейс показал, что если мыть руки с хлоркой перед операцией, а не после, то внезапно смертность послеоперационных больных от сепсиса падает с 60% до 1-2. И что, его признали спасителем? Хуй там. Затравили, заруинили карьеру, позже вообще в дурку упекли. Потому что для абсолютного большинства светил медицины признать себя дебилом, не могущим в банальное мытье рук, хуже всего. Так и тут. ЧСВ важнее практических результатов, даже если речь о жизнях людей, про математику и говорить нечего. Кто сознательно откажется от высокопарных кукареканий о первой культуре и о чем-то волшебном в голове, чего нет в бездуховном коке? Да никто, это равносильно признанию себя дебилом.
> Я о тех кому и образование достает и денег не особо требуется. Что с ними не так?
Тут как с историей антисептиков в медицине. Врач Земмельвейс показал, что если мыть руки с хлоркой перед операцией, а не после, то внезапно смертность послеоперационных больных от сепсиса падает с 60% до 1-2. И что, его признали спасителем? Хуй там. Затравили, заруинили карьеру, позже вообще в дурку упекли. Потому что для абсолютного большинства светил медицины признать себя дебилом, не могущим в банальное мытье рук, хуже всего. Так и тут. ЧСВ важнее практических результатов, даже если речь о жизнях людей, про математику и говорить нечего. Кто сознательно откажется от высокопарных кукареканий о первой культуре и о чем-то волшебном в голове, чего нет в бездуховном коке? Да никто, это равносильно признанию себя дебилом.
>>67793
Есть такая гипотеза, что чтобы что-то доказать, убедить другого математика(и себя тоже) в некоторой теореме, не нужно делать все выкладки. Если её принимать как истину, тогда "верификация -- это дополнительная работа". Но тогда получается, что один раз её сделал автор и её сделал каждый читатель. Зачем перекладывать? Верифицировать -- просто, приятно и кучу ошибок и интересных нюансов можно найти. Ответ прост: ещё нет устоявшихся стандартов верификации: всяким нормальным кокам и хорошим аналогам обычно около 30 лет разработки. И они синтаксис меняют.
Есть такая гипотеза, что чтобы что-то доказать, убедить другого математика(и себя тоже) в некоторой теореме, не нужно делать все выкладки. Если её принимать как истину, тогда "верификация -- это дополнительная работа". Но тогда получается, что один раз её сделал автор и её сделал каждый читатель. Зачем перекладывать? Верифицировать -- просто, приятно и кучу ошибок и интересных нюансов можно найти. Ответ прост: ещё нет устоявшихся стандартов верификации: всяким нормальным кокам и хорошим аналогам обычно около 30 лет разработки. И они синтаксис меняют.
>>67659 (OP)
недавно какой то пидорас рассказал про неё. Он хоть и пидорас, но вдруг что то полезное говорит. А что, в чём проблема этой homotopy type theory?
недавно какой то пидорас рассказал про неё. Он хоть и пидорас, но вдруг что то полезное говорит. А что, в чём проблема этой homotopy type theory?
>>67844
Но есть ли у тебя хоть какие-нибудь истории успеха в математике, когда во время попытки формализации поймали существенную ошибку? Т.е. не просто какую-нибудь техническую лемму, которая была сформулирована в излишней общности, когда она уже не верна, но общий ход доказательства от этого не страдает. А вот, чтобы было что-то не так с какой-то важной теоремой, которой действительно пользовались другие математики.
Если нет, то все о чем ты говоришь - это чисто спекулятивная польза. Но при этом ты предлагешь вкладывать в это очень реальные усилия.
Я слышал о примере, когда нашли уязвимость в каком-то протоколе во время его верификации. Так что наверное в компьютерной безопасности формальная верификации вещь в самом деле полезная.
Это неадекватный взгляд на то, как и почему читают математические статьи. Собственно верификацией читатели занимаются не так часто; обычно или если читатель это ответственный рецензент или если заявлен интересный результат, но есть подозрения в наличие ошибки (кстати и в таком случае искать ошибки тотально построчной проверкой - это контр-продуктивно, куда лучше искать в статье подозрительные утверждения и таким образом локализовать свое внимание на фрагментах где есть серьезные основания ожидать ошибку). Иначе цель состоит в том, чтобы понять, в чем состоят результаты и извлечь идеи доказательств/конструкций. И для последнего формализация никак не поможет. Скорее наоборот, если кто-то только произведет верификацию в Коке, но не напишет нормальную статью, то разобраться в доказательстве станет труднее.
Но есть ли у тебя хоть какие-нибудь истории успеха в математике, когда во время попытки формализации поймали существенную ошибку? Т.е. не просто какую-нибудь техническую лемму, которая была сформулирована в излишней общности, когда она уже не верна, но общий ход доказательства от этого не страдает. А вот, чтобы было что-то не так с какой-то важной теоремой, которой действительно пользовались другие математики.
Если нет, то все о чем ты говоришь - это чисто спекулятивная польза. Но при этом ты предлагешь вкладывать в это очень реальные усилия.
Я слышал о примере, когда нашли уязвимость в каком-то протоколе во время его верификации. Так что наверное в компьютерной безопасности формальная верификации вещь в самом деле полезная.
>Но тогда получается, что один раз её сделал автор и её сделал каждый читатель
Это неадекватный взгляд на то, как и почему читают математические статьи. Собственно верификацией читатели занимаются не так часто; обычно или если читатель это ответственный рецензент или если заявлен интересный результат, но есть подозрения в наличие ошибки (кстати и в таком случае искать ошибки тотально построчной проверкой - это контр-продуктивно, куда лучше искать в статье подозрительные утверждения и таким образом локализовать свое внимание на фрагментах где есть серьезные основания ожидать ошибку). Иначе цель состоит в том, чтобы понять, в чем состоят результаты и извлечь идеи доказательств/конструкций. И для последнего формализация никак не поможет. Скорее наоборот, если кто-то только произведет верификацию в Коке, но не напишет нормальную статью, то разобраться в доказательстве станет труднее.
>>67853
Для этого надо знать математику, лол
>Но есть ли у тебя хоть какие-нибудь истории успеха в математике
Для этого надо знать математику, лол
>>67853
Есть. Заповедью исключенного третьего и актуальной бесконечности пользовались веками, пока Брауэр не показал, что это просто когнитивные искажения, и основывать на них точные знания - ошибка.
> Но есть ли у тебя хоть какие-нибудь истории успеха в математике, когда во время попытки формализации поймали существенную ошибку?
Есть. Заповедью исключенного третьего и актуальной бесконечности пользовались веками, пока Брауэр не показал, что это просто когнитивные искажения, и основывать на них точные знания - ошибка.
103 Кб, 240x168>>67871
А прогреры уже запрогали ГоТТ так, чтобы он в Браузере работал? Или надо себе приложение на комп качать?
А прогреры уже запрогали ГоТТ так, чтобы он в Браузере работал? Или надо себе приложение на комп качать?
Заметил интересный паттерн - все (трое), кто с моей кафедры впоследствие заинтересовались HoTT и пруверами, на первом курсе пытались записывать лекции через латех и ебню вроде vim на своём нетбуке-хуюке. Так что эта болезнь выявляется на ранней стадии.
>>67879
Хз. Нашел в гугл-пикчах.
Хз. Нашел в гугл-пикчах.
>>67876
я тоже угораю по пруверам, и тоже в латехе сначала писал, лекции все конспектировал дотошно, хоттом переболел успешно(хуйня, не ведитесь, классическая математика в миллион раз круче)
я тоже угораю по пруверам, и тоже в латехе сначала писал, лекции все конспектировал дотошно, хоттом переболел успешно(хуйня, не ведитесь, классическая математика в миллион раз круче)
>>67853
Я истории успеха не искал и наверное их не так просто найти.
Сужу по себе: без формализации меня бы математике не научили бы никогда, потому что формат "прочёл книгу -- понял", или тем более "лектор сказал-- студент записал и вызубрил" не работает. Нет глубины необходимой.
А с верификацией оно проще будет. Сколько раз находил интересные тонкие, но важные подробности казалось бы уже известных мне теорем, без которых знание было бы искажено.
Я истории успеха не искал и наверное их не так просто найти.
Сужу по себе: без формализации меня бы математике не научили бы никогда, потому что формат "прочёл книгу -- понял", или тем более "лектор сказал-- студент записал и вызубрил" не работает. Нет глубины необходимой.
А с верификацией оно проще будет. Сколько раз находил интересные тонкие, но важные подробности казалось бы уже известных мне теорем, без которых знание было бы искажено.
>>67943
Какую-то хуйню говоришь. При чём тут твоё личное непонимание материала и, блядь, верификация? Высрал какой-то нонсеквитур (стромэн-детектор шизик триггеред). А кому-то мастурбация помогает понять материал, мы будем на основе этого делать выводы насчёт её роли в современной математике?
Ты просто не крутишься в математической среде, вот ты и не можешь понять каких-то простейших книжек. Пока ты там ебёшься со своими пруверами, обычный математик просто спросит на кафедре или, если тема сложная, инициирует семинарчик и там всё обсудят, статейки поковыряют.
Анекдотический пример, вобщем. Ну а мне в понимании книг помогает чтение других книг.
До кучи ещё и ложная эквивалентность - формализация и верификация. Как будто блядь до пруверов все математики на пальцах всё доказывали, а потом пришли матлогики и хачкеллоёбы и понеслась.
Какую-то хуйню говоришь. При чём тут твоё личное непонимание материала и, блядь, верификация? Высрал какой-то нонсеквитур (стромэн-детектор шизик триггеред). А кому-то мастурбация помогает понять материал, мы будем на основе этого делать выводы насчёт её роли в современной математике?
Ты просто не крутишься в математической среде, вот ты и не можешь понять каких-то простейших книжек. Пока ты там ебёшься со своими пруверами, обычный математик просто спросит на кафедре или, если тема сложная, инициирует семинарчик и там всё обсудят, статейки поковыряют.
Анекдотический пример, вобщем. Ну а мне в понимании книг помогает чтение других книг.
До кучи ещё и ложная эквивалентность - формализация и верификация. Как будто блядь до пруверов все математики на пальцах всё доказывали, а потом пришли матлогики и хачкеллоёбы и понеслась.
>>67947
Да не, он не троллит, он просто токсичный долбоёб, который ни одной теоремы не доказал, но имеет "очень ценное мнение".
Да не, он не троллит, он просто токсичный долбоёб, который ни одной теоремы не доказал, но имеет "очень ценное мнение".
>>67947
Нет, это правда. Математик без общения это не математик, а калека, фрик. Ни один успешный математик еще не жил без общения в среде.
Нет, это правда. Математик без общения это не математик, а калека, фрик. Ни один успешный математик еще не жил без общения в среде.
>>67953
Так вот почему во всех книгах по математике подача материала напоминает бред шизофреника.
Надо просто в той же среде крутиться, что и автор.
Так вот почему во всех книгах по математике подача материала напоминает бред шизофреника.
Надо просто в той же среде крутиться, что и автор.
>>67953
А ну так сразу видно почему вашему брату пруверы не нравятся. Так ты "успешный математик" крутящийся в элитарных кругах, который если что может "просто спросить на кафедре". А тут оказывается что можно git clone все доказательства, и ценность всех твоих социальные элитосвязей внезапно сильно уменьшилась.
А ну так сразу видно почему вашему брату пруверы не нравятся. Так ты "успешный математик" крутящийся в элитарных кругах, который если что может "просто спросить на кафедре". А тут оказывается что можно git clone все доказательства, и ценность всех твоих социальные элитосвязей внезапно сильно уменьшилась.
>>67710
Правильно ли я понимаю, что когда мы дотрагиваемся до стены, то молекулы нашего пальца начинают взаимодействовать с молекулами стены, обмениваясь на бешеной скорости кварками, и из за этого палец не пролазиет в стену?
Правильно ли я понимаю, что когда мы дотрагиваемся до стены, то молекулы нашего пальца начинают взаимодействовать с молекулами стены, обмениваясь на бешеной скорости кварками, и из за этого палец не пролазиет в стену?
>>67960
Слушай, ну всё, прямо уел меня, не спец я в К-теории, ну разве что могу когомологии де рама посчитать на многообразиях.
Если ты специалист, то зачем это нужно, какие проблемы решает? Может быть действительно стоит изучить
Слушай, ну всё, прямо уел меня, не спец я в К-теории, ну разве что могу когомологии де рама посчитать на многообразиях.
Если ты специалист, то зачем это нужно, какие проблемы решает? Может быть действительно стоит изучить
>>67957
Я эти маняфантазии уже сотый раз слышу, но вот на практике почему-то всё наоборот и в точности как говорит анон выше.
>тут оказывается что можно git clone все доказательства, и ценность всех твоих социальные элитосвязей внезапно сильно уменьшилась.
Я эти маняфантазии уже сотый раз слышу, но вот на практике почему-то всё наоборот и в точности как говорит анон выше.
>>67969
А ты типа идеалист и надеешься на успешность и адекватность присутствующих? Кто из нас в итого ебобо?:)
А ты типа идеалист и надеешься на успешность и адекватность присутствующих? Кто из нас в итого ебобо?:)
>>67969
Тем временем ты не говоришь какие проблемы решает твоя область математики. Кто её у тебя купит? (Даже чисто гипотетически)
На пруверах можно программы верифицировать, в том числе квантовые, а твоя теория ходжа и к теория ну куда её. Диффуры решать на многообразиях? А их кому продавать?
Тем временем ты не говоришь какие проблемы решает твоя область математики. Кто её у тебя купит? (Даже чисто гипотетически)
На пруверах можно программы верифицировать, в том числе квантовые, а твоя теория ходжа и к теория ну куда её. Диффуры решать на многообразиях? А их кому продавать?
>>67957
Доказательства везде написаны, интуицию за ними тебе никто просто так не даст. Вполне может быть, прочитал ты и не понял. Открой, например, доказательство Перельмана. Что будешь делать? Читать до посинения?
Доказательства везде написаны, интуицию за ними тебе никто просто так не даст. Вполне может быть, прочитал ты и не понял. Открой, например, доказательство Перельмана. Что будешь делать? Читать до посинения?
>>67969
А чего тогда вы вместе с "аноном выше" и ОПом кудахчете так на пруверы? Ну бегают там хипстеры-программисты-аутисты какие-то, в отличие от вас, элитарных, доступа к "спросить на кафедре" не имеют. Толку от этих ваших пруверов нет - тру математика только "на кафедре". Ну и хрен бы с ними?
>анон выше
А чего тогда вы вместе с "аноном выше" и ОПом кудахчете так на пруверы? Ну бегают там хипстеры-программисты-аутисты какие-то, в отличие от вас, элитарных, доступа к "спросить на кафедре" не имеют. Толку от этих ваших пруверов нет - тру математика только "на кафедре". Ну и хрен бы с ними?
>>67781
На бумаге вообще ничего нет.
По определению понимания (какому бы то ни было, несуществующему), понимание --- это то, что происходит у тебя в голове.
Человек --- мера всех вещей.
И именно это понимание и является первичным объектом, а определения теоремы доказательства --- вторичным, производным.
На верификацию вообще всем насрать, кроме фриков. Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
На бумаге вообще ничего нет.
По определению понимания (какому бы то ни было, несуществующему), понимание --- это то, что происходит у тебя в голове.
Человек --- мера всех вещей.
И именно это понимание и является первичным объектом, а определения теоремы доказательства --- вторичным, производным.
На верификацию вообще всем насрать, кроме фриков. Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
62 Кб, 555x400>>67986
Охуеть, откровения какие. Ещё несколько лет, глядишь и до интуиционизма додумаешься. А вот суть формализма как раз в том, что все нужное - на бумаге, и зависит только от непротиворечивости используемой аксиоматики. От головы в данном случае зависит только выбор аксиоматики, какой набор заповедей больше зайдет - ZFC там, NBG итд. Гедель, правда, доказал что это для оснований не подходит, да и ладно, хуй с ним.
> На бумаге вообще ничего нет.
> По определению понимания (какому бы то ни было, несуществующему), понимание --- это то, что происходит у тебя в голове.
> Человек --- мера всех вещей.
> И именно это понимание и является первичным объектом, а определения теоремы доказательства --- вторичным, производным.
Охуеть, откровения какие. Ещё несколько лет, глядишь и до интуиционизма додумаешься. А вот суть формализма как раз в том, что все нужное - на бумаге, и зависит только от непротиворечивости используемой аксиоматики. От головы в данном случае зависит только выбор аксиоматики, какой набор заповедей больше зайдет - ZFC там, NBG итд. Гедель, правда, доказал что это для оснований не подходит, да и ладно, хуй с ним.
>>67986
Ну да, во всякой прикладухе так и есть. Сантехнику не нужна физика, гамалогии можно трясти без оснований.
> На верификацию вообще всем насрать, кроме фриков. Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
Ну да, во всякой прикладухе так и есть. Сантехнику не нужна физика, гамалогии можно трясти без оснований.
>>67989
Да, вот на этой процитированной фразе, а также на вопросе "чьи проблемы твоя область решает, кроме твоих", тот анон явно сливается.
Да, вот на этой процитированной фразе, а также на вопросе "чьи проблемы твоя область решает, кроме твоих", тот анон явно сливается.
>>67987
Вот именно, ты прав. Надо больше писать всяких доказательств, брошюр, книжек, чтобы это было доступно большему количеству людей, в разных форматах, а не только "от человеку к человеку".
Вот именно, ты прав. Надо больше писать всяких доказательств, брошюр, книжек, чтобы это было доступно большему количеству людей, в разных форматах, а не только "от человеку к человеку".
>>67986
Ну что это такое?
> Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
Ну что это такое?
>>67989
ну ты прав, основания имеют такое же отношения к математике, как обсуждение интерпретаций квантовой механики к починке сан. узла, никакое то есть
ну ты прав, основания имеют такое же отношения к математике, как обсуждение интерпретаций квантовой механики к починке сан. узла, никакое то есть
>>68106
он имел в виду, проверять, верен ли доказанный кем-то результат, который проверен "авторитетами", с существующим консенсусом...
Сомнительное утверждение, так как твоё понимание может отличаться от объективной реальности. Игра в рулетку тут. Верификация позволяет нивелировать подобные неточности. (у многих серьёзных результатов есть набор неэквивалентных формулировок)
он имел в виду, проверять, верен ли доказанный кем-то результат, который проверен "авторитетами", с существующим консенсусом...
Сомнительное утверждение, так как твоё понимание может отличаться от объективной реальности. Игра в рулетку тут. Верификация позволяет нивелировать подобные неточности. (у многих серьёзных результатов есть набор неэквивалентных формулировок)
>>68111
лол
лол
>>68111
Нет, я имел в виду, что "факт" истинности или ложности того или иного математического утверждения сам по себе не имеет ни ценности, ни смысла. Допустим, гипотеза Римана верна или не верна --- какая разница? Тебе лично не плевать?
Любое утверждение можно принять в качестве аксиомы, т.е. сделать его верным или неверным по своему желанию.
Слишком большой фокус на "да/нет" аспектах --- это аберрация , являющаяся следствием принятой сейчас системы преподавания, а не какой-то глубокий факт.
Противопоставляя компьютерную верификацию "работе по старинке", многие подменяют первичную ценность вторичной.
Хотя, если считать компьютер продолжением мозга, то всё нормально. Но это получается киборг, а не человек.
>>68058
Я не он, если что.
Нет, я имел в виду, что "факт" истинности или ложности того или иного математического утверждения сам по себе не имеет ни ценности, ни смысла. Допустим, гипотеза Римана верна или не верна --- какая разница? Тебе лично не плевать?
Любое утверждение можно принять в качестве аксиомы, т.е. сделать его верным или неверным по своему желанию.
Слишком большой фокус на "да/нет" аспектах --- это аберрация , являющаяся следствием принятой сейчас системы преподавания, а не какой-то глубокий факт.
Противопоставляя компьютерную верификацию "работе по старинке", многие подменяют первичную ценность вторичной.
Хотя, если считать компьютер продолжением мозга, то всё нормально. Но это получается киборг, а не человек.
>>68058
Я не он, если что.
89 Кб, 512x512>>68113
Математике это по своей сути точное знание. На голландском буквально - wiskunde. Факт истинности или ложности утверждения это сама суть математики, вне которого ее просто нет. Отсюда и проблема оснований - что именно считать истинностью в математике.
То что ты описываешь - уровень пикрелейтед.
> Нет, я имел в виду, что "факт" истинности или ложности того или иного математического утверждения сам по себе не имеет ни ценности, ни смысла.
Математике это по своей сути точное знание. На голландском буквально - wiskunde. Факт истинности или ложности утверждения это сама суть математики, вне которого ее просто нет. Отсюда и проблема оснований - что именно считать истинностью в математике.
> Допустим, гипотеза Римана верна или не верна --- какая разница? Тебе лично не плевать?
То что ты описываешь - уровень пикрелейтед.
>>68114
А на ацтекском - Tlapōhualmatiliztli.
Гипотеза Римана не интересна по той причине, что существуют десятки эквивалетных ей утверждений и все эти утверждения формулируются очень просто; утверждения же, которые вытекают из гипотезы Римана обычно очень сложные и содержат в формулировке пространства Харди и прочее.
Отсюда понятно, что гипотезу Римана следовало бы принять за аксиому (аксиомы это, среди прочего, простые утверждения имеющие многочисленные сложные следствия).
Ну а кроме того, гипотеза Римана уже доказана Делинем в 1974-м еще.
>На голландском буквально - wiskunde.
А на ацтекском - Tlapōhualmatiliztli.
Гипотеза Римана не интересна по той причине, что существуют десятки эквивалетных ей утверждений и все эти утверждения формулируются очень просто; утверждения же, которые вытекают из гипотезы Римана обычно очень сложные и содержат в формулировке пространства Харди и прочее.
Отсюда понятно, что гипотезу Римана следовало бы принять за аксиому (аксиомы это, среди прочего, простые утверждения имеющие многочисленные сложные следствия).
Ну а кроме того, гипотеза Римана уже доказана Делинем в 1974-м еще.
>>68118
Жаль что кроме тебя этого никто не знает.
Верую, ибо блаженен.
>Ну а кроме того, гипотеза Римана уже доказана Делинем в 1974-м еще.
Жаль что кроме тебя этого никто не знает.
>что гипотезу Римана следовало бы принять за аксиому
Верую, ибо блаженен.
>>68119
Я могу сказать про тебя то же самое, ты похоже веруешь в объективные истины из мира идей или откуда еще, и считаешь что математикам принципиально важно знать истинно ли данное утверждение в абсолютном смысле, или нет. Из разряда новостей в популярных журналах типа "ALL MATH MAY BE WRONG, Researcher said".
Но на самом деле это абсолютно не важно, важны утверждения, вытекающие из гипотезы Римана, и полученные с их помощью результаты, а не сама эта сраная гипотеза. И если вдруг окажется, что эта гипотеза не верна в общем смысле, ценности полученных результатов это никак не отменит. Тем более, что она уже верна в важнейших частных случаях, что уже доказано.
Люди, всерьез интересующиеся основаниями, это люди которые не понимают что такое вообще математика, где и зачем она нужна. Математика это не каталогизация объективных истин из мира идей и не искусство выводить произвольные следствия из этих истин.
Специалисты по основаниям это плутонисты, верующие в вычислимость и занимающиеся абстрактной хуйней не имеющей приложений. Когомологии, схемная алгебраическая геометрия, К-теория и т.д. имеют гигантское количество приложений, Делинь, Гротендик, Артин, Мамфорд и прочие действительно ближе к сантехникам, как тут выразились, чем к фуфлософам-пиздаболам с их объективными истинами, трансцендентальными единствами, тезисами Черта и проч.
>Верую, ибо блаженен.
Я могу сказать про тебя то же самое, ты похоже веруешь в объективные истины из мира идей или откуда еще, и считаешь что математикам принципиально важно знать истинно ли данное утверждение в абсолютном смысле, или нет. Из разряда новостей в популярных журналах типа "ALL MATH MAY BE WRONG, Researcher said".
Но на самом деле это абсолютно не важно, важны утверждения, вытекающие из гипотезы Римана, и полученные с их помощью результаты, а не сама эта сраная гипотеза. И если вдруг окажется, что эта гипотеза не верна в общем смысле, ценности полученных результатов это никак не отменит. Тем более, что она уже верна в важнейших частных случаях, что уже доказано.
Люди, всерьез интересующиеся основаниями, это люди которые не понимают что такое вообще математика, где и зачем она нужна. Математика это не каталогизация объективных истин из мира идей и не искусство выводить произвольные следствия из этих истин.
Специалисты по основаниям это плутонисты, верующие в вычислимость и занимающиеся абстрактной хуйней не имеющей приложений. Когомологии, схемная алгебраическая геометрия, К-теория и т.д. имеют гигантское количество приложений, Делинь, Гротендик, Артин, Мамфорд и прочие действительно ближе к сантехникам, как тут выразились, чем к фуфлософам-пиздаболам с их объективными истинами, трансцендентальными единствами, тезисами Черта и проч.
>>68121
Пынямаешь ли, все что ты перечислил, вовсе не висит где-то в пустоте. Это следствия развития математической мысли, следствия, к которым привели даже не столетия эволюции самых разных математических и не только идей, методов итд. И тот подход, который ты вычитал у Вербицкого, он в точности соответствует пикрелейтед номеру "тут играем, тут не играем, тут вообще рыбу заворачивали". И.е предлагается что-то сыграть не только в отрыве от всего контекста, но и принципиально игнорировать вопрос, откуда все это вообще пошло и в чем природа всего этого. В принципе, такой подход имеет право на существование, но с определенными оговорками, которые ваша секта принципиально не принимает. Практическая применимость чего-то как критерий истины это хорошо и правильно, но принимать это не как функциональный контекстуализм, а как нечто висящее в воздухе и данное нам непонятно кем и нахуя, это сектантство.
> Когомологии, схемная алгебраическая геометрия, К-теория и т.д. имеют гигантское количество приложений, Делинь, Гротендик, Артин, Мамфорд и прочие действительно ближе к сантехникам, как тут выразились, чем к фуфлософам-пиздаболам с их объективными истинами, трансцендентальными единствами, тезисами Черта и проч.
Пынямаешь ли, все что ты перечислил, вовсе не висит где-то в пустоте. Это следствия развития математической мысли, следствия, к которым привели даже не столетия эволюции самых разных математических и не только идей, методов итд. И тот подход, который ты вычитал у Вербицкого, он в точности соответствует пикрелейтед номеру "тут играем, тут не играем, тут вообще рыбу заворачивали". И.е предлагается что-то сыграть не только в отрыве от всего контекста, но и принципиально игнорировать вопрос, откуда все это вообще пошло и в чем природа всего этого. В принципе, такой подход имеет право на существование, но с определенными оговорками, которые ваша секта принципиально не принимает. Практическая применимость чего-то как критерий истины это хорошо и правильно, но принимать это не как функциональный контекстуализм, а как нечто висящее в воздухе и данное нам непонятно кем и нахуя, это сектантство.
672 Кб, 1403x988>>68114
Вообще-то это ниоткуда не следует.
Сами по себе понятия истинности и ложности могут оказаться не совсем тем, что надо ставить в основания.
Т.е. настоящие основания должны основываться на каких-то других концепциях (каких --- не знаю), а понятия "истинности" и "ложности" --- выводиться из них. Грубо говоря.
Наполовину прикалываюсь, наполовину серьёзен.
Возможно, если математик начнёт серьёзно рефлексировать, изучать свои мысли и побуждения, то что-то из этого он сможет извлечь.
>>68121
Громкое заявление.
А слова о фуфлософии и оскорбительные, и смешные. От любителя "схемной алгебраической геометрии", у которой приложений в жизни... сколько? Для любого нормального человека ты сам пиздабол.
>Факт истинности или ложности утверждения это сама суть математики, вне которого ее просто нет.
Вообще-то это ниоткуда не следует.
Сами по себе понятия истинности и ложности могут оказаться не совсем тем, что надо ставить в основания.
Т.е. настоящие основания должны основываться на каких-то других концепциях (каких --- не знаю), а понятия "истинности" и "ложности" --- выводиться из них. Грубо говоря.
>То что ты описываешь - уровень пикрелейтед.
Наполовину прикалываюсь, наполовину серьёзен.
Возможно, если математик начнёт серьёзно рефлексировать, изучать свои мысли и побуждения, то что-то из этого он сможет извлечь.
>>68121
>Люди, всерьез интересующиеся основаниями, это люди которые не понимают что такое вообще математика, где и зачем она нужна.
Громкое заявление.
А слова о фуфлософии и оскорбительные, и смешные. От любителя "схемной алгебраической геометрии", у которой приложений в жизни... сколько? Для любого нормального человека ты сам пиздабол.
>>68125
охуенно, прямо как у Гермиды и Якобса, синоним декартовой замкнутости
>функциональный контекстуализм
охуенно, прямо как у Гермиды и Якобса, синоним декартовой замкнутости
>>68125
Погоди-ка. Это что-же получается, "пыняпучк" юродидый с /math/ и "философсмолин" пиздобол с /sci/ - одна и та-же личность? Кто бы мог подумать?
> фуфлософам-пиздаболам
Погоди-ка. Это что-же получается, "пыняпучк" юродидый с /math/ и "философсмолин" пиздобол с /sci/ - одна и та-же личность? Кто бы мог подумать?
господа, вы правы лишь частично
1) не надо смешивать а) верификацию, как стремление к абсолютной строгости доказательств вместе с б) радикальным интуиционизмом/конструктивизмом. Поверифицировать можно отлично и классические доказательства.
2) я присоединяюсь к требованию обоснования изучения алгебраической геометрии, гиперкелеровых многообразий, пучков и прочего. Покажите покупателей! Пруф или не было!
1) не надо смешивать а) верификацию, как стремление к абсолютной строгости доказательств вместе с б) радикальным интуиционизмом/конструктивизмом. Поверифицировать можно отлично и классические доказательства.
2) я присоединяюсь к требованию обоснования изучения алгебраической геометрии, гиперкелеровых многообразий, пучков и прочего. Покажите покупателей! Пруф или не было!
>>68165
Пучки нужны даже палочкосчитателям и N-петухам для построение пресловутого функционального контекстуализма, у них там современная теория типов на предпучках строится и есть расширенная теории типов, где вместо категории множеств берутся категории групоидов, и таким образом переходят в престек теорию типов, где вместо сигмы конструкция Гротендика. Те еще наркоманы.
Я за модульного деда если что, но мне кажется, что вы тут попутали понятия верификации и нормализации. Вот скажем вы можете верифицировать свои группы сфер (если построите конечно, а то выше четвертой группы никто не построил еще даже для первых трех измерений), но нормализовать терм уже не сможете, нужно изобретать механизмы оптимальной редукции, новая открытая проблема). А так когомологии элиптические, циклические, хуические, этальные, халяльные — все это изи чекается уже пару лет как. Этальные кстати если записать в HoTT будут самыми красивыми.
Пучки нужны даже палочкосчитателям и N-петухам для построение пресловутого функционального контекстуализма, у них там современная теория типов на предпучках строится и есть расширенная теории типов, где вместо категории множеств берутся категории групоидов, и таким образом переходят в престек теорию типов, где вместо сигмы конструкция Гротендика. Те еще наркоманы.
Я за модульного деда если что, но мне кажется, что вы тут попутали понятия верификации и нормализации. Вот скажем вы можете верифицировать свои группы сфер (если построите конечно, а то выше четвертой группы никто не построил еще даже для первых трех измерений), но нормализовать терм уже не сможете, нужно изобретать механизмы оптимальной редукции, новая открытая проблема). А так когомологии элиптические, циклические, хуические, этальные, халяльные — все это изи чекается уже пару лет как. Этальные кстати если записать в HoTT будут самыми красивыми.
![quote-one-cannot-inquire-into-the-foundations-and-nature-of[...].jpg](https://2ch.life//math/src/67659/15881892167170.jpg)
71 Кб, 850x400>>68166
Зачем? Все это прекрасно строится без всяких пучков.
Все дело в том, что при желании это все работает в обеих направлениях. Гамалогии можно представить в HoTT, а можно и наоборот. Всяческие вербитодрочеры веруют только во швятые гамалогии, а все остальное в их религии даже не математика. Тогда как на самом деле все сложнее. И HoTT и гамалогии, и много чего другого - это просто языки, вторичные по отношению к собственно математическому мышлению. Потому что если это не принимать, тогда придется принять, что вся математика существует только на бумаге, а роль человека - трясти синтаксис. Либо остаётся совсем уж религия - платоновский мир идей, актуальная бесконечность, исключенное третье и прочие подобные догмы, заповеди. Можно скатиться ещё дальше, до высказываний Манина о том что "математика подвешена в воздухе". Но это уже уровень патриота, который сидя за американским компьютером с американским по, пишет в американском интернете, какие пиндосы пидоры.
> Пучки нужны даже палочкосчитателям и N-петухам для построение пресловутого функционального контекстуализма, у
Зачем? Все это прекрасно строится без всяких пучков.
> А так когомологии элиптические, циклические, хуические, этальные, халяльные — все это изи чекается уже пару лет как. Этальные кстати если записать в HoTT будут самыми красивыми.
Все дело в том, что при желании это все работает в обеих направлениях. Гамалогии можно представить в HoTT, а можно и наоборот. Всяческие вербитодрочеры веруют только во швятые гамалогии, а все остальное в их религии даже не математика. Тогда как на самом деле все сложнее. И HoTT и гамалогии, и много чего другого - это просто языки, вторичные по отношению к собственно математическому мышлению. Потому что если это не принимать, тогда придется принять, что вся математика существует только на бумаге, а роль человека - трясти синтаксис. Либо остаётся совсем уж религия - платоновский мир идей, актуальная бесконечность, исключенное третье и прочие подобные догмы, заповеди. Можно скатиться ещё дальше, до высказываний Манина о том что "математика подвешена в воздухе". Но это уже уровень патриота, который сидя за американским компьютером с американским по, пишет в американском интернете, какие пиндосы пидоры.
>>68168
Строится без пучков, но с пучками выглядит компактнее. Там много изоморфизомов моделей теории типов: Категории с семействами (CwF), категории с аттрибутами (CwA), Воеводский делал С-системы, потом поняли, что это все поебота, выдуманная людьми и перешли на гротендиковский пучкизм в французском стиле. Кубическая теория типов стала записываться одной формулой: I: <sup>op</sup> → Set. Пи и сигма тоже в пучках формулируется, как функториальная смена базы, вернулись к Лавировской классике.
>Зачем? Все это прекрасно строится без всяких пучков.
Строится без пучков, но с пучками выглядит компактнее. Там много изоморфизомов моделей теории типов: Категории с семействами (CwF), категории с аттрибутами (CwA), Воеводский делал С-системы, потом поняли, что это все поебота, выдуманная людьми и перешли на гротендиковский пучкизм в французском стиле. Кубическая теория типов стала записываться одной формулой: I: <sup>op</sup> → Set. Пи и сигма тоже в пучках формулируется, как функториальная смена базы, вернулись к Лавировской классике.
>>68170
Это хорошо, что пока только модульный дед атакует, а придут спросят как Стекс Проджект закодировать и что мы будем делать, мычать? Нет, мы готовы уже модальную престек теорию типов предоставить на конструкциях Гротендика --- такая основная мотивация пучкизма в теории типов, ублажить высших сантехников и более консистетно подойти к основаниям, чтобы они могли все в себя вобрать.
Это хорошо, что пока только модульный дед атакует, а придут спросят как Стекс Проджект закодировать и что мы будем делать, мычать? Нет, мы готовы уже модальную престек теорию типов предоставить на конструкциях Гротендика --- такая основная мотивация пучкизма в теории типов, ублажить высших сантехников и более консистетно подойти к основаниям, чтобы они могли все в себя вобрать.
>>68168
нихуя не работает. Пока что выходит лишь записать тривиальные результаты 50-60х, при этом 90% времени тратится на формализмы, вместо математики. Приход программистов в математику ничего хорошего не дал в итоге, вместо решения реальных задач бесконечные новые формализмы.
>Все дело в том, что при желании это все работает в обеих направлениях.
нихуя не работает. Пока что выходит лишь записать тривиальные результаты 50-60х, при этом 90% времени тратится на формализмы, вместо математики. Приход программистов в математику ничего хорошего не дал в итоге, вместо решения реальных задач бесконечные новые формализмы.
>>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
>От любителя "схемной алгебраической геометрии", у которой приложений в жизни... сколько?
ну тупые, не знали, что надо очередной модный фреймворк оснований учить
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
>>68176
в каком то смысле это хорошо, потому что тогда математика сводится к медалистам Филдса. Математики могут успокоится, задача программистов не забирать их медали, а провести рефакторинг всей математики, очень неблагодарная но интересная деятельность. Задача оснований --- строить эффективные вычислительные модели или предлагать новые специализированные синтаксисы для каждого вида математик.
в каком то смысле это хорошо, потому что тогда математика сводится к медалистам Филдса. Математики могут успокоится, задача программистов не забирать их медали, а провести рефакторинг всей математики, очень неблагодарная но интересная деятельность. Задача оснований --- строить эффективные вычислительные модели или предлагать новые специализированные синтаксисы для каждого вида математик.
>>68178
Нельзя провести "рефакторинг" не зная что ты собственно рефакторишь. А уровень знания математики у программистов нулевой.
> задача программистов не забирать их медали, а провести рефакторинг всей математики
Нельзя провести "рефакторинг" не зная что ты собственно рефакторишь. А уровень знания математики у программистов нулевой.
>>68179
Ну когда я говорю программисты я подразумеваю Воеводского. А ты очевидно подразумеваешь своего студента имбецила, который сайт кампуса на ПХП пишет.
Ну когда я говорю программисты я подразумеваю Воеводского. А ты очевидно подразумеваешь своего студента имбецила, который сайт кампуса на ПХП пишет.
>>68180
Речь скорее о ncatlab, о любителях пруверов и функционального программирования. Воеводский был жемчужиной среди всего этого сброда, с реальными математическими результатами в прошлом.
> А ты очевидно подразумеваешь своего студента имбецила, который сайт кампуса на ПХП пишет.
Речь скорее о ncatlab, о любителях пруверов и функционального программирования. Воеводский был жемчужиной среди всего этого сброда, с реальными математическими результатами в прошлом.
>>68177
Тебя спросили про приложение алгебраической геометрии в жизни, а ты приводишь статью на википедию, где перечислено программное обеспечение, интересно. Не хочешь задуматься, почему медалист Филдса пересел за комп?
> приложений в жизни
> two-dimensional exactly solvable statistical lattice models and its related Hamiltonians
Тебя спросили про приложение алгебраической геометрии в жизни, а ты приводишь статью на википедию, где перечислено программное обеспечение, интересно. Не хочешь задуматься, почему медалист Филдса пересел за комп?
>>68181
ncatlab и ведется студентами, я сам плачу студентам за статьи на ncatlab, это студенческий образовательный проект. Ты воюешь с ветряными мельницами.
ncatlab и ведется студентами, я сам плачу студентам за статьи на ncatlab, это студенческий образовательный проект. Ты воюешь с ветряными мельницами.
>>68181
Воеводский был жемчужиной, а прувер написать не смог. Зато медаль получил, за пофиксаного Блоха-Като, рефакторер блядь. С-системы его ёбнутые. Ты реально переоцениваешь математиков.
Воеводский был жемчужиной, а прувер написать не смог. Зато медаль получил, за пофиксаного Блоха-Като, рефакторер блядь. С-системы его ёбнутые. Ты реально переоцениваешь математиков.
>>68182
Уайлс за комп не пересел, до сих пор на бумажке считает. Или ты про того, который стал с шумом радио общаться?
Уайлс за комп не пересел, до сих пор на бумажке считает. Или ты про того, который стал с шумом радио общаться?
>>68186
Нет, я ж не атакую, я ж признал, что нового не умеем производить, все что можем --- это по крупицам собирать то, что математики напридумывали используя их же методы, языки и модели. Вот и все. Да имбицильство, но оно качает, и тенуре нам не нада.
Нет, я ж не атакую, я ж признал, что нового не умеем производить, все что можем --- это по крупицам собирать то, что математики напридумывали используя их же методы, языки и модели. Вот и все. Да имбицильство, но оно качает, и тенуре нам не нада.
>>68179
Ага, а математика это согласно вашим сектантстким заповедям что?
> Нельзя провести "рефакторинг" не зная что ты собственно рефакторишь. А уровень знания математики у программистов нулевой.\t
Ага, а математика это согласно вашим сектантстким заповедям что?
>>68188
Я не очень понимаю, на что постоянно погромисты обижаются. Ну вот Многие дисциплины просачиваются в другие области будь то humanities или естественнонаучные или инженерные, это нормально. Но глупо полагать, что в 21м веке ты можешь достичь хорошего понимания современных достижений в нескольких дисциплинах.
SVD, численное решение урчп, градиентные спуски, 3Д моделирование и кватернионы, Монте-Карло, FFT, поиск группы автоморфизмов для решения какой-нибудь хитровыебанной задачи из линейной оптимизации - это не современная математика. Это всё важные вещи, они могут часто использоваться, они полезны. Но с точки зрения математики этим идеям лет 200 минимум.
Весьма вероятно, что большинство программистов выше перечисленные вещи имплементировать не сможет и прекрасно обходится куда более простыми математическими операциями. И это нормально. Ну какой-нибудь 0.00001% прикладных математиков перекочует в топологический дата саенс, это делает их программистами?
Это не какая-то профессиональная спесь. Просто в "простонародье" математикой и матаном называют всё, что сложнее обычного умножения. Если же мы говорим про пруверы и соответсвенно теоремы, то есть совершенно чёткая область чистой математики. Порог вхождения в современную актуальную чистую математику настолько высокий, что 99.9999% программистам дорога туда заказана.
Поэтому все громкие утверждения насчёт важности пруверов серьёзно просто не воспринимаются из-за совершенной некомпетентности собеседников. Это уровень ферматистов и навьестоксеров.
>Ага, а математика это согласно вашим сектантстким заповедям что?
Я не очень понимаю, на что постоянно погромисты обижаются. Ну вот Многие дисциплины просачиваются в другие области будь то humanities или естественнонаучные или инженерные, это нормально. Но глупо полагать, что в 21м веке ты можешь достичь хорошего понимания современных достижений в нескольких дисциплинах.
SVD, численное решение урчп, градиентные спуски, 3Д моделирование и кватернионы, Монте-Карло, FFT, поиск группы автоморфизмов для решения какой-нибудь хитровыебанной задачи из линейной оптимизации - это не современная математика. Это всё важные вещи, они могут часто использоваться, они полезны. Но с точки зрения математики этим идеям лет 200 минимум.
Весьма вероятно, что большинство программистов выше перечисленные вещи имплементировать не сможет и прекрасно обходится куда более простыми математическими операциями. И это нормально. Ну какой-нибудь 0.00001% прикладных математиков перекочует в топологический дата саенс, это делает их программистами?
Это не какая-то профессиональная спесь. Просто в "простонародье" математикой и матаном называют всё, что сложнее обычного умножения. Если же мы говорим про пруверы и соответсвенно теоремы, то есть совершенно чёткая область чистой математики. Порог вхождения в современную актуальную чистую математику настолько высокий, что 99.9999% программистам дорога туда заказана.
Поэтому все громкие утверждения насчёт важности пруверов серьёзно просто не воспринимаются из-за совершенной некомпетентности собеседников. Это уровень ферматистов и навьестоксеров.
>>68190
Которая точно так же, как и любая другая, представима в HoTT. Ничего волшебного в чистых гамалогиях нет. Но, с точки зрения сектанта, писать гамалогии в прувере, а не на бумаге - это пиздец харам и неко мпетентность. Почему? Да вот потомучто.
> есть совершенно чёткая область чистой математики.
Которая точно так же, как и любая другая, представима в HoTT. Ничего волшебного в чистых гамалогиях нет. Но, с точки зрения сектанта, писать гамалогии в прувере, а не на бумаге - это пиздец харам и неко мпетентность. Почему? Да вот потомучто.
>>68187
золотые слова
единственное что дополню -- может быть верификация -- это способ изучения математики для тех, кому не повезло оказаться в нужной среде в нужное время? Это я типа про себя...
Да и к тому же -- это благородное дело, если кто-то что-то хорошо верифицировал -- изучить другому человеку это очень просто.
Да, С-системы Воеводского нужны были для модели его теории типов. Но она вроде сильно специализированная какая-то, конструктивая в каком-то смысле. А это значит, что классическую математику в ней не подоказываешь. (Ну может есть какой-то хитрый способ?) Ае сли не подаказываешь, то тогда разве это "основания математики"? Получается, что нет. Или что с точки зрения адептов hott, настоящей(тм) алгебре "не нужна" аксиома выбора? Все учебники переписывать? На конечных объектах -- может быть, ну а если чуть сложнее что...
золотые слова
единственное что дополню -- может быть верификация -- это способ изучения математики для тех, кому не повезло оказаться в нужной среде в нужное время? Это я типа про себя...
Да и к тому же -- это благородное дело, если кто-то что-то хорошо верифицировал -- изучить другому человеку это очень просто.
Да, С-системы Воеводского нужны были для модели его теории типов. Но она вроде сильно специализированная какая-то, конструктивая в каком-то смысле. А это значит, что классическую математику в ней не подоказываешь. (Ну может есть какой-то хитрый способ?) Ае сли не подаказываешь, то тогда разве это "основания математики"? Получается, что нет. Или что с точки зрения адептов hott, настоящей(тм) алгебре "не нужна" аксиома выбора? Все учебники переписывать? На конечных объектах -- может быть, ну а если чуть сложнее что...
>>68190
А что такое современная математика, и можно ли ее где-нибудь применить? Или она такая ЧИСТАЯ, что нигде не применяется?
А что такое современная математика, и можно ли ее где-нибудь применить? Или она такая ЧИСТАЯ, что нигде не применяется?
>>68193
Способ ровно тот же самый, что и в классической математике - без задней мысли берешь и прописываешь нужную заповедь. И о чудо, можно её использовать для "доказательства".
> классическую математику в ней не подоказываешь. (Ну может есть какой-то хитрый способ?
Способ ровно тот же самый, что и в классической математике - без задней мысли берешь и прописываешь нужную заповедь. И о чудо, можно её использовать для "доказательства".
>>68193
С-системы точно такая же копипаста как и CwF, CwA, только Воеводсткий использовал категории, объекты которых индексированые натуральными числами. В те времена еще не было модальной HoTT поэтому теории связанных топосов Ловира еще не было в пруверах, поэтому ясно что что в С-системах этальная математика не чекается. C-системы это изоморфизм universe categories.
>Да, С-системы Воеводского нужны были для модели его теории типов. Но она вроде сильно специализированная какая-то, конструктивая в каком-то смысле.
С-системы точно такая же копипаста как и CwF, CwA, только Воеводсткий использовал категории, объекты которых индексированые натуральными числами. В те времена еще не было модальной HoTT поэтому теории связанных топосов Ловира еще не было в пруверах, поэтому ясно что что в С-системах этальная математика не чекается. C-системы это изоморфизм universe categories.
>>68198
Нет никакой его теории типов. Есть теория типов и в рамках ее DIY модели, все равноправные. Кто больше математики в своих моделях закодирует тот и победил, это и будет показателем эффективности испольования прувера.
Нет никакой его теории типов. Есть теория типов и в рамках ее DIY модели, все равноправные. Кто больше математики в своих моделях закодирует тот и победил, это и будет показателем эффективности испольования прувера.
>>68199
С-системы как и все основание построенное Воеводским просто зажигало ребят вокруг за это ему спасибо, а так же теорию типов для своей же унивалентности Воеводский построить не смог. Построили программисты, так что спесь не то что с модульного деда, но и с лауреатов Филдса можно сбить при желании.
С-системы как и все основание построенное Воеводским просто зажигало ребят вокруг за это ему спасибо, а так же теорию типов для своей же унивалентности Воеводский построить не смог. Построили программисты, так что спесь не то что с модульного деда, но и с лауреатов Филдса можно сбить при желании.
159 Кб, 700x487>>68200
Мне меньше всего понятно, почему эти вещи вообще противопоставляются. Вот если отбросить сектантскую швятую веру уровня того, что креститься нужно не тремя, а двумя пальцами писать нужно на бумаге, а не в прувере, то какие аргументы остаются против HoTT?
> теорию типов для своей же унивалентности Воеводский построить не смог. Построили программисты, так что спесь не то что с модульного деда, но и с лауреатов Филдса можно сбить при желании.
Мне меньше всего понятно, почему эти вещи вообще противопоставляются. Вот если отбросить сектантскую швятую веру уровня того, что креститься нужно не тремя, а двумя пальцами писать нужно на бумаге, а не в прувере, то какие аргументы остаются против HoTT?
>>68197
насколько я помню, если прописать аксиому выбора -- получишь противоречие с аксиомой унивалентности.
насколько я помню, если прописать аксиому выбора -- получишь противоречие с аксиомой унивалентности.
>>68201
Аргумент против HoTT см выше, для неё надо передоказывать все теоремы и неизвестно, содержится ли в ней модель ZFC.
Аргумент против HoTT см выше, для неё надо передоказывать все теоремы и неизвестно, содержится ли в ней модель ZFC.
>>68201
Сейчас пруверы - бесполезное говно для 1,5 аутистов. Но если дать всей этой теме ход, то сразу появятся кабанчики, которые сверстают "нормальный прувер" и попросят бабки за его использование. Это подтолкнет журналы не принимать пруфы не заапрувленный пруверов от ООО Кабанчик Инт. Ну а дальше смерть и вырождение математики.
Сейчас пруверы - бесполезное говно для 1,5 аутистов. Но если дать всей этой теме ход, то сразу появятся кабанчики, которые сверстают "нормальный прувер" и попросят бабки за его использование. Это подтолкнет журналы не принимать пруфы не заапрувленный пруверов от ООО Кабанчик Инт. Ну а дальше смерть и вырождение математики.
>>68206
Это очень оптимистичная программа, но я бы под ней подписался!
Это очень оптимистичная программа, но я бы под ней подписался!
>>68208
Компьютиризация убивает искусство. И да компьютер есть и всегда будет беспросветно тупым.
>Вот честно, бред какой-то уровня "аргументов" керосиновых магнатов против елестрического освещения.
Компьютиризация убивает искусство. И да компьютер есть и всегда будет беспросветно тупым.
>>67752
Ахуительные истории.
Ахуительные истории.
>>68191
Кроме этого слова больше ничего про "современную" математику не знаешь? Идее гомологий уже больше ста лет, а Э-С аксиомам уже лет так 70. Гомологии проходят на первых курсах, если что.
Вот классический пример - не знаю, о чём говорю, но буду прятаться за мемами вроде пучков и гамалогий, авось проканает и это поднимет авторитетность моего программистского мнения. Ну с этим иди в /sci/.
>гамалогиях
Кроме этого слова больше ничего про "современную" математику не знаешь? Идее гомологий уже больше ста лет, а Э-С аксиомам уже лет так 70. Гомологии проходят на первых курсах, если что.
Вот классический пример - не знаю, о чём говорю, но буду прятаться за мемами вроде пучков и гамалогий, авось проканает и это поднимет авторитетность моего программистского мнения. Ну с этим иди в /sci/.
>>68212
Ты думаешь взяв "аргументы" в кавычки ты снизишь их значимость? Ну так, мой дорогой, в таком случае твои "аргументы" говно из жопы, как тебе такое?
Ты думаешь взяв "аргументы" в кавычки ты снизишь их значимость? Ну так, мой дорогой, в таком случае твои "аргументы" говно из жопы, как тебе такое?
>>68213
Значимость чего? Рандомных, ни на чём не основанных заявлений, что типа "буковы в прувере в отличие от таких же буков на бумаге - это не искусство"? Так у подобных заявлений и так никакой значимости нет, как я могу ее дальше снизить?
Значимость чего? Рандомных, ни на чём не основанных заявлений, что типа "буковы в прувере в отличие от таких же буков на бумаге - это не искусство"? Так у подобных заявлений и так никакой значимости нет, как я могу ее дальше снизить?
>>68208
Давай, если такой умный, строго докажи, что ZFC противоречива, верифицируй в любом прувере: гарантировано получишь премию Абеля.
Давай, если такой умный, строго докажи, что ZFC противоречива, верифицируй в любом прувере: гарантировано получишь премию Абеля.
>>68214
Просто иди нахуй.
Просто иди нахуй.
53 Кб, 624x433>>68215
Ну либо противоречива, либо нет. Ты ж не против использования исключенного третьего в доказательстве? Тогда я считай доказал.
Ну либо противоречива, либо нет. Ты ж не против использования исключенного третьего в доказательстве? Тогда я считай доказал.
>>68217
не смешно
не смешно
>>68217
А он вообще кто таков?
А он вообще кто таков?
>>68212
Хорошо, давай по существу. Раз ты у нас охуенно какой математик, то тебе ничего не стоит отвечать по существу, верно? Так что я ожидаю развёрнутых ответов с пруфцами, а не балабольство и демагогию. Это всё-таки /math/, а не /pr/.
Хорошо известно, что вокруг доказательства гипотезы Пуанкаре было немало драмы из-за сказанного/напечатанного Яу, Цао, и Джу. В частности, они намекали, что доказательство Перельмана не полное. Позже это утверждали и другие (статья Моргана-Тяня, книга Бахри).
1) Могут ли пруверы (существующие на сегодняшний день) показать (однозначно), были ли пробелы в доказательстве? Как/почему нет?
2) В первой архивной статье Перельмана на эту тему он получает неравенства типа Гарнака, интегрируя неравенство Ли-Яу, и в получившихся геометриях (точнее, в одной оптимальной) считает геодезические.
Вопрос - могут ли пруверы показать, какие из этих результатов (в частности, аналог теоремы Бишопа-Громова) уже автоматически следовали из статьи Ли-Яу? Как/почему нет?
2) Могут ли пруверы показать, есть ли пробелы во второй архивной статье Перельмана, а именно в исследовании поведения решений для времени много большего времени "хирургии"? Как/почему нет?
3) Могут ли пруверы показать, корректно ли доказательство конечности времени вымирания (вторая статья)? Как/почему нет?
4) Могут ли пруверы выявить неэквивалентные утверждения между статьями Перельмана и Цао-Джу (особенно раздел 7.6 последней, включая результат о поведении потоков Риччи с хирургией на бесконечности)? Как/почему нет?
Жду демагогию, односложные ответы, мемы, шутейки, и увиливания.
>Ты ж сам видишь, что по существу того поста не возразил
Хорошо, давай по существу. Раз ты у нас охуенно какой математик, то тебе ничего не стоит отвечать по существу, верно? Так что я ожидаю развёрнутых ответов с пруфцами, а не балабольство и демагогию. Это всё-таки /math/, а не /pr/.
Хорошо известно, что вокруг доказательства гипотезы Пуанкаре было немало драмы из-за сказанного/напечатанного Яу, Цао, и Джу. В частности, они намекали, что доказательство Перельмана не полное. Позже это утверждали и другие (статья Моргана-Тяня, книга Бахри).
1) Могут ли пруверы (существующие на сегодняшний день) показать (однозначно), были ли пробелы в доказательстве? Как/почему нет?
2) В первой архивной статье Перельмана на эту тему он получает неравенства типа Гарнака, интегрируя неравенство Ли-Яу, и в получившихся геометриях (точнее, в одной оптимальной) считает геодезические.
Вопрос - могут ли пруверы показать, какие из этих результатов (в частности, аналог теоремы Бишопа-Громова) уже автоматически следовали из статьи Ли-Яу? Как/почему нет?
2) Могут ли пруверы показать, есть ли пробелы во второй архивной статье Перельмана, а именно в исследовании поведения решений для времени много большего времени "хирургии"? Как/почему нет?
3) Могут ли пруверы показать, корректно ли доказательство конечности времени вымирания (вторая статья)? Как/почему нет?
4) Могут ли пруверы выявить неэквивалентные утверждения между статьями Перельмана и Цао-Джу (особенно раздел 7.6 последней, включая результат о поведении потоков Риччи с хирургией на бесконечности)? Как/почему нет?
Жду демагогию, односложные ответы, мемы, шутейки, и увиливания.
>>68231
Может ли бумага доказывать теоремы?
Может ли бумага доказывать теоремы?
>>68231
О, чувствую шизоидное обострение у модульного деда!
О, чувствую шизоидное обострение у модульного деда!
>>68231
Нужно нейронку, которая могла бы челотекст переводить в нагромождение логической поебени и потом уже этот километр текста скармливать пруфчекеру.
Нужно нейронку, которая могла бы челотекст переводить в нагромождение логической поебени и потом уже этот километр текста скармливать пруфчекеру.
>>68220
Вольфрам знает математику еще меньше чем основатели, а теорию языков программирования вообще не знает.
Вольфрам знает математику еще меньше чем основатели, а теорию языков программирования вообще не знает.
>>68209
Ага, это сразу видно по бюджетам в области искусства и компьютерной графики.
Ага, это сразу видно по бюджетам в области искусства и компьютерной графики.
>>68231
я не он, но отвечу тебе, раз уж ты такую пасту напечатал.
Всё, что может быть доказано, может быть доказано как "на бумаге", так и на компьютере. Я сам и так, и так спокойно доказываю.
Все "драмы" -- чисто социальное явление, не относящееся к математике.
Мы говорим о пруверах, а имеем в виду "пруф ассистанты", они сами ничего сдожного не доказывают. Ты пишешь доказательство, а они проверяют, не ошибся ли ты.
Поэтому на вопрос "могут ли" ответ: да. Тебе придётся долго писать пруф, но в итоге , если твои интуитивнве рассуждения верны, то получится
я не он, но отвечу тебе, раз уж ты такую пасту напечатал.
Всё, что может быть доказано, может быть доказано как "на бумаге", так и на компьютере. Я сам и так, и так спокойно доказываю.
Все "драмы" -- чисто социальное явление, не относящееся к математике.
Мы говорим о пруверах, а имеем в виду "пруф ассистанты", они сами ничего сдожного не доказывают. Ты пишешь доказательство, а они проверяют, не ошибся ли ты.
Поэтому на вопрос "могут ли" ответ: да. Тебе придётся долго писать пруф, но в итоге , если твои интуитивнве рассуждения верны, то получится
>>68241
Да модульному деду уже преподали теорию типов на пучках и конструкциях Гротендика, если это не помогло, то остальное вряд ли поможет.
Да модульному деду уже преподали теорию типов на пучках и конструкциях Гротендика, если это не помогло, то остальное вряд ли поможет.
>>68242
Пусть подоказывают еще 100 лет на бумажке, а дальше будет без вариантов :-)
Пусть подоказывают еще 100 лет на бумажке, а дальше будет без вариантов :-)
>>68241
Тут есть одна эмпирическая гипотеза: доказательство любой достойной теоремы невозможно записать в прувере. Только тривиальные вещи 19 века и всякую комбинаторику. На данный момент за 40 и более лет компьютерных доказательств исключений не было.
>Ты пишешь доказательство, а они проверяют, не ошибся ли ты.
Тут есть одна эмпирическая гипотеза: доказательство любой достойной теоремы невозможно записать в прувере. Только тривиальные вещи 19 века и всякую комбинаторику. На данный момент за 40 и более лет компьютерных доказательств исключений не было.
>>68249
Через 100 лет приходи.
Через 100 лет приходи.
>>68248
Почему на бумаге можно?
> Тут есть одна эмпирическая гипотеза: доказательство любой достойной теоремы невозможно записать в прувере.
Почему на бумаге можно?
>>68251
потому, что интересно только модульному деду, а он видимо не филдсовский медалист.
потому, что интересно только модульному деду, а он видимо не филдсовский медалист.
>>68252
тут хуй пойми, что он имеет ввиду под математикой: создание вычислительных практичных теорий для народного хозяйства, доказательство больших теорем, нахождение изоморфизмов, рефакторинг математики, упрощение, педагогика, создание новых дисциплин, просто медальки выдаваемые тайным обществом непонятно. Понятно только, что на бумаге главное, чтоб было ОК АРНОЛЬД
тут хуй пойми, что он имеет ввиду под математикой: создание вычислительных практичных теорий для народного хозяйства, доказательство больших теорем, нахождение изоморфизмов, рефакторинг математики, упрощение, педагогика, создание новых дисциплин, просто медальки выдаваемые тайным обществом непонятно. Понятно только, что на бумаге главное, чтоб было ОК АРНОЛЬД
>>68253
Написать программу, которая сгенерирует статью по С-системам Воеводского в TeX из исходников и автоматически пошлет в журнал можно уже. А это, очевидно, настоящая математика, ее же чувак с медальками писал!
Написать программу, которая сгенерирует статью по С-системам Воеводского в TeX из исходников и автоматически пошлет в журнал можно уже. А это, очевидно, настоящая математика, ее же чувак с медальками писал!
>>68254
тоже не понимаю этого ad hominem, есть международная классификация математики, её и держитесь
тоже не понимаю этого ad hominem, есть международная классификация математики, её и держитесь
>>68251
Там многие формальности опускаются.
Там многие формальности опускаются.
>>68262
Всё doable, просто математикам быстро надоедает пруф-терм дописывать, да и программисты быстро бросают. Нужны репрессии.
Всё doable, просто математикам быстро надоедает пруф-терм дописывать, да и программисты быстро бросают. Нужны репрессии.
>>68263
Ну да выгнать всех программистов нахуй. А за упоминание cs major расстреливать из зенитки.
Ну да выгнать всех программистов нахуй. А за упоминание cs major расстреливать из зенитки.
>>68241
лол, как анон и предсказывал, он получил односложный ответ "да" без реальных пруфов и пояснений как и что
собственно, что и требовалось доказать, погромисты в реальной математике не шарят и по теме разговаривать не могут
>>68231
на этой доске всего 2.5 анона, которую даже второкурсный дифгем осилили, куда уж там потоки риччи
hottоёбы почитали определения категории и гомологии и теперь думают, что они "шарят"
не удивительно, что вербит перестал сюда заходить
лол, как анон и предсказывал, он получил односложный ответ "да" без реальных пруфов и пояснений как и что
собственно, что и требовалось доказать, погромисты в реальной математике не шарят и по теме разговаривать не могут
>>68231
на этой доске всего 2.5 анона, которую даже второкурсный дифгем осилили, куда уж там потоки риччи
hottоёбы почитали определения категории и гомологии и теперь думают, что они "шарят"
не удивительно, что вербит перестал сюда заходить
>>68275
Так это всё-таки он был, форсил тут свою единственно верную религию, лол. Нет в математике боженьки кроме вербита, а модульный дед (поел говна на обед) - пророк его.
Что вы за люди, пиздец...
> не удивительно, что вербит перестал сюда заходить
Так это всё-таки он был, форсил тут свою единственно верную религию, лол. Нет в математике боженьки кроме вербита, а модульный дед (поел говна на обед) - пророк его.
> лол, как анон и предсказывал, он получил односложный ответ "да"
> Вопросы, однозначно подразумевающие односложные ответы
> ответили односложно
> ррреее, я жи говорил
Что вы за люди, пиздец...
>>68276
Ну тогда это на уровне религии, так что пиздуйте со своими пруверами на другие доски.
>> Вопросы, однозначно подразумевающие односложные ответы
Ну тогда это на уровне религии, так что пиздуйте со своими пруверами на другие доски.
>>68278
Что на уровне религии, рабочие программы? Братишка, чёт ты с горя совсем хуйню понес.
> Ну тогда это на уровне религии
Что на уровне религии, рабочие программы? Братишка, чёт ты с горя совсем хуйню понес.
>>68276
Так а зачем тогда было говорить, что, мол, анон по существу не ответил? А как только поступили вопросы по существу - оказывается, что это секта и по существу-то никто и отвечать не может, потому что программисты ничего не знают ни о дифференциальной геометрии, ни о пруверах.
>> Вопросы, однозначно подразумевающие односложные ответы
>> ответили односложно
Так а зачем тогда было говорить, что, мол, анон по существу не ответил? А как только поступили вопросы по существу - оказывается, что это секта и по существу-то никто и отвечать не может, потому что программисты ничего не знают ни о дифференциальной геометрии, ни о пруверах.
>>68280
Вопросов по существу не поступало. На вопросы модульного деда (да поест он говна на обед) уже много лет есть однозначный ответ - да, ничего волшебного на бумаге нет, все то же самое можно делать в прувере. Он же с позиции своей швятой веры утверждает, что это не так. Зачем-то даже в очередной раз создал подобный тред.
> как только поступили вопросы по существу
Вопросов по существу не поступало. На вопросы модульного деда (да поест он говна на обед) уже много лет есть однозначный ответ - да, ничего волшебного на бумаге нет, все то же самое можно делать в прувере. Он же с позиции своей швятой веры утверждает, что это не так. Зачем-то даже в очередной раз создал подобный тред.
>>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
>можно делать в прувере
Так почему никто не делает? Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее. Представляю список теорем прошлого и позапрошлого века, которых никто не может набрать в прувере:
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
>>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
>можно делать в прувере
Так почему никто не делает? Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее. Представляю список теорем прошлого и позапрошлого века, которых никто не может набрать в прувере:
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
>>68287
Двачую, математика это прежде всего язык, все стремятся к ёмкости понятий, чтобы какую-нибудь сложную хуйню можно было выразить небольшим количеством символов, а тут всё наоборот.
>Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее.
Двачую, математика это прежде всего язык, все стремятся к ёмкости понятий, чтобы какую-нибудь сложную хуйню можно было выразить небольшим количеством символов, а тут всё наоборот.
>>68287
Справедливости ради, таки делают. Просто ты как обычно не в теме https://github.com/UniMath/UniMath например, ещё Воеводского проект, до сих пор развивается.
В той же агде юникод поддерживается, всю нотацию можно переопределить как самому удобно и угодно. Насчёт неосиляторов соглашусь, там мозги нужны. Про лемму Йонеды не смешил бы тапки, она в хаскелле-то давным-давно есть.
> Так почему никто не делает?
Справедливости ради, таки делают. Просто ты как обычно не в теме https://github.com/UniMath/UniMath например, ещё Воеводского проект, до сих пор развивается.
> Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее.
В той же агде юникод поддерживается, всю нотацию можно переопределить как самому удобно и угодно. Насчёт неосиляторов соглашусь, там мозги нужны. Про лемму Йонеды не смешил бы тапки, она в хаскелле-то давным-давно есть.
>>68290
Лол, ты про частный случай? Тащи пруф в нормальной математической формулировке.
опять ссылка на гитхаб с непойми чем и клеймо покойного Воеводского, будто он из рая дописывает. Присылай конкретные значимые теоремы из 20 века, тогда поговорим.
>Про лемму Йонеды не смешил бы тапки, она в хаскелле-то давным-давно есть.
Лол, ты про частный случай? Тащи пруф в нормальной математической формулировке.
>Справедливости ради, таки делают. Просто ты как обычно не в теме https://github.com/UniMath/UniMath
опять ссылка на гитхаб с непойми чем и клеймо покойного Воеводского, будто он из рая дописывает. Присылай конкретные значимые теоремы из 20 века, тогда поговорим.
>>68293
Ясно.
Значимые для кого? Вашей секты?
> гранаты формулировка у них не той системы
> ваш гитхаб не гитхаб, там буквы какие-то непонятные
Ясно.
> Присылай конкретные значимые теоремы из 20 века, тогда поговорим.
Значимые для кого? Вашей секты?
>>68294
Хуясно. Притащи для начала формулировку категории на хаскелле.
Для математических предметов за первый и второй курс. Теорема о нулях, теорема стокса, теорема коши из ткфп...
>Ясно.
Хуясно. Притащи для начала формулировку категории на хаскелле.
>Значимые для кого? Вашей секты?
Для математических предметов за первый и второй курс. Теорема о нулях, теорема стокса, теорема коши из ткфп...
Быстро прувер-шизики слились, когда им притащили математики. Как и казалось изначально, это просто погромисты с когнитивным диссонансом, которым кажется, что в хаскеле настоящие категории, а в пруверах - настоящие теоремы.
>>68293
можно статью или скрин тайной леммы Йонеды?
> лемму Йонеды
> пруф в нормальной математической формулировке.
можно статью или скрин тайной леммы Йонеды?
>>68298
Ну что ты, настоящее ламповое только на бумаге, ровно то же самое на винте - уже не то же самое.
> в пруверах - настоящие теоремы.
Ну что ты, настоящее ламповое только на бумаге, ровно то же самое на винте - уже не то же самое.
>>68300
Только есть нюанс, что ошибки на бумаге можно найти. Ошибки в пруверах ты будешь искать намного медленней.
Только есть нюанс, что ошибки на бумаге можно найти. Ошибки в пруверах ты будешь искать намного медленней.
>>68296
HoTT делалась для автоматизации теории гомотопий или алгебраической топологии, а не для алгебраической геометрии. Для непосредственного управления вараятис нужно ввести в ядро вместо гомотопического интервала [0,1], афинный отрезок А^1 и это уже будет называться А^1-теория гомотопий. Т.е. если ты скажем хочешь Блоха-Като доказать, то тебе сначала нужно перейти в правильную систему типов для этого.
HoTT делалась для автоматизации теории гомотопий или алгебраической топологии, а не для алгебраической геометрии. Для непосредственного управления вараятис нужно ввести в ядро вместо гомотопического интервала [0,1], афинный отрезок А^1 и это уже будет называться А^1-теория гомотопий. Т.е. если ты скажем хочешь Блоха-Като доказать, то тебе сначала нужно перейти в правильную систему типов для этого.
>>68303
Ну это любой студент на агде выкладывает на гитхабе. Тут же ничего не нужно кроме теорката и построенной категории множеств. То, что в Хаскеле просто стертый терм до System F, хаскель-доказательство в качестве школьной программы можно защитать. В этом смысле это же можно доказать даже в NuPRL и старых пруверах.
Ну это любой студент на агде выкладывает на гитхабе. Тут же ничего не нужно кроме теорката и построенной категории множеств. То, что в Хаскеле просто стертый терм до System F, хаскель-доказательство в качестве школьной программы можно защитать. В этом смысле это же можно доказать даже в NuPRL и старых пруверах.
>>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))
На 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))
>>68287
Вот тут какой-то студент на Агде написал 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
>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
>>68312
так мы видим этот тред
так мы видим этот тред
>>68316
особенно смешно то, что единственное полное доказательство этой теоремы существует только на компьютере :-)
особенно смешно то, что единственное полное доказательство этой теоремы существует только на компьютере :-)
>>68317
так и другие доказательства на компьютере, но не в прувере.
так и другие доказательства на компьютере, но не в прувере.
>>68323
конструктивная, она в CAS системах считалась
конструктивная, она в CAS системах считалась
946 Кб, 800x1200>>68162
У МЕНЯ ЗА ТАКИЕ ВОПРОСЫ В ХАРВАРДЕ УБИВАЮТ НАХУЙ ПУЧК ГРОТ СТАТЬИ ПИСАТЬ НАДО ПОВТОРЯЮ ПОВТОРЯЮ СТАТЬЯ ПО 87-тую ГРУППУ ТРЁХМЕРНОЙ СФЕРЫ НЕ ТОЖЕ САМОЕ ЧТО СТАТЬЯ ПОСВЯЩЕННАЯ ОДНОМУ КОНКРЕТНОМУ-НМУ ИНТРЕГАЛУ ПУУЧК ГРООТ ДИДИ ИЗ МГУ ПИШУТ ПРО ИНТЕГРАЛЫ СТАТЬИ И НЕ СТЫДНО КАК В НИГЕРИИ БУДЕМ ГРОООТ
>а напомните нам нахуя нам 87-я гомотопическая группа трехмерной сферы ?
У МЕНЯ ЗА ТАКИЕ ВОПРОСЫ В ХАРВАРДЕ УБИВАЮТ НАХУЙ ПУЧК ГРОТ СТАТЬИ ПИСАТЬ НАДО ПОВТОРЯЮ ПОВТОРЯЮ СТАТЬЯ ПО 87-тую ГРУППУ ТРЁХМЕРНОЙ СФЕРЫ НЕ ТОЖЕ САМОЕ ЧТО СТАТЬЯ ПОСВЯЩЕННАЯ ОДНОМУ КОНКРЕТНОМУ-НМУ ИНТРЕГАЛУ ПУУЧК ГРООТ ДИДИ ИЗ МГУ ПИШУТ ПРО ИНТЕГРАЛЫ СТАТЬИ И НЕ СТЫДНО КАК В НИГЕРИИ БУДЕМ ГРОООТ
>>68327
Лол блядь
Тут погромисты походу ни математики, ни программирования не знают
Тайпчекинг, кек
Весь тред это один большой COPE второкурсников с CS
Лол блядь
Тут погромисты походу ни математики, ни программирования не знают
Тайпчекинг, кек
Весь тред это один большой COPE второкурсников с CS
>>68328
Опять пук в лужу и швятая вера, что на бумаге можно сделать больше чем в прувере.
Опять пук в лужу и швятая вера, что на бумаге можно сделать больше чем в прувере.
>>68328
Это классическая проблема детей верующих в всезнающий всемогущий комплюктер. В силу того, что они в этой жизни еще нихуя не сделали, они не понимают, что такого не так в их вере.
Воеводский безусловно был первоклассным математиком, но своими унивалентыми основаниями он открыл дорогу всякому cs сброду дорогу туда, где ему быть никогда не следовало.
Это классическая проблема детей верующих в всезнающий всемогущий комплюктер. В силу того, что они в этой жизни еще нихуя не сделали, они не понимают, что такого не так в их вере.
Воеводский безусловно был первоклассным математиком, но своими унивалентыми основаниями он открыл дорогу всякому cs сброду дорогу туда, где ему быть никогда не следовало.
>>68298
Программистам не упало таким заниматься, на самом деле.
Программистам не упало таким заниматься, на самом деле.
>>68333
Ну вас шизиков напрямую спросили - покажите, как работает на примере любой из фундаментальных теорем 20го века, например теорема об индексе
Кто-то настрочил про гипотезу Пуанкаре, тоже тишина в ответ, неловкое "ну да, это можно..."
Пока что это выглядит как религия. Когда меня не аргументами убеждают, а просят поверить - интерес сразу пропадает. Может, поэтому в этой области нормальных математиков нет, и привлекает она одних только горе-питонистов.
>швятая вера
Ну вас шизиков напрямую спросили - покажите, как работает на примере любой из фундаментальных теорем 20го века, например теорема об индексе
Кто-то настрочил про гипотезу Пуанкаре, тоже тишина в ответ, неловкое "ну да, это можно..."
Пока что это выглядит как религия. Когда меня не аргументами убеждают, а просят поверить - интерес сразу пропадает. Может, поэтому в этой области нормальных математиков нет, и привлекает она одних только горе-питонистов.
>>68355
Кому ты нужен, в чем-то тебя убеждать? И где и кто тебя просит поверить? Сам на протяжении нескольких лет создаёшь эти треды, сам потом в них горишь. Зачем? Веруешь во швятую бумагу и бездушные кудахтеры - веруй, свободу вероисповедания не отменяли.
> Пока что это выглядит как религия. Когда меня не аргументами убеждают, а просят поверить - интерес сразу пропадает.
Кому ты нужен, в чем-то тебя убеждать? И где и кто тебя просит поверить? Сам на протяжении нескольких лет создаёшь эти треды, сам потом в них горишь. Зачем? Веруешь во швятую бумагу и бездушные кудахтеры - веруй, свободу вероисповедания не отменяли.
>>68356
А у кудахтеров появилиась душа?
А у кудахтеров появилиась душа?
>>68298
Тебе кажется, что в топовых пруверах не настоящие теоремы, просто потому что ты пока мало знаешь используемую в них математику. Я тоже раньше не знал и поэтому сомневался.
Тебе кажется, что в топовых пруверах не настоящие теоремы, просто потому что ты пока мало знаешь используемую в них математику. Я тоже раньше не знал и поэтому сомневался.
А зачем нужны пруверы? Ведь в док-вах сложных теорем есть какие-то куски, из которых потом развивают новую теорию. Если всё будут проверять компы то эти куски останутся незамеченными.
>>68360
Да тут нечему казаться - привели пример реальных, настоящих, теорем. Ответа по существу (как тут любит один) - не было. Я вот знаю математику, используемую в гипотезе Тёрстона или той же теореме Атьи-Зингера (не зря заканчивал, теперь могу щитпостить на двоще). Ну так и где они в пруверах? Или моего уровня недостаточно?
>Тебе кажется, что в топовых пруверах не настоящие теоремы
Да тут нечему казаться - привели пример реальных, настоящих, теорем. Ответа по существу (как тут любит один) - не было. Я вот знаю математику, используемую в гипотезе Тёрстона или той же теореме Атьи-Зингера (не зря заканчивал, теперь могу щитпостить на двоще). Ну так и где они в пруверах? Или моего уровня недостаточно?
>>68362
Я видел десятки академиков которые печатаются в АлгТопе но не могут на компьютере Пифагора записать и что? Там другая математика, и практика нужна.
Я видел десятки академиков которые печатаются в АлгТопе но не могут на компьютере Пифагора записать и что? Там другая математика, и практика нужна.
>>68347
Если программа написанная на сертифицированном прувере или языке, то любая программа в нём является валидным термом в топосе. Тотальное избавление от ошибок и переход в кванторы --- это и есть главная мотивация бездушевной математики.
Если программа написанная на сертифицированном прувере или языке, то любая программа в нём является валидным термом в топосе. Тотальное избавление от ошибок и переход в кванторы --- это и есть главная мотивация бездушевной математики.
>>68363
Прости, я еще хотел поинтересоваться, а Квиленновские Модельные Категории, Модельные Структуры и Гомотопические Категории --- это как, настоящая математика для модульного деда или нет?
Прости, я еще хотел поинтересоваться, а Квиленновские Модельные Категории, Модельные Структуры и Гомотопические Категории --- это как, настоящая математика для модульного деда или нет?
>>68296
Я думаю такие вещи в пруверах точно можно записать, просто он скорее всего не знает математики даже на таком уровне.
>Для математических предметов за первый и второй курс.
Я думаю такие вещи в пруверах точно можно записать, просто он скорее всего не знает математики даже на таком уровне.
>>68311
В голосину.
В голосину.
>>67751
Отвратитетельная на значит бесполезная, говно тоже чистить нужно, но неприятно, так и тут, они бы с большим удовольствием перекинули это на кого-нибудь другого.
Отвратитетельная на значит бесполезная, говно тоже чистить нужно, но неприятно, так и тут, они бы с большим удовольствием перекинули это на кого-нибудь другого.
>>67946
И найти решение тоже помогает.
>А кому-то мастурбация помогает понять материал, мы будем на основе этого делать выводы насчёт её роли в современной математике?
И найти решение тоже помогает.
>>68287
как минимум лемма Йонеды и теорема Гёделя верифицированы.
Это не модульный дед создал тред, это я, просто гораздо лучше было бы, если бы классические основания математики были такими вирусными. Верифицировать долго, но реально: и чем дальше, тем быстрее получается
как минимум лемма Йонеды и теорема Гёделя верифицированы.
Это не модульный дед создал тред, это я, просто гораздо лучше было бы, если бы классические основания математики были такими вирусными. Верифицировать долго, но реально: и чем дальше, тем быстрее получается
>>68310
там про неполноту речь, она верифицирована много где
полнота кстати попроще и тоже верифицирована в разных системах.
там про неполноту речь, она верифицирована много где
полнота кстати попроще и тоже верифицирована в разных системах.
>>68371
На всякий случай, я лично не люблю ни программировать, ни делать тяжеловесных выкладок (и, слава Аллаху, в той математике которой я занимаюсь можно обойтись без обоих). Но если сравнивать такие активности и речь идет о выкладках которые настолько механическая и трудоемкая ерунда, что их рационально автоматизировать, то запрограммировать эту автоматизацию явно привлекательнее.
На всякий случай, я лично не люблю ни программировать, ни делать тяжеловесных выкладок (и, слава Аллаху, в той математике которой я занимаюсь можно обойтись без обоих). Но если сравнивать такие активности и речь идет о выкладках которые настолько механическая и трудоемкая ерунда, что их рационально автоматизировать, то запрограммировать эту автоматизацию явно привлекательнее.
>>68385
напиши чуваку с сайта, чтобы обновил.
напиши чуваку с сайта, чтобы обновил.
>>68370
Пучкнув же.
Пучкнув же.
>>68749
Это Шольце?
Это Шольце?
2 Кб, 330x180Гомологии, гомотопии это же из топологии, так? А как это связано с основаниями математики и доказательствами вообще, объясните.
552 Кб, 435x650>>68886
Ну короче есть ГОТТ. Гомотопическая теория типов. А дальше на вики всё написано.
https://ru.wikipedia.org/wiki/Гомотопическая_теория_типов
Ну короче есть ГОТТ. Гомотопическая теория типов. А дальше на вики всё написано.
https://ru.wikipedia.org/wiki/Гомотопическая_теория_типов
>>68887
Перевод: сам я нихуя не понимаю, потому что ещё учусь (на погромиста), но звучит очень понтово.
Перевод: сам я нихуя не понимаю, потому что ещё учусь (на погромиста), но звучит очень понтово.
>>68889
Каким-каким, интуиционистским - Brouwer: "On the significance of the principle of excluded middle in mathematics, especially in function theory."
>А ну говори, каким Браузером пользуешься.
Каким-каким, интуиционистским - Brouwer: "On the significance of the principle of excluded middle in mathematics, especially in function theory."
>>68891
А в этом и смысл
А в этом и смысл
1) вначале всё свели к натуральным числам.
2) потом решили, что лучше брать за основу множества, так как натуральные числа можно определить в теории множеств как вторичные объекты, а наоборот нельзя
3) потом пришёл Рассел и всё решил свести к формальной логике - так появилась первая теория типов
«Тот факт, что вся математика есть не что иное, как символическая логика, — величайшее открытие нашего века».
4) потом математики поняли, что типы первичны над логикой. На самом деле фактически это показал тот же Рассел, но он не понял этого, полагая первичной логику.
5) работа Бурбаки описывает всё через порождающие структуры http://inponomarev.ru/teaching/speciesofstructures - вот тут по ссылке учебный курс по теории множеств и по структурам Бурбаки. Порождающие структуры по Бурбаки - это по сути типы аксиом. Некоторое среднее решение вопроса о первичности между теорией типов и логикой. При этом в своём роде окончательное - не вдаваясь в конкретное содержание, все матобъекты представляют собой структуры Бурбаки.
6) современные направления далее развивают это всё через теорию категорий. Особенно популярной оказалась идея, что первичными объектами являются высшие категории. Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.
7) самое современное слово в этой науке - гомологическая теория типов. Согласно ей, первичны не множества, ни логика, ни типы, ни структуры - первичны гомотопии. Кратко можно проследить это так:
из натуральных чисел конструируется что угодно ->
сами натуральные числа естественно появляются в теории множеств как кардиналы и ординалы конечных множеств ->
теория множеств строго может быть построена только аксиоматически и через структуры (теория топосов так возникла, но её считают частью теории множеств - просто топос "множество" один из многих топосов)
-> в конечном счёте всё это - символическая логика, при этом Рассел понял это намного раньше создания теории топосов и работ Бурбаки
-> символическая логика описывается семантикой, значит первичнее семантика (отсюда в том числе лингвистический поворот в философии)
-> дальнейший анализ показывает соотношение семантики и математики - семантика шире математики, математика же есть анализ симметрий семантики
-> все виды симметрий семантики могут быть обобщены как высшие группоиды, а высшие группоиды полностью эквиваленты гомологическим типам
-> значит, гомотопии первичнее
-> изоморфизм Карри-Ховарда показывает. что любое доказательство эквивалентно программе, а значит логические системы, типы и формальные исчисления, логики - это одно и то же, только описанное разными способами
-> на основе этого изоморфизма можно создать гомологическую теорию типов, которая описывает любой математический объект на основе "истинно фундаментальных" - симметрий семантик.
2) потом решили, что лучше брать за основу множества, так как натуральные числа можно определить в теории множеств как вторичные объекты, а наоборот нельзя
3) потом пришёл Рассел и всё решил свести к формальной логике - так появилась первая теория типов
«Тот факт, что вся математика есть не что иное, как символическая логика, — величайшее открытие нашего века».
4) потом математики поняли, что типы первичны над логикой. На самом деле фактически это показал тот же Рассел, но он не понял этого, полагая первичной логику.
5) работа Бурбаки описывает всё через порождающие структуры http://inponomarev.ru/teaching/speciesofstructures - вот тут по ссылке учебный курс по теории множеств и по структурам Бурбаки. Порождающие структуры по Бурбаки - это по сути типы аксиом. Некоторое среднее решение вопроса о первичности между теорией типов и логикой. При этом в своём роде окончательное - не вдаваясь в конкретное содержание, все матобъекты представляют собой структуры Бурбаки.
6) современные направления далее развивают это всё через теорию категорий. Особенно популярной оказалась идея, что первичными объектами являются высшие категории. Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.
7) самое современное слово в этой науке - гомологическая теория типов. Согласно ей, первичны не множества, ни логика, ни типы, ни структуры - первичны гомотопии. Кратко можно проследить это так:
из натуральных чисел конструируется что угодно ->
сами натуральные числа естественно появляются в теории множеств как кардиналы и ординалы конечных множеств ->
теория множеств строго может быть построена только аксиоматически и через структуры (теория топосов так возникла, но её считают частью теории множеств - просто топос "множество" один из многих топосов)
-> в конечном счёте всё это - символическая логика, при этом Рассел понял это намного раньше создания теории топосов и работ Бурбаки
-> символическая логика описывается семантикой, значит первичнее семантика (отсюда в том числе лингвистический поворот в философии)
-> дальнейший анализ показывает соотношение семантики и математики - семантика шире математики, математика же есть анализ симметрий семантики
-> все виды симметрий семантики могут быть обобщены как высшие группоиды, а высшие группоиды полностью эквиваленты гомологическим типам
-> значит, гомотопии первичнее
-> изоморфизм Карри-Ховарда показывает. что любое доказательство эквивалентно программе, а значит логические системы, типы и формальные исчисления, логики - это одно и то же, только описанное разными способами
-> на основе этого изоморфизма можно создать гомологическую теорию типов, которая описывает любой математический объект на основе "истинно фундаментальных" - симметрий семантик.
1) вначале всё свели к натуральным числам.
2) потом решили, что лучше брать за основу множества, так как натуральные числа можно определить в теории множеств как вторичные объекты, а наоборот нельзя
3) потом пришёл Рассел и всё решил свести к формальной логике - так появилась первая теория типов
«Тот факт, что вся математика есть не что иное, как символическая логика, — величайшее открытие нашего века».
4) потом математики поняли, что типы первичны над логикой. На самом деле фактически это показал тот же Рассел, но он не понял этого, полагая первичной логику.
5) работа Бурбаки описывает всё через порождающие структуры http://inponomarev.ru/teaching/speciesofstructures - вот тут по ссылке учебный курс по теории множеств и по структурам Бурбаки. Порождающие структуры по Бурбаки - это по сути типы аксиом. Некоторое среднее решение вопроса о первичности между теорией типов и логикой. При этом в своём роде окончательное - не вдаваясь в конкретное содержание, все матобъекты представляют собой структуры Бурбаки.
6) современные направления далее развивают это всё через теорию категорий. Особенно популярной оказалась идея, что первичными объектами являются высшие категории. Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.
7) самое современное слово в этой науке - гомологическая теория типов. Согласно ей, первичны не множества, ни логика, ни типы, ни структуры - первичны гомотопии. Кратко можно проследить это так:
из натуральных чисел конструируется что угодно ->
сами натуральные числа естественно появляются в теории множеств как кардиналы и ординалы конечных множеств ->
теория множеств строго может быть построена только аксиоматически и через структуры (теория топосов так возникла, но её считают частью теории множеств - просто топос "множество" один из многих топосов)
-> в конечном счёте всё это - символическая логика, при этом Рассел понял это намного раньше создания теории топосов и работ Бурбаки
-> символическая логика описывается семантикой, значит первичнее семантика (отсюда в том числе лингвистический поворот в философии)
-> дальнейший анализ показывает соотношение семантики и математики - семантика шире математики, математика же есть анализ симметрий семантики
-> все виды симметрий семантики могут быть обобщены как высшие группоиды, а высшие группоиды полностью эквиваленты гомологическим типам
-> значит, гомотопии первичнее
-> изоморфизм Карри-Ховарда показывает. что любое доказательство эквивалентно программе, а значит логические системы, типы и формальные исчисления, логики - это одно и то же, только описанное разными способами
-> на основе этого изоморфизма можно создать гомологическую теорию типов, которая описывает любой математический объект на основе "истинно фундаментальных" - симметрий семантик.
2) потом решили, что лучше брать за основу множества, так как натуральные числа можно определить в теории множеств как вторичные объекты, а наоборот нельзя
3) потом пришёл Рассел и всё решил свести к формальной логике - так появилась первая теория типов
«Тот факт, что вся математика есть не что иное, как символическая логика, — величайшее открытие нашего века».
4) потом математики поняли, что типы первичны над логикой. На самом деле фактически это показал тот же Рассел, но он не понял этого, полагая первичной логику.
5) работа Бурбаки описывает всё через порождающие структуры http://inponomarev.ru/teaching/speciesofstructures - вот тут по ссылке учебный курс по теории множеств и по структурам Бурбаки. Порождающие структуры по Бурбаки - это по сути типы аксиом. Некоторое среднее решение вопроса о первичности между теорией типов и логикой. При этом в своём роде окончательное - не вдаваясь в конкретное содержание, все матобъекты представляют собой структуры Бурбаки.
6) современные направления далее развивают это всё через теорию категорий. Особенно популярной оказалась идея, что первичными объектами являются высшие категории. Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.
7) самое современное слово в этой науке - гомологическая теория типов. Согласно ей, первичны не множества, ни логика, ни типы, ни структуры - первичны гомотопии. Кратко можно проследить это так:
из натуральных чисел конструируется что угодно ->
сами натуральные числа естественно появляются в теории множеств как кардиналы и ординалы конечных множеств ->
теория множеств строго может быть построена только аксиоматически и через структуры (теория топосов так возникла, но её считают частью теории множеств - просто топос "множество" один из многих топосов)
-> в конечном счёте всё это - символическая логика, при этом Рассел понял это намного раньше создания теории топосов и работ Бурбаки
-> символическая логика описывается семантикой, значит первичнее семантика (отсюда в том числе лингвистический поворот в философии)
-> дальнейший анализ показывает соотношение семантики и математики - семантика шире математики, математика же есть анализ симметрий семантики
-> все виды симметрий семантики могут быть обобщены как высшие группоиды, а высшие группоиды полностью эквиваленты гомологическим типам
-> значит, гомотопии первичнее
-> изоморфизм Карри-Ховарда показывает. что любое доказательство эквивалентно программе, а значит логические системы, типы и формальные исчисления, логики - это одно и то же, только описанное разными способами
-> на основе этого изоморфизма можно создать гомологическую теорию типов, которая описывает любой математический объект на основе "истинно фундаментальных" - симметрий семантик.
>>68903
это интересно, в какой книжке бурбаки можно прочитать про категории?
> Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.
это интересно, в какой книжке бурбаки можно прочитать про категории?
>>68907
почему?
почему?
>>68908
Topologie algébrique. Chapitres 1 à 4.
Написана посмертно с того света и впервые издана в 2016.
Topologie algébrique. Chapitres 1 à 4.
Написана посмертно с того света и впервые издана в 2016.
>>68908
А я люблю обмазываться современным категорным калом и дрочить. Каждый день я хожу по доске с черным мешком для мусора и собераю в него весь категорный кал, который вижу. На два полных мешка целый день уходит. Зато, когда после тяжёлого дня я прихожу домой, иду в тред для начинающих, говорю новичкам, что их математика не математика…ммм и измазываю тред категориями. И дрочу, представляя, что меня поглотила единая категория. Мне вообще кажется, что категории, умеют думать, у них есть свои семьи, города, чувства, не смывайте их в унитаз, лучше приютите у себя, говорите с ними, ласкайте их…. А вчера в ванной, мне преснился чудный сон, как будто я нырнул в море, и оно прератилось в копредел, функторы, кольца, поля, все из говна, даже первая культура, даже Аллах!.
А я люблю обмазываться современным категорным калом и дрочить. Каждый день я хожу по доске с черным мешком для мусора и собераю в него весь категорный кал, который вижу. На два полных мешка целый день уходит. Зато, когда после тяжёлого дня я прихожу домой, иду в тред для начинающих, говорю новичкам, что их математика не математика…ммм и измазываю тред категориями. И дрочу, представляя, что меня поглотила единая категория. Мне вообще кажется, что категории, умеют думать, у них есть свои семьи, города, чувства, не смывайте их в унитаз, лучше приютите у себя, говорите с ними, ласкайте их…. А вчера в ванной, мне преснился чудный сон, как будто я нырнул в море, и оно прератилось в копредел, функторы, кольца, поля, все из говна, даже первая культура, даже Аллах!.
>>68934
(типичные размышления деда с dxdy о современной математике)
(типичные размышления деда с dxdy о современной математике)
>>74477
Потому что математика, а не программирование.
Как там пруверы, уже хотя бы теоремы ХХ века вроде теоремы об индексе могут доказать?
Потому что математика, а не программирование.
Как там пруверы, уже хотя бы теоремы ХХ века вроде теоремы об индексе могут доказать?
>>74488
Так программы тоже раньше на листочке писали, но потом поняли, что так ошибки могут появится. Так и с теоремами, тем более учитывая изоморфизм Карри-Говарда однозначно связывающий математику и программирование.
Базу теорем же люди введут, при том более профессиональные, так что риск ошибки из-за человеческого фактора понижается. А на листочке что? Даже не проверит толком никто.
Так программы тоже раньше на листочке писали, но потом поняли, что так ошибки могут появится. Так и с теоремами, тем более учитывая изоморфизм Карри-Говарда однозначно связывающий математику и программирование.
Базу теорем же люди введут, при том более профессиональные, так что риск ошибки из-за человеческого фактора понижается. А на листочке что? Даже не проверит толком никто.
>>74504
а) В пруверах ничего внятного и интересно не доказано.
б) Читать пруверские доказательства это просто пиздец, а то что их проверил компилятор не дает никакого приемущества, все и так знают про большинство гипотез верные они или нет. Это то же самое, что музыку играть в миди проигрывателях, можно, если тебе лично это нужно зачем-то.
а) В пруверах ничего внятного и интересно не доказано.
б) Читать пруверские доказательства это просто пиздец, а то что их проверил компилятор не дает никакого приемущества, все и так знают про большинство гипотез верные они или нет. Это то же самое, что музыку играть в миди проигрывателях, можно, если тебе лично это нужно зачем-то.
>>74477
Потому что тебя, долбоеба, пытаются научить думать. Вероятно зря.
Потому что тебя, долбоеба, пытаются научить думать. Вероятно зря.
>>74504
Ох лол, даже не знаю, ты просто тролль зелёный или ещё юный и наивный.
На твой изоморфизм всем похую также, как похую, например, на теорему Кэли о группах, которая вроде как и важная, а нигде никогда не применяется, потому что себе дороже.
Ещё раз, где моя теорема об индексе в прувере? Ну раз изоморфизм, то это вообще на раз-два.
>тем более учитывая изоморфизм Карри-Говарда однозначно связывающий математику и программирование.
Ох лол, даже не знаю, ты просто тролль зелёный или ещё юный и наивный.
На твой изоморфизм всем похую также, как похую, например, на теорему Кэли о группах, которая вроде как и важная, а нигде никогда не применяется, потому что себе дороже.
Ещё раз, где моя теорема об индексе в прувере? Ну раз изоморфизм, то это вообще на раз-два.
>>74504
Только конструктивную её часть, а это 0.00001% от всей математики.
>однозначно связывающий математику и программирование.
Только конструктивную её часть, а это 0.00001% от всей математики.
>>74531
>>74552
>>74555
Ты же сам понимаешь, что твои "аргументы против пруверов" доказывают только то, что те, кто считает себя математиками, в 99 случаев из 100 не могут в пруверы, ибо деревянные по пояс. "Дело было не в бобине", как говорится. Если бы ты понимал, о чем вообще изоморфизм Карри-Говарда, ты бы не нёс такую хуйню. А так, имеем то что имеем...
>>74552
>>74555
Ты же сам понимаешь, что твои "аргументы против пруверов" доказывают только то, что те, кто считает себя математиками, в 99 случаев из 100 не могут в пруверы, ибо деревянные по пояс. "Дело было не в бобине", как говорится. Если бы ты понимал, о чем вообще изоморфизм Карри-Говарда, ты бы не нёс такую хуйню. А так, имеем то что имеем...
>>74700
Это не голословное утверждение, кстати. Года три ещё назад Сохацкий писал, что ихние академики не могут даже установить HoTT либу в коке. Агду с нужными либами какой-нибудь условный Вербицкий даже установить не осилит, про использование я вообще молчу
> те, кто считает себя математиками, в 99 случаев из 100 не могут в пруверы, ибо деревянные по пояс.
Это не голословное утверждение, кстати. Года три ещё назад Сохацкий писал, что ихние академики не могут даже установить HoTT либу в коке. Агду с нужными либами какой-нибудь условный Вербицкий даже установить не осилит, про использование я вообще молчу
>>74702
Миша вообще в линуксе сидит, насколько я помню
У вас спесь головного мозга в последней стадии, классическое "вы не понимаете, это настолько сложно, что большинство математиков даже не смогут установить, не то что использовать"
Ну и логическая ошибка обобщения, как всегда у программистов
хотт-верунов просят уже который раз показать пример доказательства сколько-нибудь содержательной теоремы вроде теоремы об индексе, а они всё уводят разговор на какую-то нерелевантную солому
"Нет, пока доказать ничего нельзя, но зато УСТАНАВЛИВАТЬ нужно ууууух как сложно, да"
> Агду с нужными либами какой-нибудь условный Вербицкий даже установить не осилит, про использование я вообще молчу
Миша вообще в линуксе сидит, насколько я помню
У вас спесь головного мозга в последней стадии, классическое "вы не понимаете, это настолько сложно, что большинство математиков даже не смогут установить, не то что использовать"
Ну и логическая ошибка обобщения, как всегда у программистов
хотт-верунов просят уже который раз показать пример доказательства сколько-нибудь содержательной теоремы вроде теоремы об индексе, а они всё уводят разговор на какую-то нерелевантную солому
"Нет, пока доказать ничего нельзя, но зато УСТАНАВЛИВАТЬ нужно ууууух как сложно, да"
>>74703
Сейчас каждый первый нитакойкаквсе зумер в линуксе сидит.
Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.
> Миша вообще в линуксе сидит, насколько я помню
Сейчас каждый первый нитакойкаквсе зумер в линуксе сидит.
Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.
Но на самом деле с пруверами в плане установки все не так печально. Есть мейд ин Блинолопатия прувер - arend, там не только HoTT искаропки и даже дополнительная либа с кубической теорией типов, но и установка в один клик мышкой, как плагин к intellij idea, что в свою очередь ставится в два клика https://arend-lang.github.io/ так что прогресс налицо, скоро HoTT будет доступна широким народным массам, в том числе и мнящим себя математиками неосиляторам. Нотацию все равно осиливать придется, правда
О, там новый релиз, теперь основная либа тоже ставится в один клик. Короче, хоть на это переползайте, раз уж даже агду поставить не можете.
> Plugin updates:
> arend-lib can be downloaded and upgraded from the IDE
>>74700
>>74700
Мой аргумент в том, что плюсы которые дают пруверы сомнительные, а минусы явные и конкретные.
Не нужно их пропагандировать остальным, а нужно желающим (тебе) взять и доказать в них что-нибудь такое убедительное, чтобы все охуели и тогда вопросов бы не было.
Никто не спорит, можно и на КОБОЛЕ доказать, только нахуя? Времени это займет много, новизны никакой не будет, а людям жрать что-то надо.
>>74700
Мой аргумент в том, что плюсы которые дают пруверы сомнительные, а минусы явные и конкретные.
Не нужно их пропагандировать остальным, а нужно желающим (тебе) взять и доказать в них что-нибудь такое убедительное, чтобы все охуели и тогда вопросов бы не было.
>Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.
Никто не спорит, можно и на КОБОЛЕ доказать, только нахуя? Времени это займет много, новизны никакой не будет, а людям жрать что-то надо.
>>74700
Так я понимаю, потому и пишу
>Если бы ты понимал, о чем вообще изоморфизм Карри-Говарда
Так я понимаю, потому и пишу
>Только конструктивную её часть, а это 0.00001% от всей математики.
>>74704
Ну то есть ни одной вразумительной теоремы современной актуальной математики хотя бы ХХ века, доказанной с помощью прувера образца 2020 года, ты привести не можешь, как и ожидалось.
Так и сказал бы, что ты пустозвон. Пердежу-то на всю доску от тебя.
>Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.
Ну то есть ни одной вразумительной теоремы современной актуальной математики хотя бы ХХ века, доказанной с помощью прувера образца 2020 года, ты привести не можешь, как и ожидалось.
Так и сказал бы, что ты пустозвон. Пердежу-то на всю доску от тебя.
>>74711
Если бы понимал, то не писал бы такую хуйню.
>>74712
Когда докажут - ты будешь точно так же кукарекать.
>>74708
Нельзя, он тьюринг-полный, сначала придется прувер на нем писать.
Автоматизация. Что-то простое человек доказать может, что-то посложнее - уже нет. Доказательство чего-то нетривиального в IUTeich человек просто не осилит, никакой. А это ещё не самое сложное.
Если бы понимал, то не писал бы такую хуйню.
>>74712
Когда докажут - ты будешь точно так же кукарекать.
>>74708
> можно и на КОБОЛЕ доказать
Нельзя, он тьюринг-полный, сначала придется прувер на нем писать.
> нахуя? Времени это займет много, новизны никакой не будет
Автоматизация. Что-то простое человек доказать может, что-то посложнее - уже нет. Доказательство чего-то нетривиального в IUTeich человек просто не осилит, никакой. А это ещё не самое сложное.
>>74718
ну да, сначала прувер, а потом доказать, это смешно хоть
Встретимся на этом же месте через сто лет, пока доказали две теоремы, обычные доказательства которых были придуманы в 60-ые. Я не спорю, может быть сейчас разгонятся и все начнут доказывать, микрософт финансирует. Но больше похоже на модную хуйню: денег освоят и забудут.
>Нельзя, он тьюринг-полный, сначала придется прувер на нем писать.
ну да, сначала прувер, а потом доказать, это смешно хоть
>Когда докажут - ты будешь точно так же кукарекать.
Встретимся на этом же месте через сто лет, пока доказали две теоремы, обычные доказательства которых были придуманы в 60-ые. Я не спорю, может быть сейчас разгонятся и все начнут доказывать, микрософт финансирует. Но больше похоже на модную хуйню: денег освоят и забудут.
>>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
>Когда докажут - ты будешь точно так же кукарекать.
почему до сих пор не доказали?
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
>>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
>Когда докажут - ты будешь точно так же кукарекать.
почему до сих пор не доказали?
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
>>74718
Нет, если реально докажут что-то, и это будет не ад хок хуита, адаптированная специально для одной единственной теоремы, то я соглашусь, что это круто, и может даже почитаю что-то.
А пока вы все со своими хотт, категориями в хаскеле, и записями лекций в имакс сидите у меня в одной корзине погромистов-второкурсников и лукавых грантопильщиков.
>Когда докажут - ты будешь точно так же кукарекать.
Нет, если реально докажут что-то, и это будет не ад хок хуита, адаптированная специально для одной единственной теоремы, то я соглашусь, что это круто, и может даже почитаю что-то.
А пока вы все со своими хотт, категориями в хаскеле, и записями лекций в имакс сидите у меня в одной корзине погромистов-второкурсников и лукавых грантопильщиков.
>>74810
Это неудивительно, ты ж даже не понимаешь, о чем не только HoTT, но даже тот же изоморфизм Карри-Говарда.
> А пока вы все со своими хотт, категориями в хаскеле, и записями лекций в имакс сидите у меня в одной корзине погромистов-второкурсников и лукавых грантопильщиков.
Это неудивительно, ты ж даже не понимаешь, о чем не только HoTT, но даже тот же изоморфизм Карри-Говарда.
>>74820
И о чём же?
И о чём же?
>>74820
Тут больше одного анона сидит, если что.
>Это неудивительно, ты ж даже не понимаешь, о чем не только HoTT, но даже тот же изоморфизм Карри-Говарда.
Тут больше одного анона сидит, если что.
>>74820
Я так понимаю, там принцип как у теорем существования. В случае, если есть доказательство обычное, то существует и на прувере и можно его написать. Последний шаг, разумеется, остается как упражнение для любопытных студентов и пенсионеров.
Я так понимаю, там принцип как у теорем существования. В случае, если есть доказательство обычное, то существует и на прувере и можно его написать. Последний шаг, разумеется, остается как упражнение для любопытных студентов и пенсионеров.
>>68197
>>68191
>>68201
>>68203
>>68208
И много других постов от этого мерзкого ублюдка. Граждане математики, обратите внимание, в треде орудует чмо, которое математику не знает, ни одного математического определения не использует, дабы не обосраться(хотя с зфс однажды все же обосрался), и пытается мимикрировать, отвечая односложно в духе "ваша математика - религия, коткудахкудахтахтах ", "почему нет, и что с того" и прочими мусорными способами, уводя дискуссию. Я сам сюда захожу редко, однако сейчас у меня было хорошее настроение, я пил чай, думал над темой магистерской и тут это программистское чмо мне испортило настроение. Посему :
Репортите его, дабы изгнать это чмо.
Всех благ, господа математики.
>>68191
>>68201
>>68203
>>68208
И много других постов от этого мерзкого ублюдка. Граждане математики, обратите внимание, в треде орудует чмо, которое математику не знает, ни одного математического определения не использует, дабы не обосраться(хотя с зфс однажды все же обосрался), и пытается мимикрировать, отвечая односложно в духе "ваша математика - религия, коткудахкудахтахтах ", "почему нет, и что с того" и прочими мусорными способами, уводя дискуссию. Я сам сюда захожу редко, однако сейчас у меня было хорошее настроение, я пил чай, думал над темой магистерской и тут это программистское чмо мне испортило настроение. Посему :
Репортите его, дабы изгнать это чмо.
Всех благ, господа математики.
>>74897
Платонист, спок
Платонист, спок
Ип
Воеводский сам что-то доказал с помощью hott?
>>74897
Ты вот на это мне ответь, я правильно понимаю ваш езормфизъмъ?
>Я так понимаю, там принцип как у теорем существования.
Ты вот на это мне ответь, я правильно понимаю ваш езормфизъмъ?
>>74912
Ну или не он, но сомневаюсь, что есть два таких конструктуха.
Ну или не он, но сомневаюсь, что есть два таких конструктуха.
Фигасе. Вы все еще сретесь тут? https://www.youtube.com/watch?v=21qPOReu4FI
>>75296
Упоротый, даже лекцию прочитал на тему статьи. Конструктухи это клуб фанатиков, я не видел, чтобы какой-нибудь Лури носился по миру и орал "5 шагов принятия высших категорий", "высшие топосы это будущее математики, умоляю, используйте их в доказательстве" итд итп.
Упоротый, даже лекцию прочитал на тему статьи. Конструктухи это клуб фанатиков, я не видел, чтобы какой-нибудь Лури носился по миру и орал "5 шагов принятия высших категорий", "высшие топосы это будущее математики, умоляю, используйте их в доказательстве" итд итп.
>>75303
Если ты чего-то не видел, это не значит, что этого не было.
Если ты чего-то не видел, это не значит, что этого не было.
>>67659 (OP)
было несколько знакомых пациентов лет пять назад, все так или иначе относились к СПбАУ.
было несколько знакомых пациентов лет пять назад, все так или иначе относились к СПбАУ.
>>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льтат или нет.
На б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льтат или нет.
>>67659 (OP)
А что это за бублик на оп пике?
А что это за бублик на оп пике?
>>68185
Из цитаты видно, что автор (1) триггерится на слово "рефакторинг" и (2) завидует математикам до зубовного скрежета.
"Скажите, как его зовут?" (с)
>Воеводский был жемчужиной, а прувер написать не смог.
>Зато медаль получил, за пофиксаного Блоха-Като, рефакторер блядь.
>С-системы его ёбнутые.
>Ты реально переоцениваешь математиков.
Из цитаты видно, что автор (1) триггерится на слово "рефакторинг" и (2) завидует математикам до зубовного скрежета.
"Скажите, как его зовут?" (с)
Господа, а вот там Тифарет в своем тифаретнике пишет, что фигурант данного треда продолжительно продолжал употреблять вещества группы диссоциативов, в частности на букву К.
может кто-нибудь из присутствующих фармакологов объяснить неопытному посетителю чисто для кругозора, к каким наблюдаемым симптомам приводит употребление данного круга веществ? как это могло сказаться на фигуранте обсуждения?
может кто-нибудь из присутствующих фармакологов объяснить неопытному посетителю чисто для кругозора, к каким наблюдаемым симптомам приводит употребление данного круга веществ? как это могло сказаться на фигуранте обсуждения?
>>80424
он там про шеня что-то написал, то ли хуесосит а шень няшный, то ли имеет в виду что-то своё, понятное только близким друзьям. Я не понял
А где он про "фигурант данного треда" пишет, я не вижу
тоже темнишь что-то
он там про шеня что-то написал, то ли хуесосит а шень няшный, то ли имеет в виду что-то своё, понятное только близким друзьям. Я не понял
А где он про "фигурант данного треда" пишет, я не вижу
тоже темнишь что-то
>>80424
По первым же ссылкам из гугла описываются симптомы, похожие на то, что рассказывал фигурант
По первым же ссылкам из гугла описываются симптомы, похожие на то, что рассказывал фигурант
>Наблюдается гиперактивность человека, которая сопровождается странным мышлением и невнятной речью. Наркоман может рассказывать о несуществующих вещах и галлюцинациях. Подобные видения постепенно прогрессируют и превращаются в постоянное явление, тем самым, формируя у человека фобии.
> дезориентированы, испытывают ощущение, что они "находятся в другом измерении", "общаются с Богом", "с дьяволом", переносятся в другие места, слышат какую-то особую "неземную" музыку и пр. Некоторые лица в период интоксикации ощущают безграничные творческие способности: им кажется, что они сочиняют музыку, складывают стихи, им приходят в голову удивительные фасоны одежды и пр.
>>80435
разве "нулевой пациент" существенно благозвучнее? хм.
разве "нулевой пациент" существенно благозвучнее? хм.
>>80433
удивительные фасоны оснований математики, ага.
>им приходят в голову удивительные фасоны одежды и пр.
удивительные фасоны оснований математики, ага.
>>80512
а вдруг их несколько? или они размножаются...
а вдруг их несколько? или они размножаются...
Вопрос к адептам и сектантам. Сегодня, а может и давным давно, мне во сне явился ангел. Мы перетерли за математику. Произошло озарение.
Есть симплициальная категория Delta. Есть кубическая категория I, даже в нескольких версиях. С дельтой в hott вроде все кисло. С кубиками лучше.
Есть категория Gamma имени Сигала. Есть Sym^{op}, скелет FinSet^{op}. Гамма относится к дельте, как сим-оп к кубикам. Я не знаю, насколько это известно и банально, но это так.
1. Ясно, что дельта и кубики - это что-то ассоциативное, а гамма и сим-оп - это что-то ассоциативное и коммутативное. Есть ли в hott утверждение вида "когда ассоциативно - это гомотопический тип, а когда еще и коммутативно - это спектр"?
2. Гомотопический тип - это хороший предпучок и на дельте, и на кубиках. С гаммой и сим-оп все сложнее. Хороший симплициальный предпучок на гамме - это связный спектр. Хороший предпучок на сим-оп, со значениями в категории симплициальных множеств с отмеченной точкой, - это спектр, не обязательно связный. Раз в одном случае эквивалентность есть, а в другом эквивалентности нет, оба случая нетривиальны и содержательны. Hott как-нибудь помогает увидеть это нетривиальное содержание?
Есть симплициальная категория Delta. Есть кубическая категория I, даже в нескольких версиях. С дельтой в hott вроде все кисло. С кубиками лучше.
Есть категория Gamma имени Сигала. Есть Sym^{op}, скелет FinSet^{op}. Гамма относится к дельте, как сим-оп к кубикам. Я не знаю, насколько это известно и банально, но это так.
1. Ясно, что дельта и кубики - это что-то ассоциативное, а гамма и сим-оп - это что-то ассоциативное и коммутативное. Есть ли в hott утверждение вида "когда ассоциативно - это гомотопический тип, а когда еще и коммутативно - это спектр"?
2. Гомотопический тип - это хороший предпучок и на дельте, и на кубиках. С гаммой и сим-оп все сложнее. Хороший симплициальный предпучок на гамме - это связный спектр. Хороший предпучок на сим-оп, со значениями в категории симплициальных множеств с отмеченной точкой, - это спектр, не обязательно связный. Раз в одном случае эквивалентность есть, а в другом эквивалентности нет, оба случая нетривиальны и содержательны. Hott как-нибудь помогает увидеть это нетривиальное содержание?
>>80566
выкиньте свои комплексы Кана, вместе со всей фибратной демагогией, прямо в анналы истории, и Квиллена туда же, быстро, решительно.
если вы обращали внимание, то Сова хвалит Лури, который тоже увлекался именно эти клеточными комплексами, но зато Каледин ругает. и для того есть причины.
выкиньте свои комплексы Кана, вместе со всей фибратной демагогией, прямо в анналы истории, и Квиллена туда же, быстро, решительно.
если вы обращали внимание, то Сова хвалит Лури, который тоже увлекался именно эти клеточными комплексами, но зато Каледин ругает. и для того есть причины.
>>81561
типа сидит каледин такой, на лурье подрачивает, утомился, зашёл в блог совы... ба! а сова, оказывается, лурье любит! быстрее побегу, напишу, как я лурье не выношу вообще
типа сидит каледин такой, на лурье подрачивает, утомился, зашёл в блог совы... ба! а сова, оказывается, лурье любит! быстрее побегу, напишу, как я лурье не выношу вообще
>>80570
ок, выкинули, дальше какие инструкции будут?
ок, выкинули, дальше какие инструкции будут?
>>81591
Вышел модуль на крыльцо
Расширить себе кольцо
Сунул функтор нет кольца
Так и шлёпнулся с крыльца
Вышел модуль на крыльцо
Расширить себе кольцо
Сунул функтор нет кольца
Так и шлёпнулся с крыльца
>>81733
Можно вместо "расширить" использовать "растянуть"?
Можно вместо "расширить" использовать "растянуть"?
>>68202
Нормально там всё, книгу‐то открой хотя бы.
Нормально там всё, книгу‐то открой хотя бы.