Господа и дамы, сообщите хотя бы частичную информацию: когда, а главное - где и/или от кого вы узнали про homotopy type theory? Нужно отследить цепочку распространения заразы вплоть до нулевого пациента. (понятно кого)
Что в ней плохого, объясните?
Трактор @ хочешь остаться - давай считай количественный результат @ компьютер программировать @ Haskell @ Ocaml @ Coq @ Воеводский @ HoTT
Как-то так.
> (понятно кого)
Кого? Понятно кому?
Эх, друже, после нормальной математики хаскелом занялся...
остальное - клёвые вещи, так держать
>нормальной математики хаскелом занялся
Почему математики такие высокомерные?
>>67710
А ты, физик, сам как считаешь, то что ты докатился до хаскеля, это деградация?
>Почему математики такие высокомерные?
не увидел в его посте высокомерия, честно говоря
что нравится, тем и занимайся
но сравнивать хаскелл с математикой, скажем, брст вполне себе можно объективно
то, что она в разы или даже на целые порядки проще в первом случае, тебя волновать не должно, если тебя интересует эта область
>деградация
не он, но брст я проходил
если под деградацией понимать уменьшение сложности, то да
это как учиться лет 10 в музыкалке и консерватории, чтобы потом играть собачий вальс одним пальцем
Хаскель это грааль теории категорий, которая в свою очередь является программироваем и второй культурой.
>Хаскель это грааль теории категорий
Ну не то, чтобы там была какая-то особо замысловатая теория категорий.
>>67659 (OP)
Уже довольно давно (лет 8 назад), когда я учил логику.
Если ты уже веришь в реальность вне-временных бесконечных объектов, что очень естественно для математиков, то почему бы еще не принять бога.
>А ты, физик, сам как считаешь, то что ты докатился до хаскеля,
На самом деле я больше по Coq / OCaml, а не по Хаскелю.
> это деградация?
Соглашусь, что занятие теорией/математикой, так сказать, "на бумажке" -- это чуть более "возвышенная" деятельность, чем запрограммировывание пусть и того-же самого. С другой стороны, мне, как физику, приятно видеть как мои идеи реализовываются "в железе". Кроме того, у меня довольно хаотичное мышление - физически не могу исписывать 40 листовые тетрадки выкладками как некоторые коллеги. Компьютер помогает организовывать и проверять -- Coq мне находил пару нетривиальных ошибок в моих построениях.
Т.е. я бы на "это деградация?" ответил что это вопрос вкуса и личных предпочтений, но... Не знаю как оно у математиков, но среди физиков наблюдал неоднократно что навык программирования вызывает у многих чувство некоего такого испуганного раздражения. Особенно если автоматизировать какую-нибудь муторную символьную выкладку - могут почти открыто злиться на тебя. И вот это довольно сложно объяснить только тем, что это им "не интересно".
это >>67733 не я
>, а главное - где и/или от кого вы узнали про homotopy type theory?
Интервью с Воеводским.
Просто пограмирование отвратительный аутизм и тупость, вполне понятно, что адеквату неприятно марать этим мозг.
Не понял, на что конкретно физики раздражаются и почему злятся на тебя?
>Просто пограмирование отвратительный аутизм и тупость, вполне понятно, что адеквату неприятно марать этим мозг.
Ты правда считаешь, что программирование хуже чем та деятельность, которую оно автоматизирует?
Как по мне, автоматизация нудных выкладок, о которой пишет >>67741, это безусловно позитивная вещь.
> на что конкретно
Деталей не хочу говорить, слишком деанон.
Пример 1: докладываю семинар @ вот модель, вот пара нетривиальных свойств модели, все формально доказано @ у дядечки вопрос "а вот если такой параметр то это контрпример" @ аlt-tab вбиваю параметр в конфиг, запускаю Coq @ за две секунды готово доказательство что все ок @ дядечка остался злой и недовольный.
Пример 2: есть несколько классов моделей, скажем A,B,C и у каждой параметр - натуральное число. Коллега взял модель B2, сказал, что она наиболее интересная из " соображений натуральности" и навыводил ее свойств, опубликовав статью с полотнами выкладок. Взялся делать то-же самое для С1. А тут я со своим Coq - вбиваешь класс модели и параметр - через секунду получаешь ту самую портянку со всеми доказательствами. Коллега со мной с тех пор не разговаривает.
> почему злятся на тебя?
Яж почем знаю...
Похоже, высокоинтеллектуальные круги - тот еще гадюшник. Слышал, что шахматисты тоже люто, бешено ненавидят друг друга.
Ради любопытства, в чем бонус Coq в такого рода деятельности? Казалось бы для обсчета моделей куда проще было бы использовать систему символических вычислений. Понятно, что так не получишь формального доказательства; но обычно в физике никто и не ставит таких критериев строгости. При этом получение именно формального доказательства вещь явно не бесплатная и требует кучи дополнительных усилий.
>Ради любопытства, в чем бонус Coq в такого рода деятельности?
Опять детали не скажу. Это специфика данной области теорфизики - тут Coq очень хорошо подходит.
Нет. Хейта к коку нет, есть хейт к его слепым последователям, которые утверждают, что маняматика нинужна и автоматизированные пруверы - будущее. У таких вот "экспертов" просто не хватает образования, чтобы понять, о чём вообще современная математика, но они её уже "решили".
Тебеж >>67752 объяснил -- по статье в год на каждое натуральное число. И получ, что ты не хуйней страдаешь, а ресерч.
Это практическое виденье.
Я о тех кому и образование достает и денег не особо требуется. Что с ними не так?
> Не на бумаге, а в голове.
А что у тебя есть волшебного математического в голове, чего нет в математической нотации на бумаге? Особая уличная магия?
> Это специфика данной области теорфизики
И что же это за область?
> Я о тех кому и образование достает и денег не особо требуется. Что с ними не так?
Тут как с историей антисептиков в медицине. Врач Земмельвейс показал, что если мыть руки с хлоркой перед операцией, а не после, то внезапно смертность послеоперационных больных от сепсиса падает с 60% до 1-2. И что, его признали спасителем? Хуй там. Затравили, заруинили карьеру, позже вообще в дурку упекли. Потому что для абсолютного большинства светил медицины признать себя дебилом, не могущим в банальное мытье рук, хуже всего. Так и тут. ЧСВ важнее практических результатов, даже если речь о жизнях людей, про математику и говорить нечего. Кто сознательно откажется от высокопарных кукареканий о первой культуре и о чем-то волшебном в голове, чего нет в бездуховном коке? Да никто, это равносильно признанию себя дебилом.
Есть такая гипотеза, что чтобы что-то доказать, убедить другого математика(и себя тоже) в некоторой теореме, не нужно делать все выкладки. Если её принимать как истину, тогда "верификация -- это дополнительная работа". Но тогда получается, что один раз её сделал автор и её сделал каждый читатель. Зачем перекладывать? Верифицировать -- просто, приятно и кучу ошибок и интересных нюансов можно найти. Ответ прост: ещё нет устоявшихся стандартов верификации: всяким нормальным кокам и хорошим аналогам обычно около 30 лет разработки. И они синтаксис меняют.
недавно какой то пидорас рассказал про неё. Он хоть и пидорас, но вдруг что то полезное говорит. А что, в чём проблема этой homotopy type theory?
Но есть ли у тебя хоть какие-нибудь истории успеха в математике, когда во время попытки формализации поймали существенную ошибку? Т.е. не просто какую-нибудь техническую лемму, которая была сформулирована в излишней общности, когда она уже не верна, но общий ход доказательства от этого не страдает. А вот, чтобы было что-то не так с какой-то важной теоремой, которой действительно пользовались другие математики.
Если нет, то все о чем ты говоришь - это чисто спекулятивная польза. Но при этом ты предлагешь вкладывать в это очень реальные усилия.
Я слышал о примере, когда нашли уязвимость в каком-то протоколе во время его верификации. Так что наверное в компьютерной безопасности формальная верификации вещь в самом деле полезная.
>Но тогда получается, что один раз её сделал автор и её сделал каждый читатель
Это неадекватный взгляд на то, как и почему читают математические статьи. Собственно верификацией читатели занимаются не так часто; обычно или если читатель это ответственный рецензент или если заявлен интересный результат, но есть подозрения в наличие ошибки (кстати и в таком случае искать ошибки тотально построчной проверкой - это контр-продуктивно, куда лучше искать в статье подозрительные утверждения и таким образом локализовать свое внимание на фрагментах где есть серьезные основания ожидать ошибку). Иначе цель состоит в том, чтобы понять, в чем состоят результаты и извлечь идеи доказательств/конструкций. И для последнего формализация никак не поможет. Скорее наоборот, если кто-то только произведет верификацию в Коке, но не напишет нормальную статью, то разобраться в доказательстве станет труднее.
>Но есть ли у тебя хоть какие-нибудь истории успеха в математике
Для этого надо знать математику, лол
> Но есть ли у тебя хоть какие-нибудь истории успеха в математике, когда во время попытки формализации поймали существенную ошибку?
Есть. Заповедью исключенного третьего и актуальной бесконечности пользовались веками, пока Брауэр не показал, что это просто когнитивные искажения, и основывать на них точные знания - ошибка.
>пока Брауэр не показал
"Показал"? Ты сделал ошибку в слове "заповедовал".
>>67870
Ну-ну. А по факту как всегда ни одного ответа по существу, например на >>67781 , одна анальная клоунада. Ничего нового, одна попаболь одного еблана от HoTT итд...
А прогреры уже запрогали ГоТТ так, чтобы он в Браузере работал? Или надо себе приложение на комп качать?
я тоже угораю по пруверам, и тоже в латехе сначала писал, лекции все конспектировал дотошно, хоттом переболел успешно(хуйня, не ведитесь, классическая математика в миллион раз круче)
Я истории успеха не искал и наверное их не так просто найти.
Сужу по себе: без формализации меня бы математике не научили бы никогда, потому что формат "прочёл книгу -- понял", или тем более "лектор сказал-- студент записал и вызубрил" не работает. Нет глубины необходимой.
А с верификацией оно проще будет. Сколько раз находил интересные тонкие, но важные подробности казалось бы уже известных мне теорем, без которых знание было бы искажено.
Какую-то хуйню говоришь. При чём тут твоё личное непонимание материала и, блядь, верификация? Высрал какой-то нонсеквитур (стромэн-детектор шизик триггеред). А кому-то мастурбация помогает понять материал, мы будем на основе этого делать выводы насчёт её роли в современной математике?
Ты просто не крутишься в математической среде, вот ты и не можешь понять каких-то простейших книжек. Пока ты там ебёшься со своими пруверами, обычный математик просто спросит на кафедре или, если тема сложная, инициирует семинарчик и там всё обсудят, статейки поковыряют.
Анекдотический пример, вобщем. Ну а мне в понимании книг помогает чтение других книг.
До кучи ещё и ложная эквивалентность - формализация и верификация. Как будто блядь до пруверов все математики на пальцах всё доказывали, а потом пришли матлогики и хачкеллоёбы и понеслась.
> обычный математик просто спросит на кафедре
Рассмешил... Это ты траллишь так, да? Да?
Да не, он не троллит, он просто токсичный долбоёб, который ни одной теоремы не доказал, но имеет "очень ценное мнение".
Нет, это правда. Математик без общения это не математик, а калека, фрик. Ни один успешный математик еще не жил без общения в среде.
Так вот почему во всех книгах по математике подача материала напоминает бред шизофреника.
Надо просто в той же среде крутиться, что и автор.
>во всех книгах по математике
>бред
>>67950
>токсичный долбоёб,
Традиционный баттхёрт неосиляторов. Это единственная группа анонимусов, которая стабильно обижается на всю доску уже вот три.. четвёртый год даже.
>>67950
>токсичный
Уябывай уже на реддит, и strawman свой захвати.
А ну так сразу видно почему вашему брату пруверы не нравятся. Так ты "успешный математик" крутящийся в элитарных кругах, который если что может "просто спросить на кафедре". А тут оказывается что можно git clone все доказательства, и ценность всех твоих социальные элитосвязей внезапно сильно уменьшилась.
Правильно ли я понимаю, что когда мы дотрагиваемся до стены, то молекулы нашего пальца начинают взаимодействовать с молекулами стены, обмениваясь на бешеной скорости кварками, и из за этого палец не пролазиет в стену?
Слушай, ну всё, прямо уел меня, не спец я в К-теории, ну разве что могу когомологии де рама посчитать на многообразиях.
Если ты специалист, то зачем это нужно, какие проблемы решает? Может быть действительно стоит изучить
>тут оказывается что можно git clone все доказательства, и ценность всех твоих социальные элитосвязей внезапно сильно уменьшилась.
Я эти маняфантазии уже сотый раз слышу, но вот на практике почему-то всё наоборот и в точности как говорит анон выше.
А ты типа идеалист и надеешься на успешность и адекватность присутствующих? Кто из нас в итого ебобо?:)
Тем временем ты не говоришь какие проблемы решает твоя область математики. Кто её у тебя купит? (Даже чисто гипотетически)
На пруверах можно программы верифицировать, в том числе квантовые, а твоя теория ходжа и к теория ну куда её. Диффуры решать на многообразиях? А их кому продавать?
Доказательства везде написаны, интуицию за ними тебе никто просто так не даст. Вполне может быть, прочитал ты и не понял. Открой, например, доказательство Перельмана. Что будешь делать? Читать до посинения?
>анон выше
А чего тогда вы вместе с "аноном выше" и ОПом кудахчете так на пруверы? Ну бегают там хипстеры-программисты-аутисты какие-то, в отличие от вас, элитарных, доступа к "спросить на кафедре" не имеют. Толку от этих ваших пруверов нет - тру математика только "на кафедре". Ну и хрен бы с ними?
На бумаге вообще ничего нет.
По определению понимания (какому бы то ни было, несуществующему), понимание --- это то, что происходит у тебя в голове.
Человек --- мера всех вещей.
И именно это понимание и является первичным объектом, а определения теоремы доказательства --- вторичным, производным.
На верификацию вообще всем насрать, кроме фриков. Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
> На бумаге вообще ничего нет.
> По определению понимания (какому бы то ни было, несуществующему), понимание --- это то, что происходит у тебя в голове.
> Человек --- мера всех вещей.
> И именно это понимание и является первичным объектом, а определения теоремы доказательства --- вторичным, производным.
Охуеть, откровения какие. Ещё несколько лет, глядишь и до интуиционизма додумаешься. А вот суть формализма как раз в том, что все нужное - на бумаге, и зависит только от непротиворечивости используемой аксиоматики. От головы в данном случае зависит только выбор аксиоматики, какой набор заповедей больше зайдет - ZFC там, NBG итд. Гедель, правда, доказал что это для оснований не подходит, да и ладно, хуй с ним.
> На верификацию вообще всем насрать, кроме фриков. Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
Ну да, во всякой прикладухе так и есть. Сантехнику не нужна физика, гамалогии можно трясти без оснований.
Да, вот на этой процитированной фразе, а также на вопросе "чьи проблемы твоя область решает, кроме твоих", тот анон явно сливается.
Вот именно, ты прав. Надо больше писать всяких доказательств, брошюр, книжек, чтобы это было доступно большему количеству людей, в разных форматах, а не только "от человеку к человеку".
Узнал из чатика, где обсуждают теорию типов.
Сохацкий активно HoTT пропагандирует.
ну что, ушёл с седовласыми старцами на кафедру советоваться?
> Я не могу представить себе здорового человека, которого всерьёз волнует, верен тот или иной математический результат или нет.
Ну что это такое?
ну ты прав, основания имеют такое же отношения к математике, как обсуждение интерпретаций квантовой механики к починке сан. узла, никакое то есть
он имел в виду, проверять, верен ли доказанный кем-то результат, который проверен "авторитетами", с существующим консенсусом...
Сомнительное утверждение, так как твоё понимание может отличаться от объективной реальности. Игра в рулетку тут. Верификация позволяет нивелировать подобные неточности. (у многих серьёзных результатов есть набор неэквивалентных формулировок)
Нет, я имел в виду, что "факт" истинности или ложности того или иного математического утверждения сам по себе не имеет ни ценности, ни смысла. Допустим, гипотеза Римана верна или не верна --- какая разница? Тебе лично не плевать?
Любое утверждение можно принять в качестве аксиомы, т.е. сделать его верным или неверным по своему желанию.
Слишком большой фокус на "да/нет" аспектах --- это аберрация , являющаяся следствием принятой сейчас системы преподавания, а не какой-то глубокий факт.
Противопоставляя компьютерную верификацию "работе по старинке", многие подменяют первичную ценность вторичной.
Хотя, если считать компьютер продолжением мозга, то всё нормально. Но это получается киборг, а не человек.
>>68058
Я не он, если что.
> Нет, я имел в виду, что "факт" истинности или ложности того или иного математического утверждения сам по себе не имеет ни ценности, ни смысла.
Математике это по своей сути точное знание. На голландском буквально - wiskunde. Факт истинности или ложности утверждения это сама суть математики, вне которого ее просто нет. Отсюда и проблема оснований - что именно считать истинностью в математике.
> Допустим, гипотеза Римана верна или не верна --- какая разница? Тебе лично не плевать?
То что ты описываешь - уровень пикрелейтед.
>На голландском буквально - wiskunde.
А на ацтекском - Tlapōhualmatiliztli.
Гипотеза Римана не интересна по той причине, что существуют десятки эквивалетных ей утверждений и все эти утверждения формулируются очень просто; утверждения же, которые вытекают из гипотезы Римана обычно очень сложные и содержат в формулировке пространства Харди и прочее.
Отсюда понятно, что гипотезу Римана следовало бы принять за аксиому (аксиомы это, среди прочего, простые утверждения имеющие многочисленные сложные следствия).
Ну а кроме того, гипотеза Римана уже доказана Делинем в 1974-м еще.
>Ну а кроме того, гипотеза Римана уже доказана Делинем в 1974-м еще.
Жаль что кроме тебя этого никто не знает.
>что гипотезу Римана следовало бы принять за аксиому
Верую, ибо блаженен.
>Верую, ибо блаженен.
Я могу сказать про тебя то же самое, ты похоже веруешь в объективные истины из мира идей или откуда еще, и считаешь что математикам принципиально важно знать истинно ли данное утверждение в абсолютном смысле, или нет. Из разряда новостей в популярных журналах типа "ALL MATH MAY BE WRONG, Researcher said".
Но на самом деле это абсолютно не важно, важны утверждения, вытекающие из гипотезы Римана, и полученные с их помощью результаты, а не сама эта сраная гипотеза. И если вдруг окажется, что эта гипотеза не верна в общем смысле, ценности полученных результатов это никак не отменит. Тем более, что она уже верна в важнейших частных случаях, что уже доказано.
Люди, всерьез интересующиеся основаниями, это люди которые не понимают что такое вообще математика, где и зачем она нужна. Математика это не каталогизация объективных истин из мира идей и не искусство выводить произвольные следствия из этих истин.
Специалисты по основаниям это плутонисты, верующие в вычислимость и занимающиеся абстрактной хуйней не имеющей приложений. Когомологии, схемная алгебраическая геометрия, К-теория и т.д. имеют гигантское количество приложений, Делинь, Гротендик, Артин, Мамфорд и прочие действительно ближе к сантехникам, как тут выразились, чем к фуфлософам-пиздаболам с их объективными истинами, трансцендентальными единствами, тезисами Черта и проч.
>>68121
> Когомологии, схемная алгебраическая геометрия, К-теория и т.д. имеют гигантское количество приложений, Делинь, Гротендик, Артин, Мамфорд и прочие действительно ближе к сантехникам, как тут выразились, чем к фуфлософам-пиздаболам с их объективными истинами, трансцендентальными единствами, тезисами Черта и проч.
Пынямаешь ли, все что ты перечислил, вовсе не висит где-то в пустоте. Это следствия развития математической мысли, следствия, к которым привели даже не столетия эволюции самых разных математических и не только идей, методов итд. И тот подход, который ты вычитал у Вербицкого, он в точности соответствует пикрелейтед номеру "тут играем, тут не играем, тут вообще рыбу заворачивали". И.е предлагается что-то сыграть не только в отрыве от всего контекста, но и принципиально игнорировать вопрос, откуда все это вообще пошло и в чем природа всего этого. В принципе, такой подход имеет право на существование, но с определенными оговорками, которые ваша секта принципиально не принимает. Практическая применимость чего-то как критерий истины это хорошо и правильно, но принимать это не как функциональный контекстуализм, а как нечто висящее в воздухе и данное нам непонятно кем и нахуя, это сектантство.
>Факт истинности или ложности утверждения это сама суть математики, вне которого ее просто нет.
Вообще-то это ниоткуда не следует.
Сами по себе понятия истинности и ложности могут оказаться не совсем тем, что надо ставить в основания.
Т.е. настоящие основания должны основываться на каких-то других концепциях (каких --- не знаю), а понятия "истинности" и "ложности" --- выводиться из них. Грубо говоря.
>То что ты описываешь - уровень пикрелейтед.
Наполовину прикалываюсь, наполовину серьёзен.
Возможно, если математик начнёт серьёзно рефлексировать, изучать свои мысли и побуждения, то что-то из этого он сможет извлечь.
>>68121
>Люди, всерьез интересующиеся основаниями, это люди которые не понимают что такое вообще математика, где и зачем она нужна.
Громкое заявление.
А слова о фуфлософии и оскорбительные, и смешные. От любителя "схемной алгебраической геометрии", у которой приложений в жизни... сколько? Для любого нормального человека ты сам пиздабол.
>функциональный контекстуализм
охуенно, прямо как у Гермиды и Якобса, синоним декартовой замкнутости
а напомните нам нахуя нам 87-я гомотопическая группа трехмерной сферы ?
> фуфлософам-пиздаболам
Погоди-ка. Это что-же получается, "пыняпучк" юродидый с /math/ и "философсмолин" пиздобол с /sci/ - одна и та-же личность? Кто бы мог подумать?
1) не надо смешивать а) верификацию, как стремление к абсолютной строгости доказательств вместе с б) радикальным интуиционизмом/конструктивизмом. Поверифицировать можно отлично и классические доказательства.
2) я присоединяюсь к требованию обоснования изучения алгебраической геометрии, гиперкелеровых многообразий, пучков и прочего. Покажите покупателей! Пруф или не было!
Пучки нужны даже палочкосчитателям и N-петухам для построение пресловутого функционального контекстуализма, у них там современная теория типов на предпучках строится и есть расширенная теории типов, где вместо категории множеств берутся категории групоидов, и таким образом переходят в престек теорию типов, где вместо сигмы конструкция Гротендика. Те еще наркоманы.
Я за модульного деда если что, но мне кажется, что вы тут попутали понятия верификации и нормализации. Вот скажем вы можете верифицировать свои группы сфер (если построите конечно, а то выше четвертой группы никто не построил еще даже для первых трех измерений), но нормализовать терм уже не сможете, нужно изобретать механизмы оптимальной редукции, новая открытая проблема). А так когомологии элиптические, циклические, хуические, этальные, халяльные — все это изи чекается уже пару лет как. Этальные кстати если записать в HoTT будут самыми красивыми.
> Пучки нужны даже палочкосчитателям и N-петухам для построение пресловутого функционального контекстуализма, у
Зачем? Все это прекрасно строится без всяких пучков.
> А так когомологии элиптические, циклические, хуические, этальные, халяльные — все это изи чекается уже пару лет как. Этальные кстати если записать в HoTT будут самыми красивыми.
Все дело в том, что при желании это все работает в обеих направлениях. Гамалогии можно представить в HoTT, а можно и наоборот. Всяческие вербитодрочеры веруют только во швятые гамалогии, а все остальное в их религии даже не математика. Тогда как на самом деле все сложнее. И HoTT и гамалогии, и много чего другого - это просто языки, вторичные по отношению к собственно математическому мышлению. Потому что если это не принимать, тогда придется принять, что вся математика существует только на бумаге, а роль человека - трясти синтаксис. Либо остаётся совсем уж религия - платоновский мир идей, актуальная бесконечность, исключенное третье и прочие подобные догмы, заповеди. Можно скатиться ещё дальше, до высказываний Манина о том что "математика подвешена в воздухе". Но это уже уровень патриота, который сидя за американским компьютером с американским по, пишет в американском интернете, какие пиндосы пидоры.
>Зачем? Все это прекрасно строится без всяких пучков.
Строится без пучков, но с пучками выглядит компактнее. Там много изоморфизомов моделей теории типов: Категории с семействами (CwF), категории с аттрибутами (CwA), Воеводский делал С-системы, потом поняли, что это все поебота, выдуманная людьми и перешли на гротендиковский пучкизм в французском стиле. Кубическая теория типов стала записываться одной формулой: I: <sup>op</sup> → Set. Пи и сигма тоже в пучках формулируется, как функториальная смена базы, вернулись к Лавировской классике.
Это хорошо, что пока только модульный дед атакует, а придут спросят как Стекс Проджект закодировать и что мы будем делать, мычать? Нет, мы готовы уже модальную престек теорию типов предоставить на конструкциях Гротендика --- такая основная мотивация пучкизма в теории типов, ублажить высших сантехников и более консистетно подойти к основаниям, чтобы они могли все в себя вобрать.
>Все дело в том, что при желании это все работает в обеих направлениях.
нихуя не работает. Пока что выходит лишь записать тривиальные результаты 50-60х, при этом 90% времени тратится на формализмы, вместо математики. Приход программистов в математику ничего хорошего не дал в итоге, вместо решения реальных задач бесконечные новые формализмы.
>От любителя "схемной алгебраической геометрии", у которой приложений в жизни... сколько?
ну тупые, не знали, что надо очередной модный фреймворк оснований учить
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
в каком то смысле это хорошо, потому что тогда математика сводится к медалистам Филдса. Математики могут успокоится, задача программистов не забирать их медали, а провести рефакторинг всей математики, очень неблагодарная но интересная деятельность. Задача оснований --- строить эффективные вычислительные модели или предлагать новые специализированные синтаксисы для каждого вида математик.
> задача программистов не забирать их медали, а провести рефакторинг всей математики
Нельзя провести "рефакторинг" не зная что ты собственно рефакторишь. А уровень знания математики у программистов нулевой.
Ну когда я говорю программисты я подразумеваю Воеводского. А ты очевидно подразумеваешь своего студента имбецила, который сайт кампуса на ПХП пишет.
> А ты очевидно подразумеваешь своего студента имбецила, который сайт кампуса на ПХП пишет.
Речь скорее о ncatlab, о любителях пруверов и функционального программирования. Воеводский был жемчужиной среди всего этого сброда, с реальными математическими результатами в прошлом.
> приложений в жизни
> two-dimensional exactly solvable statistical lattice models and its related Hamiltonians
Тебя спросили про приложение алгебраической геометрии в жизни, а ты приводишь статью на википедию, где перечислено программное обеспечение, интересно. Не хочешь задуматься, почему медалист Филдса пересел за комп?
ncatlab и ведется студентами, я сам плачу студентам за статьи на ncatlab, это студенческий образовательный проект. Ты воюешь с ветряными мельницами.
Воеводский был жемчужиной, а прувер написать не смог. Зато медаль получил, за пофиксаного Блоха-Като, рефакторер блядь. С-системы его ёбнутые. Ты реально переоцениваешь математиков.
Уайлс за комп не пересел, до сих пор на бумажке считает. Или ты про того, который стал с шумом радио общаться?
Нет, я ж не атакую, я ж признал, что нового не умеем производить, все что можем --- это по крупицам собирать то, что математики напридумывали используя их же методы, языки и модели. Вот и все. Да имбицильство, но оно качает, и тенуре нам не нада.
> Нельзя провести "рефакторинг" не зная что ты собственно рефакторишь. А уровень знания математики у программистов нулевой.\t
Ага, а математика это согласно вашим сектантстким заповедям что?
>Ага, а математика это согласно вашим сектантстким заповедям что?
Я не очень понимаю, на что постоянно погромисты обижаются. Ну вот Многие дисциплины просачиваются в другие области будь то humanities или естественнонаучные или инженерные, это нормально. Но глупо полагать, что в 21м веке ты можешь достичь хорошего понимания современных достижений в нескольких дисциплинах.
SVD, численное решение урчп, градиентные спуски, 3Д моделирование и кватернионы, Монте-Карло, FFT, поиск группы автоморфизмов для решения какой-нибудь хитровыебанной задачи из линейной оптимизации - это не современная математика. Это всё важные вещи, они могут часто использоваться, они полезны. Но с точки зрения математики этим идеям лет 200 минимум.
Весьма вероятно, что большинство программистов выше перечисленные вещи имплементировать не сможет и прекрасно обходится куда более простыми математическими операциями. И это нормально. Ну какой-нибудь 0.00001% прикладных математиков перекочует в топологический дата саенс, это делает их программистами?
Это не какая-то профессиональная спесь. Просто в "простонародье" математикой и матаном называют всё, что сложнее обычного умножения. Если же мы говорим про пруверы и соответсвенно теоремы, то есть совершенно чёткая область чистой математики. Порог вхождения в современную актуальную чистую математику настолько высокий, что 99.9999% программистам дорога туда заказана.
Поэтому все громкие утверждения насчёт важности пруверов серьёзно просто не воспринимаются из-за совершенной некомпетентности собеседников. Это уровень ферматистов и навьестоксеров.
> есть совершенно чёткая область чистой математики.
Которая точно так же, как и любая другая, представима в HoTT. Ничего волшебного в чистых гамалогиях нет. Но, с точки зрения сектанта, писать гамалогии в прувере, а не на бумаге - это пиздец харам и неко мпетентность. Почему? Да вот потомучто.
золотые слова
единственное что дополню -- может быть верификация -- это способ изучения математики для тех, кому не повезло оказаться в нужной среде в нужное время? Это я типа про себя...
Да и к тому же -- это благородное дело, если кто-то что-то хорошо верифицировал -- изучить другому человеку это очень просто.
Да, С-системы Воеводского нужны были для модели его теории типов. Но она вроде сильно специализированная какая-то, конструктивая в каком-то смысле. А это значит, что классическую математику в ней не подоказываешь. (Ну может есть какой-то хитрый способ?) Ае сли не подаказываешь, то тогда разве это "основания математики"? Получается, что нет. Или что с точки зрения адептов hott, настоящей(тм) алгебре "не нужна" аксиома выбора? Все учебники переписывать? На конечных объектах -- может быть, ну а если чуть сложнее что...
я человек простой: слышу про математику и деньги -- пишу свою фейкотелегу: puchkist
А что такое современная математика, и можно ли ее где-нибудь применить? Или она такая ЧИСТАЯ, что нигде не применяется?
> классическую математику в ней не подоказываешь. (Ну может есть какой-то хитрый способ?
Способ ровно тот же самый, что и в классической математике - без задней мысли берешь и прописываешь нужную заповедь. И о чудо, можно её использовать для "доказательства".
>Да, С-системы Воеводского нужны были для модели его теории типов. Но она вроде сильно специализированная какая-то, конструктивая в каком-то смысле.
С-системы точно такая же копипаста как и CwF, CwA, только Воеводсткий использовал категории, объекты которых индексированые натуральными числами. В те времена еще не было модальной HoTT поэтому теории связанных топосов Ловира еще не было в пруверах, поэтому ясно что что в С-системах этальная математика не чекается. C-системы это изоморфизм universe categories.
Нет никакой его теории типов. Есть теория типов и в рамках ее DIY модели, все равноправные. Кто больше математики в своих моделях закодирует тот и победил, это и будет показателем эффективности испольования прувера.
С-системы как и все основание построенное Воеводским просто зажигало ребят вокруг за это ему спасибо, а так же теорию типов для своей же унивалентности Воеводский построить не смог. Построили программисты, так что спесь не то что с модульного деда, но и с лауреатов Филдса можно сбить при желании.
> теорию типов для своей же унивалентности Воеводский построить не смог. Построили программисты, так что спесь не то что с модульного деда, но и с лауреатов Филдса можно сбить при желании.
Мне меньше всего понятно, почему эти вещи вообще противопоставляются. Вот если отбросить сектантскую швятую веру уровня того, что креститься нужно не тремя, а двумя пальцами писать нужно на бумаге, а не в прувере, то какие аргументы остаются против HoTT?
насколько я помню, если прописать аксиому выбора -- получишь противоречие с аксиомой унивалентности.
Аргумент против HoTT см выше, для неё надо передоказывать все теоремы и неизвестно, содержится ли в ней модель ZFC.
Тогда чекаться будет любая теорема, что неинтересно. Ex falso quodlibet
Сейчас пруверы - бесполезное говно для 1,5 аутистов. Но если дать всей этой теме ход, то сразу появятся кабанчики, которые сверстают "нормальный прувер" и попросят бабки за его использование. Это подтолкнет журналы не принимать пруфы не заапрувленный пруверов от ООО Кабанчик Инт. Ну а дальше смерть и вырождение математики.
Это очень оптимистичная программа, но я бы под ней подписался!
В классической математике это никого не останавливает почему-то.
>>68206
Вот честно, бред какой-то уровня "аргументов" керосиновых магнатов против елестрического освещения.
>Вот честно, бред какой-то уровня "аргументов" керосиновых магнатов против елестрического освещения.
Компьютиризация убивает искусство. И да компьютер есть и всегда будет беспросветно тупым.
>гамалогиях
Кроме этого слова больше ничего про "современную" математику не знаешь? Идее гомологий уже больше ста лет, а Э-С аксиомам уже лет так 70. Гомологии проходят на первых курсах, если что.
Вот классический пример - не знаю, о чём говорю, но буду прятаться за мемами вроде пучков и гамалогий, авось проканает и это поднимет авторитетность моего программистского мнения. Ну с этим иди в /sci/.
Ты ж сам видишь, что по существу того поста не возразил. А все "аргументы" против свелись к >>68209
Ты думаешь взяв "аргументы" в кавычки ты снизишь их значимость? Ну так, мой дорогой, в таком случае твои "аргументы" говно из жопы, как тебе такое?
Значимость чего? Рандомных, ни на чём не основанных заявлений, что типа "буковы в прувере в отличие от таких же буков на бумаге - это не искусство"? Так у подобных заявлений и так никакой значимости нет, как я могу ее дальше снизить?
Давай, если такой умный, строго докажи, что ZFC противоречива, верифицируй в любом прувере: гарантировано получишь премию Абеля.
Ну либо противоречива, либо нет. Ты ж не против использования исключенного третьего в доказательстве? Тогда я считай доказал.
>Ты ж сам видишь, что по существу того поста не возразил
Хорошо, давай по существу. Раз ты у нас охуенно какой математик, то тебе ничего не стоит отвечать по существу, верно? Так что я ожидаю развёрнутых ответов с пруфцами, а не балабольство и демагогию. Это всё-таки /math/, а не /pr/.
Хорошо известно, что вокруг доказательства гипотезы Пуанкаре было немало драмы из-за сказанного/напечатанного Яу, Цао, и Джу. В частности, они намекали, что доказательство Перельмана не полное. Позже это утверждали и другие (статья Моргана-Тяня, книга Бахри).
1) Могут ли пруверы (существующие на сегодняшний день) показать (однозначно), были ли пробелы в доказательстве? Как/почему нет?
2) В первой архивной статье Перельмана на эту тему он получает неравенства типа Гарнака, интегрируя неравенство Ли-Яу, и в получившихся геометриях (точнее, в одной оптимальной) считает геодезические.
Вопрос - могут ли пруверы показать, какие из этих результатов (в частности, аналог теоремы Бишопа-Громова) уже автоматически следовали из статьи Ли-Яу? Как/почему нет?
2) Могут ли пруверы показать, есть ли пробелы во второй архивной статье Перельмана, а именно в исследовании поведения решений для времени много большего времени "хирургии"? Как/почему нет?
3) Могут ли пруверы показать, корректно ли доказательство конечности времени вымирания (вторая статья)? Как/почему нет?
4) Могут ли пруверы выявить неэквивалентные утверждения между статьями Перельмана и Цао-Джу (особенно раздел 7.6 последней, включая результат о поведении потоков Риччи с хирургией на бесконечности)? Как/почему нет?
Жду демагогию, односложные ответы, мемы, шутейки, и увиливания.
Нужно нейронку, которая могла бы челотекст переводить в нагромождение логической поебени и потом уже этот километр текста скармливать пруфчекеру.
Вольфрам знает математику еще меньше чем основатели, а теорию языков программирования вообще не знает.
Ага, это сразу видно по бюджетам в области искусства и компьютерной графики.
я не он, но отвечу тебе, раз уж ты такую пасту напечатал.
Всё, что может быть доказано, может быть доказано как "на бумаге", так и на компьютере. Я сам и так, и так спокойно доказываю.
Все "драмы" -- чисто социальное явление, не относящееся к математике.
Мы говорим о пруверах, а имеем в виду "пруф ассистанты", они сами ничего сдожного не доказывают. Ты пишешь доказательство, а они проверяют, не ошибся ли ты.
Поэтому на вопрос "могут ли" ответ: да. Тебе придётся долго писать пруф, но в итоге , если твои интуитивнве рассуждения верны, то получится
Да модульному деду уже преподали теорию типов на пучках и конструкциях Гротендика, если это не помогло, то остальное вряд ли поможет.
Пусть подоказывают еще 100 лет на бумажке, а дальше будет без вариантов :-)
>Ты пишешь доказательство, а они проверяют, не ошибся ли ты.
Тут есть одна эмпирическая гипотеза: доказательство любой достойной теоремы невозможно записать в прувере. Только тривиальные вещи 19 века и всякую комбинаторику. На данный момент за 40 и более лет компьютерных доказательств исключений не было.
Это правда, но уже лучше чем Principia Mathematica, согласись!
> Тут есть одна эмпирическая гипотеза: доказательство любой достойной теоремы невозможно записать в прувере.
Почему на бумаге можно?
потому, что интересно только модульному деду, а он видимо не филдсовский медалист.
тут хуй пойми, что он имеет ввиду под математикой: создание вычислительных практичных теорий для народного хозяйства, доказательство больших теорем, нахождение изоморфизмов, рефакторинг математики, упрощение, педагогика, создание новых дисциплин, просто медальки выдаваемые тайным обществом непонятно. Понятно только, что на бумаге главное, чтоб было ОК АРНОЛЬД
Написать программу, которая сгенерирует статью по С-системам Воеводского в TeX из исходников и автоматически пошлет в журнал можно уже. А это, очевидно, настоящая математика, ее же чувак с медальками писал!
тоже не понимаю этого ad hominem, есть международная классификация математики, её и держитесь
>Тебе придётся долго писать пруф
Долго это порядка времени возврата Пуанкаре?
Всё doable, просто математикам быстро надоедает пруф-терм дописывать, да и программисты быстро бросают. Нужны репрессии.
Ну да выгнать всех программистов нахуй. А за упоминание cs major расстреливать из зенитки.
лол, как анон и предсказывал, он получил односложный ответ "да" без реальных пруфов и пояснений как и что
собственно, что и требовалось доказать, погромисты в реальной математике не шарят и по теме разговаривать не могут
>>68231
на этой доске всего 2.5 анона, которую даже второкурсный дифгем осилили, куда уж там потоки риччи
hottоёбы почитали определения категории и гомологии и теперь думают, что они "шарят"
не удивительно, что вербит перестал сюда заходить
> не удивительно, что вербит перестал сюда заходить
Так это всё-таки он был, форсил тут свою единственно верную религию, лол. Нет в математике боженьки кроме вербита, а модульный дед (поел говна на обед) - пророк его.
> лол, как анон и предсказывал, он получил односложный ответ "да"
> Вопросы, однозначно подразумевающие односложные ответы
> ответили односложно
> ррреее, я жи говорил
Что вы за люди, пиздец...
>> Вопросы, однозначно подразумевающие односложные ответы
Ну тогда это на уровне религии, так что пиздуйте со своими пруверами на другие доски.
> Ну тогда это на уровне религии
Что на уровне религии, рабочие программы? Братишка, чёт ты с горя совсем хуйню понес.
>> Вопросы, однозначно подразумевающие односложные ответы
>> ответили односложно
Так а зачем тогда было говорить, что, мол, анон по существу не ответил? А как только поступили вопросы по существу - оказывается, что это секта и по существу-то никто и отвечать не может, потому что программисты ничего не знают ни о дифференциальной геометрии, ни о пруверах.
> как только поступили вопросы по существу
Вопросов по существу не поступало. На вопросы модульного деда (да поест он говна на обед) уже много лет есть однозначный ответ - да, ничего волшебного на бумаге нет, все то же самое можно делать в прувере. Он же с позиции своей швятой веры утверждает, что это не так. Зачем-то даже в очередной раз создал подобный тред.
>можно делать в прувере
Так почему никто не делает? Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее. Представляю список теорем прошлого и позапрошлого века, которых никто не может набрать в прувере:
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
>Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее.
Двачую, математика это прежде всего язык, все стремятся к ёмкости понятий, чтобы какую-нибудь сложную хуйню можно было выразить небольшим количеством символов, а тут всё наоборот.
> Так почему никто не делает?
Справедливости ради, таки делают. Просто ты как обычно не в теме https://github.com/UniMath/UniMath например, ещё Воеводского проект, до сих пор развивается.
> Выглядит так, что способ записи настолько тупой и сложный, что никто не может осилить хоть что-то стоящее.
В той же агде юникод поддерживается, всю нотацию можно переопределить как самому удобно и угодно. Насчёт неосиляторов соглашусь, там мозги нужны. Про лемму Йонеды не смешил бы тапки, она в хаскелле-то давным-давно есть.
>Про лемму Йонеды не смешил бы тапки, она в хаскелле-то давным-давно есть.
Лол, ты про частный случай? Тащи пруф в нормальной математической формулировке.
>Справедливости ради, таки делают. Просто ты как обычно не в теме https://github.com/UniMath/UniMath
опять ссылка на гитхаб с непойми чем и клеймо покойного Воеводского, будто он из рая дописывает. Присылай конкретные значимые теоремы из 20 века, тогда поговорим.
> гранаты формулировка у них не той системы
> ваш гитхаб не гитхаб, там буквы какие-то непонятные
Ясно.
> Присылай конкретные значимые теоремы из 20 века, тогда поговорим.
Значимые для кого? Вашей секты?
>Ясно.
Хуясно. Притащи для начала формулировку категории на хаскелле.
>Значимые для кого? Вашей секты?
Для математических предметов за первый и второй курс. Теорема о нулях, теорема стокса, теорема коши из ткфп...
> лемму Йонеды
> пруф в нормальной математической формулировке.
можно статью или скрин тайной леммы Йонеды?
> в пруверах - настоящие теоремы.
Ну что ты, настоящее ламповое только на бумаге, ровно то же самое на винте - уже не то же самое.
Только есть нюанс, что ошибки на бумаге можно найти. Ошибки в пруверах ты будешь искать намного медленней.
HoTT делалась для автоматизации теории гомотопий или алгебраической топологии, а не для алгебраической геометрии. Для непосредственного управления вараятис нужно ввести в ядро вместо гомотопического интервала [0,1], афинный отрезок А^1 и это уже будет называться А^1-теория гомотопий. Т.е. если ты скажем хочешь Блоха-Като доказать, то тебе сначала нужно перейти в правильную систему типов для этого.
Ну это любой студент на агде выкладывает на гитхабе. Тут же ничего не нужно кроме теорката и построенной категории множеств. То, что в Хаскеле просто стертый терм до System F, хаскель-доказательство в качестве школьной программы можно защитать. В этом смысле это же можно доказать даже в NuPRL и старых пруверах.
> Ошибки в пруверах ты будешь искать намного медленней.
Ошибки прувер сам найдет
На 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))
>Gödel's Completeness Theorem
Вот тут какой-то студент на Агде написал Gödel's Completeness Theorem
https://mathoverflow.net/questions/272982/how-do-we-construct-the-g%C3%B6del-s-sentence-in-martin-l%C3%B6f-type-theory
>Classification of Finite Simple Groups
сразу видно воинственного неадеквата
особенно смешно то, что единственное полное доказательство этой теоремы существует только на компьютере :-)
так и другие доказательства на компьютере, но не в прувере.
>Ошибки прувер сам найдет
>Вера в всемогущий безошибочный компьютер
О как это знакомо.
Пруферы гомотопические, а классификация простых конечных групп конструктивна?
>а напомните нам нахуя нам 87-я гомотопическая группа трехмерной сферы ?
У МЕНЯ ЗА ТАКИЕ ВОПРОСЫ В ХАРВАРДЕ УБИВАЮТ НАХУЙ ПУЧК ГРОТ СТАТЬИ ПИСАТЬ НАДО ПОВТОРЯЮ ПОВТОРЯЮ СТАТЬЯ ПО 87-тую ГРУППУ ТРЁХМЕРНОЙ СФЕРЫ НЕ ТОЖЕ САМОЕ ЧТО СТАТЬЯ ПОСВЯЩЕННАЯ ОДНОМУ КОНКРЕТНОМУ-НМУ ИНТРЕГАЛУ ПУУЧК ГРООТ ДИДИ ИЗ МГУ ПИШУТ ПРО ИНТЕГРАЛЫ СТАТЬИ И НЕ СТЫДНО КАК В НИГЕРИИ БУДЕМ ГРОООТ
Лол блядь
Тут погромисты походу ни математики, ни программирования не знают
Тайпчекинг, кек
Весь тред это один большой COPE второкурсников с CS
Опять пук в лужу и швятая вера, что на бумаге можно сделать больше чем в прувере.
Это классическая проблема детей верующих в всезнающий всемогущий комплюктер. В силу того, что они в этой жизни еще нихуя не сделали, они не понимают, что такого не так в их вере.
Воеводский безусловно был первоклассным математиком, но своими унивалентыми основаниями он открыл дорогу всякому cs сброду дорогу туда, где ему быть никогда не следовало.
>швятая вера
Ну вас шизиков напрямую спросили - покажите, как работает на примере любой из фундаментальных теорем 20го века, например теорема об индексе
Кто-то настрочил про гипотезу Пуанкаре, тоже тишина в ответ, неловкое "ну да, это можно..."
Пока что это выглядит как религия. Когда меня не аргументами убеждают, а просят поверить - интерес сразу пропадает. Может, поэтому в этой области нормальных математиков нет, и привлекает она одних только горе-питонистов.
> Пока что это выглядит как религия. Когда меня не аргументами убеждают, а просят поверить - интерес сразу пропадает.
Кому ты нужен, в чем-то тебя убеждать? И где и кто тебя просит поверить? Сам на протяжении нескольких лет создаёшь эти треды, сам потом в них горишь. Зачем? Веруешь во швятую бумагу и бездушные кудахтеры - веруй, свободу вероисповедания не отменяли.
Тебе кажется, что в топовых пруверах не настоящие теоремы, просто потому что ты пока мало знаешь используемую в них математику. Я тоже раньше не знал и поэтому сомневался.
>Тебе кажется, что в топовых пруверах не настоящие теоремы
Да тут нечему казаться - привели пример реальных, настоящих, теорем. Ответа по существу (как тут любит один) - не было. Я вот знаю математику, используемую в гипотезе Тёрстона или той же теореме Атьи-Зингера (не зря заканчивал, теперь могу щитпостить на двоще). Ну так и где они в пруверах? Или моего уровня недостаточно?
Я видел десятки академиков которые печатаются в АлгТопе но не могут на компьютере Пифагора записать и что? Там другая математика, и практика нужна.
Если программа написанная на сертифицированном прувере или языке, то любая программа в нём является валидным термом в топосе. Тотальное избавление от ошибок и переход в кванторы --- это и есть главная мотивация бездушевной математики.
Прости, я еще хотел поинтересоваться, а Квиленновские Модельные Категории, Модельные Структуры и Гомотопические Категории --- это как, настоящая математика для модульного деда или нет?
>Для математических предметов за первый и второй курс.
Я думаю такие вещи в пруверах точно можно записать, просто он скорее всего не знает математики даже на таком уровне.
Отвратитетельная на значит бесполезная, говно тоже чистить нужно, но неприятно, так и тут, они бы с большим удовольствием перекинули это на кого-нибудь другого.
>А кому-то мастурбация помогает понять материал, мы будем на основе этого делать выводы насчёт её роли в современной математике?
И найти решение тоже помогает.
как минимум лемма Йонеды и теорема Гёделя верифицированы.
Это не модульный дед создал тред, это я, просто гораздо лучше было бы, если бы классические основания математики были такими вирусными. Верифицировать долго, но реально: и чем дальше, тем быстрее получается
>>68310
там про неполноту речь, она верифицирована много где
полнота кстати попроще и тоже верифицирована в разных системах.
На всякий случай, я лично не люблю ни программировать, ни делать тяжеловесных выкладок (и, слава Аллаху, в той математике которой я занимаюсь можно обойтись без обоих). Но если сравнивать такие активности и речь идет о выкладках которые настолько механическая и трудоемкая ерунда, что их рационально автоматизировать, то запрограммировать эту автоматизацию явно привлекательнее.
> Это не модульный дед создал тред, это я
Ну короче есть ГОТТ. Гомотопическая теория типов. А дальше на вики всё написано.
https://ru.wikipedia.org/wiki/%D0%93%D0%BE%D0%BC%D0%BE%D1%82%D0%BE%D0%BF%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D1%82%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D1%82%D0%B8%D0%BF%D0%BE%D0%B2
Перевод: сам я нихуя не понимаю, потому что ещё учусь (на погромиста), но звучит очень понтово.
>А ну говори, каким Браузером пользуешься.
Каким-каким, интуиционистским - Brouwer: "On the significance of the principle of excluded middle in mathematics, especially in function theory."
2) потом решили, что лучше брать за основу множества, так как натуральные числа можно определить в теории множеств как вторичные объекты, а наоборот нельзя
3) потом пришёл Рассел и всё решил свести к формальной логике - так появилась первая теория типов
«Тот факт, что вся математика есть не что иное, как символическая логика, — величайшее открытие нашего века».
4) потом математики поняли, что типы первичны над логикой. На самом деле фактически это показал тот же Рассел, но он не понял этого, полагая первичной логику.
5) работа Бурбаки описывает всё через порождающие структуры http://inponomarev.ru/teaching/speciesofstructures - вот тут по ссылке учебный курс по теории множеств и по структурам Бурбаки. Порождающие структуры по Бурбаки - это по сути типы аксиом. Некоторое среднее решение вопроса о первичности между теорией типов и логикой. При этом в своём роде окончательное - не вдаваясь в конкретное содержание, все матобъекты представляют собой структуры Бурбаки.
6) современные направления далее развивают это всё через теорию категорий. Особенно популярной оказалась идея, что первичными объектами являются высшие категории. Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.
7) самое современное слово в этой науке - гомологическая теория типов. Согласно ей, первичны не множества, ни логика, ни типы, ни структуры - первичны гомотопии. Кратко можно проследить это так:
из натуральных чисел конструируется что угодно ->
сами натуральные числа естественно появляются в теории множеств как кардиналы и ординалы конечных множеств ->
теория множеств строго может быть построена только аксиоматически и через структуры (теория топосов так возникла, но её считают частью теории множеств - просто топос "множество" один из многих топосов)
-> в конечном счёте всё это - символическая логика, при этом Рассел понял это намного раньше создания теории топосов и работ Бурбаки
-> символическая логика описывается семантикой, значит первичнее семантика (отсюда в том числе лингвистический поворот в философии)
-> дальнейший анализ показывает соотношение семантики и математики - семантика шире математики, математика же есть анализ симметрий семантики
-> все виды симметрий семантики могут быть обобщены как высшие группоиды, а высшие группоиды полностью эквиваленты гомологическим типам
-> значит, гомотопии первичнее
-> изоморфизм Карри-Ховарда показывает. что любое доказательство эквивалентно программе, а значит логические системы, типы и формальные исчисления, логики - это одно и то же, только описанное разными способами
-> на основе этого изоморфизма можно создать гомологическую теорию типов, которая описывает любой математический объект на основе "истинно фундаментальных" - симметрий семантик.
>https://inponomarev.ru/burb
не дай бог такому зачет сдавать
> Это уже не противоречит Бурбаки - все эти категории могут быть классифицированы его структурами.
это интересно, в какой книжке бурбаки можно прочитать про категории?
Topologie algébrique. Chapitres 1 à 4.
Написана посмертно с того света и впервые издана в 2016.
А я люблю обмазываться современным категорным калом и дрочить. Каждый день я хожу по доске с черным мешком для мусора и собераю в него весь категорный кал, который вижу. На два полных мешка целый день уходит. Зато, когда после тяжёлого дня я прихожу домой, иду в тред для начинающих, говорю новичкам, что их математика не математика…ммм и измазываю тред категориями. И дрочу, представляя, что меня поглотила единая категория. Мне вообще кажется, что категории, умеют думать, у них есть свои семьи, города, чувства, не смывайте их в унитаз, лучше приютите у себя, говорите с ними, ласкайте их…. А вчера в ванной, мне преснился чудный сон, как будто я нырнул в море, и оно прератилось в копредел, функторы, кольца, поля, все из говна, даже первая культура, даже Аллах!.
(типичные размышления деда с dxdy о современной математике)
Потому что математика, а не программирование.
Как там пруверы, уже хотя бы теоремы ХХ века вроде теоремы об индексе могут доказать?
Так программы тоже раньше на листочке писали, но потом поняли, что так ошибки могут появится. Так и с теоремами, тем более учитывая изоморфизм Карри-Говарда однозначно связывающий математику и программирование.
Базу теорем же люди введут, при том более профессиональные, так что риск ошибки из-за человеческого фактора понижается. А на листочке что? Даже не проверит толком никто.
а) В пруверах ничего внятного и интересно не доказано.
б) Читать пруверские доказательства это просто пиздец, а то что их проверил компилятор не дает никакого приемущества, все и так знают про большинство гипотез верные они или нет. Это то же самое, что музыку играть в миди проигрывателях, можно, если тебе лично это нужно зачем-то.
Потому что тебя, долбоеба, пытаются научить думать. Вероятно зря.
>тем более учитывая изоморфизм Карри-Говарда однозначно связывающий математику и программирование.
Ох лол, даже не знаю, ты просто тролль зелёный или ещё юный и наивный.
На твой изоморфизм всем похую также, как похую, например, на теорему Кэли о группах, которая вроде как и важная, а нигде никогда не применяется, потому что себе дороже.
Ещё раз, где моя теорема об индексе в прувере? Ну раз изоморфизм, то это вообще на раз-два.
>однозначно связывающий математику и программирование.
Только конструктивную её часть, а это 0.00001% от всей математики.
>>74552
>>74555
Ты же сам понимаешь, что твои "аргументы против пруверов" доказывают только то, что те, кто считает себя математиками, в 99 случаев из 100 не могут в пруверы, ибо деревянные по пояс. "Дело было не в бобине", как говорится. Если бы ты понимал, о чем вообще изоморфизм Карри-Говарда, ты бы не нёс такую хуйню. А так, имеем то что имеем...
> те, кто считает себя математиками, в 99 случаев из 100 не могут в пруверы, ибо деревянные по пояс.
Это не голословное утверждение, кстати. Года три ещё назад Сохацкий писал, что ихние академики не могут даже установить HoTT либу в коке. Агду с нужными либами какой-нибудь условный Вербицкий даже установить не осилит, про использование я вообще молчу
> Агду с нужными либами какой-нибудь условный Вербицкий даже установить не осилит, про использование я вообще молчу
Миша вообще в линуксе сидит, насколько я помню
У вас спесь головного мозга в последней стадии, классическое "вы не понимаете, это настолько сложно, что большинство математиков даже не смогут установить, не то что использовать"
Ну и логическая ошибка обобщения, как всегда у программистов
хотт-верунов просят уже который раз показать пример доказательства сколько-нибудь содержательной теоремы вроде теоремы об индексе, а они всё уводят разговор на какую-то нерелевантную солому
"Нет, пока доказать ничего нельзя, но зато УСТАНАВЛИВАТЬ нужно ууууух как сложно, да"
> Миша вообще в линуксе сидит, насколько я помню
Сейчас каждый первый нитакойкаквсе зумер в линуксе сидит.
Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.
> Plugin updates:
> arend-lib can be downloaded and upgraded from the IDE
>>74700
Мой аргумент в том, что плюсы которые дают пруверы сомнительные, а минусы явные и конкретные.
Не нужно их пропагандировать остальным, а нужно желающим (тебе) взять и доказать в них что-нибудь такое убедительное, чтобы все охуели и тогда вопросов бы не было.
>Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.
Никто не спорит, можно и на КОБОЛЕ доказать, только нахуя? Времени это займет много, новизны никакой не будет, а людям жрать что-то надо.
>Если бы ты понимал, о чем вообще изоморфизм Карри-Говарда
Так я понимаю, потому и пишу
>Только конструктивную её часть, а это 0.00001% от всей математики.
>Вообще, смеюсь с твоей веры, что на бамаге можно доказать что-то чего нельзя в прувере.
Ну то есть ни одной вразумительной теоремы современной актуальной математики хотя бы ХХ века, доказанной с помощью прувера образца 2020 года, ты привести не можешь, как и ожидалось.
Так и сказал бы, что ты пустозвон. Пердежу-то на всю доску от тебя.
Если бы понимал, то не писал бы такую хуйню.
>>74712
Когда докажут - ты будешь точно так же кукарекать.
>>74708
> можно и на КОБОЛЕ доказать
Нельзя, он тьюринг-полный, сначала придется прувер на нем писать.
> нахуя? Времени это займет много, новизны никакой не будет
Автоматизация. Что-то простое человек доказать может, что-то посложнее - уже нет. Доказательство чего-то нетривиального в IUTeich человек просто не осилит, никакой. А это ещё не самое сложное.
>Нельзя, он тьюринг-полный, сначала придется прувер на нем писать.
ну да, сначала прувер, а потом доказать, это смешно хоть
>Когда докажут - ты будешь точно так же кукарекать.
Встретимся на этом же месте через сто лет, пока доказали две теоремы, обычные доказательства которых были придуманы в 60-ые. Я не спорю, может быть сейчас разгонятся и все начнут доказывать, микрософт финансирует. Но больше похоже на модную хуйню: денег освоят и забудут.
> больше похоже на модную хуйню: денег освоят и забудут.
Вообще ничем не похоже.
>Когда докажут - ты будешь точно так же кукарекать.
почему до сих пор не доказали?
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
>Если бы понимал, то не писал бы такую хуйню.
Так это ж про тебя, а не про меня.
>Когда докажут - ты будешь точно так же кукарекать.
Нет, если реально докажут что-то, и это будет не ад хок хуита, адаптированная специально для одной единственной теоремы, то я соглашусь, что это круто, и может даже почитаю что-то.
А пока вы все со своими хотт, категориями в хаскеле, и записями лекций в имакс сидите у меня в одной корзине погромистов-второкурсников и лукавых грантопильщиков.
> А пока вы все со своими хотт, категориями в хаскеле, и записями лекций в имакс сидите у меня в одной корзине погромистов-второкурсников и лукавых грантопильщиков.
Это неудивительно, ты ж даже не понимаешь, о чем не только HoTT, но даже тот же изоморфизм Карри-Говарда.
>Это неудивительно, ты ж даже не понимаешь, о чем не только HoTT, но даже тот же изоморфизм Карри-Говарда.
Тут больше одного анона сидит, если что.
Я так понимаю, там принцип как у теорем существования. В случае, если есть доказательство обычное, то существует и на прувере и можно его написать. Последний шаг, разумеется, остается как упражнение для любопытных студентов и пенсионеров.
>>68191
>>68201
>>68203
>>68208
И много других постов от этого мерзкого ублюдка. Граждане математики, обратите внимание, в треде орудует чмо, которое математику не знает, ни одного математического определения не использует, дабы не обосраться(хотя с зфс однажды все же обосрался), и пытается мимикрировать, отвечая односложно в духе "ваша математика - религия, коткудахкудахтахтах ", "почему нет, и что с того" и прочими мусорными способами, уводя дискуссию. Я сам сюда захожу редко, однако сейчас у меня было хорошее настроение, я пил чай, думал над темой магистерской и тут это программистское чмо мне испортило настроение. Посему :
Репортите его, дабы изгнать это чмо.
Всех благ, господа математики.
>Я так понимаю, там принцип как у теорем существования.
Ты вот на это мне ответь, я правильно понимаю ваш езормфизъмъ?
Ну или не он, но сомневаюсь, что есть два таких конструктуха.
Упоротый, даже лекцию прочитал на тему статьи. Конструктухи это клуб фанатиков, я не видел, чтобы какой-нибудь Лури носился по миру и орал "5 шагов принятия высших категорий", "высшие топосы это будущее математики, умоляю, используйте их в доказательстве" итд итп.
Если ты чего-то не видел, это не значит, что этого не было.
было несколько знакомых пациентов лет пять назад, все так или иначе относились к СПбАУ.
На б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льтат или нет.
А что это за бублик на оп пике?
>Воеводский был жемчужиной, а прувер написать не смог.
>Зато медаль получил, за пофиксаного Блоха-Като, рефакторер блядь.
>С-системы его ёбнутые.
>Ты реально переоцениваешь математиков.
Из цитаты видно, что автор (1) триггерится на слово "рефакторинг" и (2) завидует математикам до зубовного скрежета.
"Скажите, как его зовут?" (с)
может кто-нибудь из присутствующих фармакологов объяснить неопытному посетителю чисто для кругозора, к каким наблюдаемым симптомам приводит употребление данного круга веществ? как это могло сказаться на фигуранте обсуждения?
он там про шеня что-то написал, то ли хуесосит а шень няшный, то ли имеет в виду что-то своё, понятное только близким друзьям. Я не понял
А где он про "фигурант данного треда" пишет, я не вижу
тоже темнишь что-то
По первым же ссылкам из гугла описываются симптомы, похожие на то, что рассказывал фигурант
>Наблюдается гиперактивность человека, которая сопровождается странным мышлением и невнятной речью. Наркоман может рассказывать о несуществующих вещах и галлюцинациях. Подобные видения постепенно прогрессируют и превращаются в постоянное явление, тем самым, формируя у человека фобии.
> дезориентированы, испытывают ощущение, что они "находятся в другом измерении", "общаются с Богом", "с дьяволом", переносятся в другие места, слышат какую-то особую "неземную" музыку и пр. Некоторые лица в период интоксикации ощущают безграничные творческие способности: им кажется, что они сочиняют музыку, складывают стихи, им приходят в голову удивительные фасоны одежды и пр.
>фигурант данного треда
Иди нахер с таким жаргоном. Полицейщина мерзкая.
>А где он про "фигурант данного треда" пишет, я не вижу
В некрологе на Воеводского и пишет.
>им приходят в голову удивительные фасоны одежды и пр.
удивительные фасоны оснований математики, ага.
Есть симплициальная категория Delta. Есть кубическая категория I, даже в нескольких версиях. С дельтой в hott вроде все кисло. С кубиками лучше.
Есть категория Gamma имени Сигала. Есть Sym^{op}, скелет FinSet^{op}. Гамма относится к дельте, как сим-оп к кубикам. Я не знаю, насколько это известно и банально, но это так.
1. Ясно, что дельта и кубики - это что-то ассоциативное, а гамма и сим-оп - это что-то ассоциативное и коммутативное. Есть ли в hott утверждение вида "когда ассоциативно - это гомотопический тип, а когда еще и коммутативно - это спектр"?
2. Гомотопический тип - это хороший предпучок и на дельте, и на кубиках. С гаммой и сим-оп все сложнее. Хороший симплициальный предпучок на гамме - это связный спектр. Хороший предпучок на сим-оп, со значениями в категории симплициальных множеств с отмеченной точкой, - это спектр, не обязательно связный. Раз в одном случае эквивалентность есть, а в другом эквивалентности нет, оба случая нетривиальны и содержательны. Hott как-нибудь помогает увидеть это нетривиальное содержание?
выкиньте свои комплексы Кана, вместе со всей фибратной демагогией, прямо в анналы истории, и Квиллена туда же, быстро, решительно.
если вы обращали внимание, то Сова хвалит Лури, который тоже увлекался именно эти клеточными комплексами, но зато Каледин ругает. и для того есть причины.
...И причины эти в том, что Каледин Иванова дураком считает.
типа сидит каледин такой, на лурье подрачивает, утомился, зашёл в блог совы... ба! а сова, оказывается, лурье любит! быстрее побегу, напишу, как я лурье не выношу вообще
Побегу и напишу
@
Как лурье не выношу
Матемачу давно не хватает частушек. И гармониста.
Вышел модуль на крыльцо
Расширить себе кольцо
Сунул функтор нет кольца
Так и шлёпнулся с крыльца