24 декабря Архивач восстановлен после серьёзной аварии. К сожалению, значительная часть сохранённых изображений и видео была потеряна. Подробности случившегося. Мы призываем всех неравнодушных помочь нам с восстановлением утраченного контента!
Тред открывает Самуэль Эйленберг, один из создателей гомологической алгебры и теории категорий. Теория категорий занимает центральное место в современной математике, находя многочисленные применения и за её пределами.
Кроме этого, предлагается 2 задачи, соответствующие по стилю двум лагерям посетителей этих тредов.
1. Рассмотрим категорию Ch(R) цепных комплексов правых R-модулей, где R - ассоциативное кольцо с единицей. Известный факт - Ch(R) абелева. Рассмотрим категорию K(R), которая является факторкатегорией Ch(R): объекты в ней те же, а морфизмы - это классы эквивалентности морфизмов в Ch(R) по отношению гомотопности. Вопрос - будет ли K(R) абелевой категорией? 2. Решить в натуральных числах уравнение 5^n=6*m^2+1
P.S. Нормальный математик способен решить обе задачи.
>>255072 На самом деле элементарного решения (которое мог бы придумать школьник) я не знаю. Возможно, его и нет. Но я и не говорил, что задача школьная.
Мне кажется, что решение я нашёл, позже напишу его, если никто не придумает. Но оно использует некие знания о факториальности колец.
>>255039 Попробую вторую. Легко видеть, что (2, 2) - решение. Попытаемся показать, что их больше нет. Точнее, покажем, что бесконечно много их быть не может, а если есть еще (по ходу доказательства будем откидывать вырожденные случаи), то они маленькие.
Рассмотрим по модулю 6 => n четно. Во имя экономии букв переобозначим n := 2n, т.е. 5^2n = 6m^2+1. Перепишем как (5^n)^2 - 6 m^2 = 1. Это уравнение Пелля: x^2 - n y^2 = 1. Нам понадобится пару фактов: 1) (a, b) - решение уравнения Пелля <=> a + b sqrt(n) имеет норму 1 как элемент поля Q(sqrt(n)), т.е. является в нем обратимым элементом. 2) Ранг группы обратимых элементов поля Q(sqrt(n)) равен 1. Это значит, что все обратимые элементы являются степенями одного из них, и, поскольку при умножении элементов Q(sqrt(n)) коэффициенты будут расти, все решения можно породить из первого нетривиального тривиальное - (1, 0). В нашем случае таковым решением является (5, 2). Таким образом, если (x, y) - k-ое решение, то (k+1)е решение - это (5x + 62y, 5y+2x) раскройте скобки в (x + ysqrt(6))(5 + 2sqrt(6)), или (5x+12y, 5y+2x).
Нам нужно найти такое решение нашего уравнения Пелля, у которого x = 5^n для некоторого (достаточно большого) n. Попытаемся показать, что таких нет. Первым делом посмотрим на связь k-го и (k+1)-го решения: (x, y)=>(5x+12y, 5y+2x). Отсюда видно, что если есть некоторое решение (5x+12y, 5y+2x), у которого 5x+12y = 5^n, то y должно делиться на 5. Во имя экономии букв y заменим на 5y: (x, 5y)=>(5x+60y, 25y+2x). Составим систему из двух уравнений: 1) В новом решении первая компонента равна 5^n, т.е. 5x + 60y = 5^n, или x + 12y = 5^(n-1). Во имя удобства n-1 заменяем на n: x + 12y = 5^n. 2) Старое решение (x, 5y) тоже является решением: x^2 - 625y^2 = 1. Выражаем в первом уравнении x и подставляем его во второе. Получается квадратное уравнение на y. После сокращения оно принимает вид: 6y^2 + 245^ny - (5^(2n) - 1) = 0. Дискриминант равен ВНЕЗАПНО 4, корни (-245^n +- 2)/(26). Видно, что числитель на 6 не делится, значит, y не целое - противоречие с тем, что решения задачи существует меньшее решение (x, y). Единственный возможный вариант из оставшихся - что наше решение и есть наименьшее. Этот вариант реализуется. endproof;
>>255088 Более того есть теорема о том, что не существует программы в общем виде решающей диофантово уравнение (или хотя бы которая говорит существует ли решение вообще).
>>255089 Ну, это имеется ввиду "настоящее" решение. Но вольфрам же легко может обладать механизмами распознавания таких уравнений, у него, вроде, довольно продвинутый CAS.
>>255088 Кстати умеет, вот только что это тебе даст? Теперь надо найти все такие t, что число ((5 + 2 sqrt(6))^t + (5 - 2 sqrt(6))^t)/2 равно степени пятерки. Я бы не сказал, что стало проще.
>>255076 вот вам половину решения по-школьному: 5^n оканчивается на 0 либо 5=> =>6*m^2 оканчивается на 4 (на 9 оканчиваться не может т.к. число четное) => =>m^2=4X, где X- число у которого есть натур. корень Y=> =>m=2Y, где Y - любое нат. число посчитать n че-то не получается, возможно сделаю когда просплюсь
>>255083 >После сокращения оно принимает вид: 6y^2 + 245^ny - (5^(2n) - 1) = 0. Дискриминант равен ВНЕЗАПНО 4 Нет. (245^n)^2-(5^(2n)-1)64=5^2n(24^2+24)-1 Проебал знак и квадрат у 24, полагаю.
>>255113 там очевидно подставляются двойки и по индукции дальше из >>255110 выражения видно: 5^n=24X+1, (X-любое нат. число как я определил в первом посте) если X=1 то n=2, то есть (m,n)=(2,2) проходит если n=3 , то получается 125=6m^2+1 124=6m^2 но m=2Y, значит m^2 кратно 4, значит 6m^2 кратно 24, чего нет в левой части, значит m=3 не проходит, это база индукции. допустим при n=t>3 равенство не выполняется, то есть: 5^t-1 != 24X, для наглядности (5^t)/24=А, то есть А-1/24!=X тогда при n=t+1 (5^t)5-1 != 24X, или 5А-1/24 != X интуитивно вроде ясно что если при вычитании из нецелого числа (А) другого нецелого (1/24) мы не получим целое (X), то и домножив А на 5 мы целый Х не получим, доказать это вроде как несложно (все дробные части 5А можно тупо перебрать), но мне лень.
Итак, платина. Какая книга самая читабельная по математике. На первом курсе сдавал экзамен по векторной алгебре и матану по самому ебнутому учебнику. Тогда было похуй. Сейчас решил задрочить, ибо чувствую, что по базе где-то, но проседаю.
>>255345 >доказать это вроде как несложно (все дробные части 5А можно тупо перебрать), но мне лень. ДОКАЗАЛ ТЕОРЕМУ ФЕРМА ТЧК ДЛЯ N=3 ДОКАЗАТЬ, ВРОДЕ, НЕСЛОЖНО, А ДАЛЬШЕ ПО ИНДУКЦИИ
Суп. Не знаю, где спрашивать, поэтому спрошу здесь. Есть ряд a(n)=144/(n^2+18n+80) Посчитал его сумму аналитически, вышло 17. Посчитал частичные суммы ряда, формула получилась такая: 17 - (72(2N + 19))/((N + 9)*(N + 10)) Посчитал частичные суммы для N=100, 1000, 10000, 100000 Они получились: 15.6849 16.8574 16.9856 16.9986 cоответственно. Нашел абсолютную и относительную погрешности для каждого значения, затем число верных цифр через формулу с относительной погрешностью. Эти числа получились 2, 3, 4, 5 соответственно. Все эти вычисления проводил в матлабе. Проверял несколько раз, ошибок нет.
Потом нашел количества верных цифр другим способом, через определение верного числа, и в этот раз количества получились 1, 2, 3, 4.
Встаёт вопрос: какого хуя?
С одной стороны, если первый набор верный, то при округлении до приведённого количества знаков не получается искомое число, получается ряд: 16, 16.9, 16.99, 16.999, что неправильно.
Если верен второй набор, то при округлении выходят верные числа, но: первое значение, 15.6849, до одного знака не округлить никак.
Мои расчеты пикрелэйтед, уже хуй знает сколько сижу с этим, нихуя понять не могу, в чём проблема.
>>261422 на английском, надо думать сейчас везде зарубежом математику на английском ведут вроде да даже на матфаке сегодня вроде есть курсы на английском а мочизуки - это фетиш, да (но на самом деле он просто няшка и бог)
А помогите пожалуйста с матаном. Нужно доказать, то несобственный интеграл sin(x^2) (от 0 до бесконечности) сходится, критерием Коши. Как, например, Абелем сделать - я знаю, а тут в ступоре.
>>280904 >Бурбаке >гранты Наркоман? Это была группа уже состоявшихся математиков на зарплате, бурбакизм они пилили из любви к искусству. Какие деньги, на что?
>>281116 Это дух истинного математического треда сциентача. Фантомный образ того самого лампового идеала, который не может быть достигнут. И поэтому он будет жить вечно.
Меня интереусет определение без порочного круга. Предлагали аскиомы Пеано, но как я уже писал они строятся в формальных системах в которых индукция (а как прямое следствие и N) понимается интуитивно как первоначальное понятие.
>>292659 Стоп-стоп. Ты галопом по Европам не прыгай. Определение натуральных чисел - это вообще что по-твоему? Это всего лишь описание свойств некоего объекта ("суть" объекта не важна, это могут быть множества, лямбда-термы, дискретные категории, моноиды без нетривиальных стрелок, NNO, да хоть аллах). А индукция (точнее, аксиома индукции) - это всего лишь одно из свойств, которые мы задали сами, как захотели (точнее потому, что такое определение полезно). И подумай сам, почему эта аксиома обычно последняя, и ты поймёшь глупость своего вопроса. Ещё добавлю, что есть системы арифметики, где аксиома индукции совсем другая. А есть ещё, ВНЕЗАПНО, разрешимые, полные и системы, допускающие уничтожение кванторов (мне похуй на перевод на пидарашкоязык).
В случае натуральных числе в том и сложность, что отстраненное описание объекта без привлечения понятий уровня самого определение N невозможно. Индукция понимается расширенно, т.е. по сути. Как неограниченный процесс последовательного применениея какого либо действия (с предположением что мы на каждом шаге понимаем что это за действие).
>>292779 Ещё раз говорю, индукция индукции рознь. В PRA это эффективно просто цикл for ... do с конечным числом шагов. Где тут зацикленность определений? Вообще не понимаю, в чём твоя проблема.
Так с конечным числом шагов ты далеко и не уедешь, тут и обсуждать нечего. А как только пявляется какая либо форма бесконечной индукции, то тут и появляется проблематика про которую я в том посте писал.
>>292613 >Тут есть кто-нибудь, кто хоть сколько-то владеет пруверами? Или только верунчики-мочисосники? Только верунчики. А ты никак интер-юниверсал тейхмюллер теорем доказать надумал, лол? К слову, я что-то не нагуглил Мочизукиной цитаты с пика, видимо проблема_цитат_в_интернете_ленин.png?
>>293155 > Каким именно прувером владеешь? Знаком с Idris'ом (близок к Adga) же, хотя это не совсем прувер. Неприятная особенность пруверов состоит в том, что они зовут определения типов и функций как definition constant variable theorem inductive record structure и прочими словами, слабо связанными с семантикой. А вообще, можешь глянуть http://docs.idris-lang.org/en/latest/index.htmlпожалуй, более подробная документация, чем у хаскеля и https://leanprover.github.io/tutorial/index.html
>>293161 > Зацикленность определений В чём конкретно?
> Не сможешь ни в какой форме оперировать бесконечностью в математике, а это эпик фейл на который никто не согласен. Ты ведь гумус, да? Просто признайся, чтоб я не тратил время понапрасну.
>>293193 > интер-юниверсал тейхмюллер теорем Нет такой теоремы. Это раз. Второе: его говнотеория нахуй не нужна. Характерный пример, как классическая математика скатывается в сраное, ненужное и неоперабельное говно. Другое дело - каты, зависимые типы, нормализация.
>>293212 Нет, ты этим явно не владеешь. Видел твой тред в пр. Или, если думаешь, что владеешь, нормализуй простенькую теорему:
для любых (рациональных) p, q, p<q существуют такие натуральные n и k, что пикрелейтед
>>293220 > Прувер должен упрощать усилия, а не усложнять. Тогда Agda здесь явно мимо из-за отсутствия тактик (как и Idris, хотя для него тактики можно написать).
>>293223 Ты, по-моему, путаешь дар божий с яишницей. Причём тут идрис и агда, если я веду речь о пруверах? Прувер - это специализированный софт (со своим скриптовым языком). Идрис и агда - просто ФЯП. А, ну давай, скажи мне опять, что в них любая прога автоматом - доказательство теоремы
>>293231 > спойлер Зачем? Проще показать https://github.com/HoTT/HoTT-Agda > Причём тут идрис и агда, если я веду речь о пруверах? Ок, я понял, о чём ты. Тогда нет.
>>293231 >>293220 >В том и фишка. Прувер должен упрощать усилия, а не усложнять. >Прувер - это специализированный софт (со своим скриптовым языком). Ты понимаешь, что софта, который бы сколь-нибудь существенно помогал доказывать теоремы путем автоматизации процесса доказательства фактически нет? Все что есть - это программы автоматизация в которых практически исчерпывается нахождением формальных выводов для некоторых совершенно очевидных с точки зрения нормальных математиков переходов. другой анон
>>293239 Единственное сколь-нибудь полезное, с точки зрения доказательство теорем, применение для всех этих систем - это видимо замена перебирающих программ на формализованные версии. Видимо случаи когда в пруф ассистанте сделать перебор легче, чем написать программу крайне редки, но безусловно первое выглядит куда убедительнее. Правда, насколько для этих применений существенен аппарат тактик - это еще вопрос. Я читал статью о формализации теоремы о четырех красках и как там утверждалось, тактики там использовались вемьма мало.
>>293238 Бред. Я лично с Бауэром и Швихтенбергом общался. Один хорошо владеет когом, а другой - разработчик минилога (на схеме). У меня есть куча примеров теорем анализа, формализованных в минилоге. Я спрашивал не потому, что я ничего об это не знаю, я спрашивал, есть ли ИТТ кто-то, кто владеет.
>>293280 > Использование интуитивного понятия индукции в той или иной форме при определении N. Конкретно выражайся. Что такое N? Множество натуральных чисел? Так его нет в аксиомах Пеано. В PA вообще нет множеств, её язык не позволяет формализовать такое понятие. Второе, что такое "интуитивное" понятие индукции? Конкретно математическими терминами выражайся. Третье, ещё раз говорю аксиома индукции - это всего лишь отдельная аксиома. Как это понять: она определеяет N? словоблудие полное.
> Я то нет. Пруф диплома, пожалуйста. Мои - на пике. Я приматчик, но хотя бы не ГСМ как ты.
> Конкретно выражайся. Что такое N? Множество натуральных чисел? Так его нет в аксиомах Пеано.
Множества тут ни при чем, для начала хоть как-то эти объекты определи.
> Второе, что такое "интуитивное" понятие индукции?
В книгах по матлогике "интуитивное" часто называют "содержательным" как противоположность формального подхода. Это часть так называемой абстракции потенциальной осуществимости, т.е. предположения что мы можем проводить счетно-конструктивные процессы бесконечно долго и на каждом шаге можем осознать построенный объект.
> Конкретно математическими терминами выражайся.
Я выражаюсь конкретно на сколько это возможно (по крайней мере в книжках по матлогике используют такие же термины, я ни одного не выдумал). Формально тут выражаться невозможно потому что это исходные понятия, неопределяемые.
> Третье, ещё раз говорю аксиома индукции - это всего лишь отдельная аксиома. Как это понять: она определеяет N? словоблудие полное.
Ну аксиома, и что? Вопрос то ставился, как определить натуральные числа, а ты предложил эту аксиоматику в качестве определения. На что я тебе возразил, что в таком случае она содержит порочный круг в своем определении. Теперь ты говоришь, типа , а эти аксиомы и не должны определять N. Тогда зачем ты их вообще притянул?
>>293285 >Бред. >Типичный бред мочисосника. Это конечно замечательный уровень аргументации. Но, каким образом, единственное содержательное, что ты сказал по этом поводу >У меня есть куча примеров теорем анализа, формализованных в минилоге. противоречит моим наблюдениям о текущем положение дел? Вопрос ведь не в принципиальной возможности формализации (так и в idris'е принципиально ничего не мешает формализировать), а в количестве усилий затрачиваемых на получение доказательства в пруф ассистанте по сравнению с аккуратным доказательством на человеческом языке.
>>293287 Пруфани дипломом. И ты кто вообще? Это ты про идрис писал или про аксиомы Пеано?
>>293384 Какой порочный круг, какие неопределимые понятия, исходные какие? - ё-моё, что несёт, вообще охуеть. С ужасом представляю, какая у тебя каша в голове.
>>293396 Ты не можешь этого сравнивать, потому что не владеешь аппаратом. Кто-то вспашет поле мотыгой, потому что ему так проще и понятнее, а кто-то изобретёт трактор и навесной плуг. Второе займёт, допустим, много больше времени, но всего лишь один раз.
>>293406 >Ты не можешь этого сравнивать, потому что не владеешь аппаратом. Ну офигеть, какой-то прикладник, который почувствовал себя приобщившимся к высокой науке, будет указывать мне, что я могу оценивать, а что нет. Мне приходилось слушать доклады и просматривать статьи людей, которые этим занимаются. Этого вполне достаточно, чтобы иметь общее представление о положение дел в области. >Кто-то вспашет поле мотыгой, потому что ему так проще и понятнее, а кто-то изобретёт трактор и навесной плуг. Второе займёт, допустим, много больше времени, но всего лишь один раз. Я конечно могу что-то упускать. Но когда ты, человек позиционирующий себя, как специалист в этой области, в качестве возражений даешь не конкретные примеры успешного применения, а очень неконкретно сформулированные ожидания(?) это лишь подкрепляет справедливость моих наблюдений (еще раз подчеркну, о текущем положение дел, а не о том, до чего это может развиться через 20 лет).
>>293213 >Нет такой теоремы. Это раз. Да, это теория, не теорема. Попутал, бывает. >его говнотеория нахуй не нужна. Характерный пример, как классическая математика скатывается в сраное, ненужное и неоперабельное говно. Ну ты в ней хоть разобрался, что такие заявления делаешь? Или как в совке было с Пастернаком, "не читал, но осуждаю"?
>>293418 > конкретные примеры успешного применения > даешь не конкретные примеры успешного применения Охуенные маневрирования, студент мухосранского матфака. Ещё одно подвтерждение, что математике можно научиться только самому, что я и делаю на протяжении многих лет. В то время как напыщенные студики Верхнекрасножопинских вузов будут думать, что Сидор Феофанович им всё охуенно разжевал. Или какой-нибудь индюк уровня Алексея Бабушкина расскажет им о пруверах на студенческой конференции деревени Мошонки.
> позиционирующий себя, как специалист в этой области Процитируй.
>>293422 Ещё чего. Разбираться в каком-то неоперабельном говне. Желаю удачи тем клоунам, кто решился. Главное, чтоб как у Отелбаева не вышло бггг
>>293431 >Аргментов по существу дела у меня нет, сведу спор к чистой демагогии. Не то, чтобы в твоих предшествующих постах не было демагогических приемов, но это уже за гранью - мне на таком уровне спорить не интересно.
>>293469 Ладно, предположим, что ты неадекватно понял мою позицию, а не то, что ты лишь притворяешься, упорствуя в повторение своего аргумента, который совершенно не противоречит тому, о чем писал я.
Фактически, выше ты утверждал, что одно из качеств прувера состоит в, упрощение доказательств теорем по сравнению с обычным математическим подходом (по крайней мере я так тебя понял). Я же утверждаю, что современные нам пруф ассистанты этого, возможно за исключением очень специфичных случаев, не достигают. Чуть подробнее. Пусть у математика есть более-менее оформившиеся идеи доказательства некой гипотезы. Перед ним есть две возможности - написать статью с доказательством или формализовать доказательство в одном из современных пруф ассистантов. Так вот, я утверждаю, что первое, на текущий момент, практически во всех ситуациях, будет существенно проще. При этом, я совершенно не сомневаюсь, что если, скажем, подробное, не апеллирующее к геометрической интуиции и т.п., доказательство уместилось, скажем, в 20 страниц, то его формализация является вполне выполнимой задачей или что вполне реально формализовать классический анализ.
У меня сложилось впечатление, что современные пруф ассистанты (это пруверы или нет?) сделаны чтобы не упрощать процесс доказательства, а заставлять проверять мельчайшие детали, чтобы не допустить ошибку. А так же брутфорсить комбинаторику всякую.
>>293479 >>293491 А ты так и не выучил падежи, клоун? Все твои посты как пахли собачьей ссаниной 3 года назад, так и пахнут. Мне до безобразия противно с тобой вообще говорить, зная какой ты неадекватный дурак, и даже похуй, что ты там будешь сейчас кукарекать про отход от темы.
Твоё понимание пруверов, их цели и задачи, до ужаса вульгарно. Суть прувера не в облегчении (по крайней мере на начальных этапах). Как и, собственно, суть правильной, конструктивной математики, а в аккуратности и полезности построений. Если ты откроешь код, скажем, IVT из примеров минлога, то увидишь, что никакой ёбли с деталями там нет и код легко читаем и короток. Он, конечно, длинее пруфа, записанного на бумажке, но легко сопоставим с ним. Поскольку правильная математика имеет existence и disjunction property, то термы низшего тайплевела генерируются из такого пруфа автоматически путём нормализации и получаем, вуа-ля, рабочий алгоритм, готовый к применению сразу с доказательством его корректности. В HOL Light формализация ещё проще (formalizing 100 theorems of analysis in HOL Light) и код пруфов выглдяти практически также, как и сами пруфы. IVT - довольно простой пример. Рассмотрим такой весьма полезный пример, как Ляпуновская теория стабильности. На практике нас интересует не стабильность как таковая (по крайней мере не абстрактное существоавние области стабилньости, а как минимум точная её оценка), а ассимптотическая стабильность с оценкой скорости сходимости. При некоторых естественных условиях на модель системы и её функцию Ляпунова, такая оценка возможна и тогда, доказывая устойчивость, в минлоге получаешь алгоритм оценки автоматом. При этом, делая это ручками, можно было бы охуеть (задача с экспоненциальными рядами выше, например). Пруверы кажутся дикостью тем, кто не владеет программированием. А это как правило студенты мухосранских матфаков, учащиеся по программе 19го века, и не слышавшие о HoTT ни слова.
>>293581 Во-первых, петушная - это мочисосники. А во-вторых, мы живём в эру компьютеров. Классикопетушки становятся не нужны.
>>293590 > оценивает таймлайн этого процесса как "лет 10" Во-первых, цитатку, а во-вторых, HoTT - развивающайся теория, не говоря уже о том, что 10 лет - не срок для серьёзных разработок. Конечно, это не петушиные 10 аксиом а-ля "давайте придумаем всезнающий оракул, который за нас всё будет решать" (кто не понял, это аксиома выбора)
> покажи код теоремы С какими пацанами? Ты же вообще ни в какой код не можешь, студентик мухосранского матfuck'а.
>>293550 >что ты там будешь сейчас кукарекать про отход от темы. >Он, конечно, длинее пруфа, записанного на бумажке Или иными словами, ты и сам вполне понимаешь, что я прав. Твоя проблема состоит в том, что ты выдаешь свои мечты за реальность и при этом агрессивно настаиваешь на их истинности. Идеи о практическом применение изоморфизма Карри-Говарда для теории типов - это круто, но опять же текущие реализации недостаточно хороши, чтобы было осмысленно использовать это кому-либо, если его не интересуют пруф ассистантами сами по себе (или что-нибудь родственное). Лучше бы прекращал тут распространять ложную информацию, а написал какую-нибудь новую тактику (или как там называется аналог для минлога?), может и приблизил бы светлое будущее, где действительно "пруверы упрощают усилия".
>>293647 " что гораздо важнее и интереснее заниматься разработкой новой системы для формальных доказательств построенной с учетом унивалентной семантики и того нового виденья "смысла" в языках теории типов, которые она открывает. А сколько времени это может занять, я пока совершенно не вижу."
Я немного познал дзен на выходных, потому не буду тебя витиевато поливать говном, скажу только, что код на лиспе/coq читается заметно хуже обычного языка + LaTeX.
> Какой порочный круг, какие неопределимые понятия, исходные какие? - ё-моё, что несёт, вообще охуеть. С ужасом представляю, какая у тебя каша в голове.
Это у тебя вместо мозга насрано. Зачем ты лезешь в спор, если фомрулировку задачи не осилил???
>>293773 > Я немного познал дзен на выходных Буду считать, что я своей цели добился. Посеял семена сомнения ещё в одном глупом мочисоснике. Как говорил Андрюша Бауэр, в обращении к конструктивной математике человек должен пройти отрицание-гнев-торг-депрессию-смирение. Отрицание у тебя уже пробито.
>HoTT - развивающайся теория Молодая, динамично развивающаяся теория. >всезнающий оракул, который за нас всё будет решать >аксиома выбора Аксиома выбора? А я думал, у тебя самокритика пробудилась. Конструктивисты и интуиционисты на протяжении десятилетий старательно зарабатывали себе статус петухов-сектантов сомнительной научной ценности. Если когда-то их (при большом желании) можно было воспринимать серьезно, то теперь в среде нормальных математиков (сияние интуиционистической задницы быстро озаряет комнату) уважительнее сделать татуировку хуя на лбу, чем признаться в принадлежности к гребешковому братству. Главные методы убежденного сторонника альтернативного взгляда на математику, как ИТТ, так и ИРЛ — разведение истерики, тупых, бессмысленных и беспощадных срачей, паразитирование на «модных трендах», вроде компьютеров и компьютерных доказательств (компьютерные вычисления, конечно, придумали конструктивисты), вербовка школоты, которая еще не знает что да как. А разгадка проста: математик использует любые методы, в том числе «конструктивные», конструктивист — только конструктивные (на самом деле не конструктивные, а рекламные, потому что содержательная деятельность для лохов, которые скоро загнуться). Я бы этого не писал, если бы экспонат ИТТ, не был типичным представителем своего вида.
>>293929 Чувак, я сам дрочу на всякие типы и пруф асистанты, но это не значит, что они в текущем состоянии для чистой математики не говно (если хочешь аккуратной формулировки: не настолько полезны насколько тебе и мне хочется).
>>293948 Был культурный конфилкт в 60-х. Тогда математика и физика отдалились. Сейчас у них неплохой союз (особенно он блистал в 80-е и 90-е).
А так вообще причины обычные: математики говорят, что физки преступно нестроги, а физики, что математики занимаются никому ненужным буквоедством и игрой в бисе.
Что, конечно, детсад. Потому что физику и не надо быть строгим, т.к. есть эксперимент и он решает успешность модели, а математика настолько строга, насколько это надо чтобы не совершать ошибок на данном её этапе развития.
Тред открывает Самуэль Эйленберг, один из создателей гомологической алгебры и теории категорий. Теория категорий занимает центральное место в современной математике, находя многочисленные применения и за её пределами.
Кроме этого, предлагается 2 задачи, соответствующие по стилю двум лагерям посетителей этих тредов.
1. Рассмотрим категорию Ch(R) цепных комплексов правых R-модулей, где R - ассоциативное кольцо с единицей. Известный факт - Ch(R) абелева. Рассмотрим категорию K(R), которая является факторкатегорией Ch(R): объекты в ней те же, а морфизмы - это классы эквивалентности морфизмов в Ch(R) по отношению гомотопности. Вопрос - будет ли K(R) абелевой категорией?
2. Решить в натуральных числах уравнение 5^n=6*m^2+1
P.S. Нормальный математик способен решить обе задачи.