Я с тобой, друг
вторая сложная чёт
На самом деле элементарного решения (которое мог бы придумать школьник) я не знаю. Возможно, его и нет. Но я и не говорил, что задача школьная.
Мне кажется, что решение я нашёл, позже напишу его, если никто не придумает. Но оно использует некие знания о факториальности колец.
Попробую вторую.
Легко видеть, что (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;
Фак, все звездочки умножения превратились в разметку. Ну, я надеюсь, по написанному это можно восстановить.
А вольфрам альфа не умеет такие задачи решать, что ли?
Более того есть теорема о том, что не существует программы в общем виде решающей диофантово уравнение (или хотя бы которая говорит существует ли решение вообще).
Ну, это имеется ввиду "настоящее" решение. Но вольфрам же легко может обладать механизмами распознавания таких уравнений, у него, вроде, довольно продвинутый CAS.
Задачи нинужны. Один дурак может задать тысячу вопросов.
Кстати умеет, вот только что это тебе даст? Теперь надо найти все такие t, что число ((5 + 2 sqrt(6))^t + (5 - 2 sqrt(6))^t)/2 равно степени пятерки. Я бы не сказал, что стало проще.
о, уравнение Пелля, найс
вот вам половину решения по-школьному:
5^n оканчивается на 0 либо 5=>
=>6*m^2 оканчивается на 4 (на 9 оканчиваться не может т.к. число четное) =>
=>m^2=4X, где X- число у которого есть натур. корень Y=>
=>m=2Y, где Y - любое нат. число
посчитать n че-то не получается, возможно сделаю когда просплюсь
ДОКАЗАЛ ТЕОРЕМУ ФЕРМА ТЧК ПОДРОБНОСТИ В ПИСЬМЕ ТЧК ОСНОВНАЯ ИДЕЯ - ПЕРЕНЕСТИ с^n В ЛЕВУЮ ЧАСТЬ ТЧК
Ну и нахуй тогда она нужна? Хуйню какую-то сделоли.
Доска закрыта?
>После сокращения оно принимает вид: 6y^2 + 245^ny - (5^(2n) - 1) = 0. Дискриминант равен ВНЕЗАПНО 4
Нет. (245^n)^2-(5^(2n)-1)64=5^2n(24^2+24)-1
Проебал знак и квадрат у 24, полагаю.
Почти правильно, только в конце дискриминант неправильный.
Бамп
там очевидно подставляются двойки и по индукции дальше
из выражения видно:
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А можно тупо перебрать), но мне лень.
Итак, платина. Какая книга самая читабельная по математике. На первом курсе сдавал экзамен по векторной алгебре и матану по самому ебнутому учебнику. Тогда было похуй. Сейчас решил задрочить, ибо чувствую, что по базе где-то, но проседаю.
>доказать это вроде как несложно (все дробные части 5А можно тупо перебрать), но мне лень.
ДОКАЗАЛ ТЕОРЕМУ ФЕРМА ТЧК ДЛЯ N=3 ДОКАЗАТЬ, ВРОДЕ, НЕСЛОЖНО, А ДАЛЬШЕ ПО ИНДУКЦИИ
Книг "по математике" не существует. Математика слишком обширна. Читай научные статьи.
http://www.mathnet.ru/php/archive.phtml?jrnid=aa&wshow=contents&option_lang=rus&viewarchiveID=8&vl=21#V21
Aluffi - Algebra: Chapter 0
И, кстати, новая статья
BOGOMOLOV’S PROOF OF THE GEOMETRIC VERSION
OF THE SZPIRO CONJECTURE FROM THE POINT OF
VIEW OF INTER-UNIVERSAL TEICHMULLER THEORY
http://www.kurims.kyoto-u.ac.jp/~motizuki/Bogomolov%20from%20the%20Point%20of%20View%20of%20Inter-universal%20Teichmuller%20Theory.pdf
BOGOMOLOV’S PROOF OF THE GEOMETRIC VERSION
OF THE SZPIRO CONJECTURE FROM THE POINT OF
VIEW OF INTER-UNIVERSAL TEICHMULLER THEORY
http://www.kurims.kyoto-u.ac.jp/~motizuki/Bogomolov%20from%20the%20Point%20of%20View%20of%20Inter-universal%20Teichmuller%20Theory.pdf
Корея? Что за дед в красной толстовке в центре?
Япония, же, RIMS, курс лекций по интеруниверсалке, ну
не тонем
Перекатываемся
Ух ты, кто-то вспомнил былые времена адекватных маттредов
этот тред живее всех живых
на каком языке ведутся лекции?
кто-то из здешних изучает? или это просто фетиш такой?
такие как я этому значительно поспособствовали, меня, например, забанили на неделю
потрясающе, это на самом деле происходит? запись от первого апреля
Суп. Не знаю, где спрашивать, поэтому спрошу здесь.
Есть ряд 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, до одного знака не округлить никак.
Мои расчеты пикрелэйтед, уже хуй знает сколько сижу с этим, нихуя понять не могу, в чём проблема.
Есть ряд 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, до одного знака не округлить никак.
Мои расчеты пикрелэйтед, уже хуй знает сколько сижу с этим, нихуя понять не могу, в чём проблема.
на английском, надо думать
сейчас везде зарубежом математику на английском ведут вроде
да даже на матфаке сегодня вроде есть курсы на английском
а мочизуки - это фетиш, да (но на самом деле он просто няшка и бог)
С очередным новым тредом по традиции вас также приветствует непотопляемый Эйленберг и его две задачки
лёгкий бамп
>5^n оканчивается на 0 либо 5
кекнул
Вечный бамп, по традиции
бамп по традиции!
давайте уже здесь что-нибудь обсудим серьёзно и без понтов, только не знаю что предложить
давайте уже здесь что-нибудь обсудим серьёзно и без понтов, только не знаю что предложить
Это алгоритмически неразрешимая задача.
Колмогоровская сложность нужна ради её свойств.
такс такс что тут у нас ахахах бамп наканец-та
вот настоящий азиатский бог
2. n=2, m=2
мимо на каникулах
бамп
кто что читает сейчас?
читаю вот Желобенко, "Компактные группы Ли и их представления", вроде нормас книжка
Сдаю сраную картофельную сессию, так что временная пауза, увы.
А помогите пожалуйста с матаном. Нужно доказать, то несобственный интеграл sin(x^2) (от 0 до бесконечности) сходится, критерием Коши. Как, например, Абелем сделать - я знаю, а тут в ступоре.
Поясните, кто Бурбаке дал денег на начальном этапе? Какие были гранты тогда?
>Бурбаке
>гранты
Наркоман? Это была группа уже состоявшихся математиков на зарплате, бурбакизм они пилили из любви к искусству. Какие деньги, на что?
То чувство, когда Бурбаки - состоявшиеся математики, а я простой чухан, кукарекающий на дваче.
По традиции
Как же это замечательно звучит.
Что это за тред? Почему он до сих пор жив, если есть маттред? Во всяком случае, мне здесь нравится.
Это дух истинного математического треда сциентача. Фантомный образ того самого лампового идеала, который не может быть достигнут. И поэтому он будет жить вечно.
Вечный
YOU SHALL NOT FALL
Этот тред не умрет
still alive
up up up we go
Как вы тут определяете натуральные числа?
Тут всем на это похуй, маня.
Очень зря.
На что похуй? На корректное определение N?
Круто. У меня начали появляться последователи которым не безразлично это определение.
Похуй на маняфантазии школьников, которым летом нечего себя занять, и они называют себя митамотематиками
Во-первых, метаматематика - это здорово.
Во-вторых, очень важно иметь определения натуральных и всех остальных чисел.
>важно
Кому?
Всем. И даже тебе.
Гёдель уже всё пояснил таким озабоченным важностью.
А ну-ка скажи, что он объяснил. И если скажешь что-то не так, то ты биомусор.
Не употребляй слов смысла которых ты не понимаешь. Гёдель про определения вообще ничего не говорил.
Пеаномрази пытаются в математику, лал.
Я как раз не признаю аскиомы Пеано за определение. Соснул.?
>школьник/недостудент
>не признаю
топ кек
Ебанашка малограмотная, об этом у многих известных математиков сказано. Степанов и Успенский например.
>известных математиков
>Степанов и Успенский
>известных математиков
>какие-то пидорашки
топус кекус
Если некий гомосексуалист будет тут автаркофажить анимой - репортить буду нещадно.
По теме треда. Тут есть кто-нибудь, кто хоть сколько-то владеет пруверами? Или только верунчики-мочисосники?
По теме треда. Тут есть кто-нибудь, кто хоть сколько-то владеет пруверами? Или только верунчики-мочисосники?
>анимой
Доставлено.
Камрад, тут даже определением натуральнх чисел не владеют, какой уж тем прувер.
А что именно тебя интересует? Или чем тебе не нравятся общепринятые опредления?
Репортнуто
Меня интереусет определение без порочного круга. Предлагали аскиомы Пеано, но как я уже писал они строятся в формальных системах в которых индукция (а как прямое следствие и N) понимается интуитивно как первоначальное понятие.
n = 0, m = 0
В натуральных числах, придурок.
Стоп-стоп. Ты галопом по Европам не прыгай. Определение натуральных чисел - это вообще что по-твоему? Это всего лишь описание свойств некоего объекта ("суть" объекта не важна, это могут быть множества, лямбда-термы, дискретные категории, моноиды без нетривиальных стрелок, NNO, да хоть аллах). А индукция (точнее, аксиома индукции) - это всего лишь одно из свойств, которые мы задали сами, как захотели (точнее потому, что такое определение полезно). И подумай сам, почему эта аксиома обычно последняя, и ты поймёшь глупость своего вопроса. Ещё добавлю, что есть системы арифметики, где аксиома индукции совсем другая. А есть ещё, ВНЕЗАПНО, разрешимые, полные и системы, допускающие уничтожение кванторов (мне похуй на перевод на пидарашкоязык).
Вопрос в том как определять, натуральные числа.
В случае натуральных числе в том и сложность, что отстраненное описание объекта без привлечения понятий уровня самого определение N невозможно.
Индукция понимается расширенно, т.е. по сути. Как неограниченный процесс последовательного применениея какого либо действия (с предположением что мы на каждом шаге понимаем что это за действие).
>индукция (а как прямое следствие и N)
Где в индукции N?
>говорит пидор, который аваторкофажит мочидзукой
Магнитные на северном полюсе.
Ещё раз говорю, индукция индукции рознь. В PRA это эффективно просто цикл for ... do с конечным числом шагов. Где тут зацикленность определений? Вообще не понимаю, в чём твоя проблема.
Так с конечным числом шагов ты далеко и не уедешь, тут и обсуждать нечего. А как только пявляется какая либо форма бесконечной индукции, то тут и появляется проблематика про которую я в том посте писал.
> Тут есть кто-нибудь, кто хоть сколько-то владеет пруверами?
Допустим, и? В зависимых типах нет ничего трудного для овладения.
> В натуральных числах, придурок
> подразумевая, что натуральные числа начинаются не с нуля
И эти люди что-то говорят про пидорашкоязык.
Я не видел тот пост. О какой это "проблематике" речь? И что значит "далеко и не уедешь"? Ты гумус или где? Говори чётко.
Каким именно прувером владеешь?
Ты совсем идиот?
> О какой это "проблематике" речь?
Зацикленность определений, то на что ты отвечал.
> И что значит "далеко и не уедешь"?
Не сможешь ни в какой форме оперировать бесконечностью в математике, а это эпик фейл на который никто не согласен.
Дат фил от осознания того, что нельзя взять все интегралы.
>Тут есть кто-нибудь, кто хоть сколько-то владеет пруверами? Или только верунчики-мочисосники?
Только верунчики. А ты никак интер-юниверсал тейхмюллер теорем доказать надумал, лол? К слову, я что-то не нагуглил Мочизукиной цитаты с пика, видимо проблема_цитат_в_интернете_ленин.png?
> Каким именно прувером владеешь?
Знаком с 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
> Зацикленность определений
В чём конкретно?
> Не сможешь ни в какой форме оперировать бесконечностью в математике, а это эпик фейл на который никто не согласен.
Ты ведь гумус, да? Просто признайся, чтоб я не тратил время понапрасну.
> интер-юниверсал тейхмюллер теорем
Нет такой теоремы. Это раз. Второе: его говнотеория нахуй не нужна. Характерный пример, как классическая математика скатывается в сраное, ненужное и неоперабельное говно. Другое дело - каты, зависимые типы, нормализация.
Нет, ты этим явно не владеешь. Видел твой тред в пр. Или, если думаешь, что владеешь, нормализуй простенькую теорему:
для любых (рациональных) p, q, p<q существуют такие натуральные n и k, что пикрелейтед
> для любых (рациональных) p, q, p<q существуют такие натуральные n и k, что пикрелейтед
Лол. Мне и без прувера было бы лень этим заниматься.
В том и фишка. Прувер должен упрощать усилия, а не усложнять.
> Прувер должен упрощать усилия, а не усложнять.
Тогда Agda здесь явно мимо из-за отсутствия тактик (как и Idris, хотя для него тактики можно написать).
Ты, по-моему, путаешь дар божий с яишницей. Причём тут идрис и агда, если я веду речь о пруверах? Прувер - это специализированный софт (со своим скриптовым языком). Идрис и агда - просто ФЯП. А, ну давай, скажи мне опять, что в них любая прога автоматом - доказательство теоремы
> спойлер
Зачем? Проще показать https://github.com/HoTT/HoTT-Agda
> Причём тут идрис и агда, если я веду речь о пруверах?
Ок, я понял, о чём ты. Тогда нет.
>В том и фишка. Прувер должен упрощать усилия, а не усложнять.
>Прувер - это специализированный софт (со своим скриптовым языком).
Ты понимаешь, что софта, который бы сколь-нибудь существенно помогал доказывать теоремы путем автоматизации процесса доказательства фактически нет? Все что есть - это программы автоматизация в которых практически исчерпывается нахождением формальных выводов для некоторых совершенно очевидных с точки зрения нормальных математиков переходов.
другой анон
Тем не менее, есть вещи, которые алгоритмизировать можно, и которые слишком громоздкие, чтобы доказывать вручную.
Единственное сколь-нибудь полезное, с точки зрения доказательство теорем, применение для всех этих систем - это видимо замена перебирающих программ на формализованные версии. Видимо случаи когда в пруф ассистанте сделать перебор легче, чем написать программу крайне редки, но безусловно первое выглядит куда убедительнее. Правда, насколько для этих применений существенен аппарат тактик - это еще вопрос. Я читал статью о формализации теоремы о четырех красках и как там утверждалось, тактики там использовались вемьма мало.
> В чём конкретно?
Использование интуитивного понятия индукции в той или иной форме при определении N.
> Ты ведь гумус, да? Просто признайся, чтоб я не тратил время понапрасну.
Я то нет. А вот судя по уровню вопросов, ты очень смахиваешь на ГСМ.
Бред. Я лично с Бауэром и Швихтенбергом общался. Один хорошо владеет когом, а другой - разработчик минилога (на схеме). У меня есть куча примеров теорем анализа, формализованных в минилоге. Я спрашивал не потому, что я ничего об это не знаю, я спрашивал, есть ли ИТТ кто-то, кто владеет.
Типичный бред мочисосника.
> Использование интуитивного понятия индукции в той или иной форме при определении N.
Конкретно выражайся. Что такое N? Множество натуральных чисел? Так его нет в аксиомах Пеано. В PA вообще нет множеств, её язык не позволяет формализовать такое понятие. Второе, что такое "интуитивное" понятие индукции? Конкретно математическими терминами выражайся. Третье, ещё раз говорю аксиома индукции - это всего лишь отдельная аксиома. Как это понять: она определеяет N? словоблудие полное.
> Я то нет.
Пруф диплома, пожалуйста. Мои - на пике. Я приматчик, но хотя бы не ГСМ как ты.
> Я приматчик
Вот это я понимаю, камингаут покруче чем у пидора-яблочника.
PS У меня диплом чистого математика, с такими как ты я даже в одном поле срать не буду.
> Конкретно выражайся. Что такое N? Множество натуральных чисел? Так его нет в аксиомах Пеано.
Множества тут ни при чем, для начала хоть как-то эти объекты определи.
> Второе, что такое "интуитивное" понятие индукции?
В книгах по матлогике "интуитивное" часто называют "содержательным" как противоположность формального подхода. Это часть так называемой абстракции потенциальной осуществимости, т.е. предположения что мы можем проводить счетно-конструктивные процессы бесконечно долго и на каждом шаге можем осознать построенный объект.
> Конкретно математическими терминами выражайся.
Я выражаюсь конкретно на сколько это возможно (по крайней мере в книжках по матлогике используют такие же термины, я ни одного не выдумал). Формально тут выражаться невозможно потому что это исходные понятия, неопределяемые.
> Третье, ещё раз говорю аксиома индукции - это всего лишь отдельная аксиома. Как это понять: она определеяет N? словоблудие полное.
Ну аксиома, и что? Вопрос то ставился, как определить натуральные числа, а ты предложил эту аксиоматику в качестве определения. На что я тебе возразил, что в таком случае она содержит порочный круг в своем определении. Теперь ты говоришь, типа , а эти аксиомы и не должны определять N. Тогда зачем ты их вообще притянул?
>Бред.
>Типичный бред мочисосника.
Это конечно замечательный уровень аргументации. Но, каким образом, единственное содержательное, что ты сказал по этом поводу
>У меня есть куча примеров теорем анализа, формализованных в минилоге.
противоречит моим наблюдениям о текущем положение дел? Вопрос ведь не в принципиальной возможности формализации (так и в idris'е принципиально ничего не мешает формализировать), а в количестве усилий затрачиваемых на получение доказательства в пруф ассистанте по сравнению с аккуратным доказательством на человеческом языке.
Пруфани дипломом. И ты кто вообще? Это ты про идрис писал или про аксиомы Пеано?
Какой порочный круг, какие неопределимые понятия, исходные какие? - ё-моё, что несёт, вообще охуеть. С ужасом представляю, какая у тебя каша в голове.
Ты не можешь этого сравнивать, потому что не владеешь аппаратом. Кто-то вспашет поле мотыгой, потому что ему так проще и понятнее, а кто-то изобретёт трактор и навесной плуг. Второе займёт, допустим, много больше времени, но всего лишь один раз.
>Ты не можешь этого сравнивать, потому что не владеешь аппаратом.
Ну офигеть, какой-то прикладник, который почувствовал себя приобщившимся к высокой науке, будет указывать мне, что я могу оценивать, а что нет. Мне приходилось слушать доклады и просматривать статьи людей, которые этим занимаются. Этого вполне достаточно, чтобы иметь общее представление о положение дел в области.
>Кто-то вспашет поле мотыгой, потому что ему так проще и понятнее, а кто-то изобретёт трактор и навесной плуг. Второе займёт, допустим, много больше времени, но всего лишь один раз.
Я конечно могу что-то упускать. Но когда ты, человек позиционирующий себя, как специалист в этой области, в качестве возражений даешь не конкретные примеры успешного применения, а очень неконкретно сформулированные ожидания(?) это лишь подкрепляет справедливость моих наблюдений (еще раз подчеркну, о текущем положение дел, а не о том, до чего это может развиться через 20 лет).
>Нет такой теоремы. Это раз.
Да, это теория, не теорема. Попутал, бывает.
>его говнотеория нахуй не нужна. Характерный пример, как классическая математика скатывается в сраное, ненужное и неоперабельное говно.
Ну ты в ней хоть разобрался, что такие заявления делаешь? Или как в совке было с Пастернаком, "не читал, но осуждаю"?
> конкретные примеры успешного применения
> даешь не конкретные примеры успешного применения
Охуенные маневрирования, студент мухосранского матфака. Ещё одно подвтерждение, что математике можно научиться только самому, что я и делаю на протяжении многих лет. В то время как напыщенные студики Верхнекрасножопинских вузов будут думать, что Сидор Феофанович им всё охуенно разжевал. Или какой-нибудь индюк уровня Алексея Бабушкина расскажет им о пруверах на студенческой конференции деревени Мошонки.
> позиционирующий себя, как специалист в этой области
Процитируй.
Ещё чего. Разбираться в каком-то неоперабельном говне. Желаю удачи тем клоунам, кто решился. Главное, чтоб как у Отелбаева не вышло бггг
>Аргментов по существу дела у меня нет, сведу спор к чистой демагогии.
Не то, чтобы в твоих предшествующих постах не было демагогических приемов, но это уже за гранью - мне на таком уровне спорить не интересно.
> Может, если я буду отрицать существование формализованных доказательств теорем анализа, то они исчезнут
С тобой всё ясно.
Ладно, предположим, что ты неадекватно понял мою позицию, а не то, что ты лишь притворяешься, упорствуя в повторение своего аргумента, который совершенно не противоречит тому, о чем писал я.
Фактически, выше ты утверждал, что одно из качеств прувера состоит в, упрощение доказательств теорем по сравнению с обычным математическим подходом (по крайней мере я так тебя понял). Я же утверждаю, что современные нам пруф ассистанты этого, возможно за исключением очень специфичных случаев, не достигают. Чуть подробнее. Пусть у математика есть более-менее оформившиеся идеи доказательства некой гипотезы. Перед ним есть две возможности - написать статью с доказательством или формализовать доказательство в одном из современных пруф ассистантов. Так вот, я утверждаю, что первое, на текущий момент, практически во всех ситуациях, будет существенно проще. При этом, я совершенно не сомневаюсь, что если, скажем, подробное, не апеллирующее к геометрической интуиции и т.п., доказательство уместилось, скажем, в 20 страниц, то его формализация является вполне выполнимой задачей или что вполне реально формализовать классический анализ.
У меня сложилось впечатление, что современные пруф ассистанты (это пруверы или нет?) сделаны чтобы не упрощать процесс доказательства, а заставлять проверять мельчайшие детали, чтобы не допустить ошибку. А так же брутфорсить комбинаторику всякую.
А ты так и не выучил падежи, клоун? Все твои посты как пахли собачьей ссаниной 3 года назад, так и пахнут. Мне до безобразия противно с тобой вообще говорить, зная какой ты неадекватный дурак, и даже похуй, что ты там будешь сейчас кукарекать про отход от темы.
Твоё понимание пруверов, их цели и задачи, до ужаса вульгарно. Суть прувера не в облегчении (по крайней мере на начальных этапах). Как и, собственно, суть правильной, конструктивной математики, а в аккуратности и полезности построений. Если ты откроешь код, скажем, IVT из примеров минлога, то увидишь, что никакой ёбли с деталями там нет и код легко читаем и короток. Он, конечно, длинее пруфа, записанного на бумажке, но легко сопоставим с ним. Поскольку правильная математика имеет existence и disjunction property, то термы низшего тайплевела генерируются из такого пруфа автоматически путём нормализации и получаем, вуа-ля, рабочий алгоритм, готовый к применению сразу с доказательством его корректности. В HOL Light формализация ещё проще (formalizing 100 theorems of analysis in HOL Light) и код пруфов выглдяти практически также, как и сами пруфы. IVT - довольно простой пример. Рассмотрим такой весьма полезный пример, как Ляпуновская теория стабильности. На практике нас интересует не стабильность как таковая (по крайней мере не абстрактное существоавние области стабилньости, а как минимум точная её оценка), а ассимптотическая стабильность с оценкой скорости сходимости. При некоторых естественных условиях на модель системы и её функцию Ляпунова, такая оценка возможна и тогда, доказывая устойчивость, в минлоге получаешь алгоритм оценки автоматом. При этом, делая это ручками, можно было бы охуеть (задача с экспоненциальными рядами выше, например). Пруверы кажутся дикостью тем, кто не владеет программированием. А это как правило студенты мухосранских матфаков, учащиеся по программе 19го века, и не слышавшие о HoTT ни слова.
>ассимптотическая
Обосрамс.
Посты от двух разных людей, так что чини детектор.
и вообще, какого хуя программистская петушня лезет в математику?
> что никакой ёбли с деталями там нет и код легко читаем и короток
То-то Воеводский до сих пор не формализовал основания и оценивает таймлайн этого процесса как "лет 10".
Ну и да, покажи код теоремы, мы с пацанами поржом над его читаемостью.
Поссал на агрессивного фанбоя.
Во-первых, петушная - это мочисосники. А во-вторых, мы живём в эру компьютеров. Классикопетушки становятся не нужны.
> оценивает таймлайн этого процесса как "лет 10"
Во-первых, цитатку, а во-вторых, HoTT - развивающайся теория, не говоря уже о том, что 10 лет - не срок для серьёзных разработок. Конечно, это не петушиные 10 аксиом а-ля "давайте придумаем всезнающий оракул, который за нас всё будет решать" (кто не понял, это аксиома выбора)
> покажи код теоремы
С какими пацанами? Ты же вообще ни в какой код не можешь, студентик мухосранского матfuck'а.
http://pastebin.com/hFc3ZB5v
Имплаинг хотт решила проблемы финитного построения.
>что ты там будешь сейчас кукарекать про отход от темы.
>Он, конечно, длинее пруфа, записанного на бумажке
Или иными словами, ты и сам вполне понимаешь, что я прав. Твоя проблема состоит в том, что ты выдаешь свои мечты за реальность и при этом агрессивно настаиваешь на их истинности.
Идеи о практическом применение изоморфизма Карри-Говарда для теории типов - это круто, но опять же текущие реализации недостаточно хороши, чтобы было осмысленно использовать это кому-либо, если его не интересуют пруф ассистантами сами по себе (или что-нибудь родственное).
Лучше бы прекращал тут распространять ложную информацию, а написал какую-нибудь новую тактику (или как там называется аналог для минлога?), может и приблизил бы светлое будущее, где действительно "пруверы упрощают усилия".
Привет, я няшная кошкодевочка.
Привет, кошкодевочка. Я анонимус.
" что гораздо важнее и интереснее заниматься разработкой новой системы для формальных доказательств построенной с учетом унивалентной семантики и того нового виденья "смысла" в языках теории типов, которые она открывает. А сколько времени это может занять, я пока совершенно не вижу."
http://baaltii1.livejournal.com/198675.html
Я немного познал дзен на выходных, потому не буду тебя витиевато поливать говном, скажу только, что код на лиспе/coq читается заметно хуже обычного языка + LaTeX.
> Какой порочный круг, какие неопределимые понятия, исходные какие? - ё-моё, что несёт, вообще охуеть. С ужасом представляю, какая у тебя каша в голове.
Это у тебя вместо мозга насрано. Зачем ты лезешь в спор, если фомрулировку задачи не осилил???
> Я немного познал дзен на выходных
Буду считать, что я своей цели добился. Посеял семена сомнения ещё в одном глупом мочисоснике. Как говорил Андрюша Бауэр, в обращении к конструктивной математике человек должен пройти отрицание-гнев-торг-депрессию-смирение. Отрицание у тебя уже пробито.
>HoTT - развивающайся теория
Молодая, динамично развивающаяся теория.
>всезнающий оракул, который за нас всё будет решать
>аксиома выбора
Аксиома выбора? А я думал, у тебя самокритика пробудилась.
Конструктивисты и интуиционисты на протяжении десятилетий старательно зарабатывали себе статус петухов-сектантов сомнительной научной ценности. Если когда-то их (при большом желании) можно было воспринимать серьезно, то теперь в среде нормальных математиков (сияние интуиционистической задницы быстро озаряет комнату) уважительнее сделать татуировку хуя на лбу, чем признаться в принадлежности к гребешковому братству. Главные методы убежденного сторонника альтернативного взгляда на математику, как ИТТ, так и ИРЛ — разведение истерики, тупых, бессмысленных и беспощадных срачей, паразитирование на «модных трендах», вроде компьютеров и компьютерных доказательств (компьютерные вычисления, конечно, придумали конструктивисты), вербовка школоты, которая еще не знает что да как. А разгадка проста: математик использует любые методы, в том числе «конструктивные», конструктивист — только конструктивные (на самом деле не конструктивные, а рекламные, потому что содержательная деятельность для лохов, которые скоро загнуться). Я бы этого не писал, если бы экспонат ИТТ, не был типичным представителем своего вида.
Молодая, динамично развивающаяся теория.
>всезнающий оракул, который за нас всё будет решать
>аксиома выбора
Аксиома выбора? А я думал, у тебя самокритика пробудилась.
Конструктивисты и интуиционисты на протяжении десятилетий старательно зарабатывали себе статус петухов-сектантов сомнительной научной ценности. Если когда-то их (при большом желании) можно было воспринимать серьезно, то теперь в среде нормальных математиков (сияние интуиционистической задницы быстро озаряет комнату) уважительнее сделать татуировку хуя на лбу, чем признаться в принадлежности к гребешковому братству. Главные методы убежденного сторонника альтернативного взгляда на математику, как ИТТ, так и ИРЛ — разведение истерики, тупых, бессмысленных и беспощадных срачей, паразитирование на «модных трендах», вроде компьютеров и компьютерных доказательств (компьютерные вычисления, конечно, придумали конструктивисты), вербовка школоты, которая еще не знает что да как. А разгадка проста: математик использует любые методы, в том числе «конструктивные», конструктивист — только конструктивные (на самом деле не конструктивные, а рекламные, потому что содержательная деятельность для лохов, которые скоро загнуться). Я бы этого не писал, если бы экспонат ИТТ, не был типичным представителем своего вида.
Я тебе напомню, что компьютер в данный момент невоспринимает неконструктивные методы. А вот интуиционистам скоро пизда.
Чувак, я сам дрочу на всякие типы и пруф асистанты, но это не значит, что они в текущем состоянии для чистой математики не говно (если хочешь аккуратной формулировки: не настолько полезны насколько тебе и мне хочется).
Почему физики всегда хуесосят математиков?
А чем боль и мучения помогают богам?
А чем боль и мучения помогают богам?
Обычно наоборот.
Они просто смотрят на математиков, как на аутистов. И что характерно, зачастую они правы.
Физик это неудавшийся математик.
Был культурный конфилкт в 60-х. Тогда математика и физика отдалились. Сейчас у них неплохой союз (особенно он блистал в 80-е и 90-е).
А так вообще причины обычные: математики говорят, что физки преступно нестроги, а физики, что математики занимаются никому ненужным буквоедством и игрой в бисе.
Что, конечно, детсад. Потому что физику и не надо быть строгим, т.к. есть эксперимент и он решает успешность модели, а математика настолько строга, насколько это надо чтобы не совершать ошибок на данном её этапе развития.
Все взрослые люди это понимают.
Не тонуть.
Аноны, поясните аутисту: почему 2x(x - 1)2 =
2x (x2 - 2x + 1), а не 2x x2 - 2x + 1?
Ведь (a - b)2 = a2- 2ab + b2, а не (a2 - 2ab + b2).
2x (x2 - 2x + 1), а не 2x x2 - 2x + 1?
Ведь (a - b)2 = a2- 2ab + b2, а не (a2 - 2ab + b2).
Что в твоем воспаленном мозгу означает выражение 2x x2 - 2x + 1? В каком порядке в это выражении нужно выполняють операции?
Толсто
Проебался знак умножения между 2x и x^2
Держи: ×
Например, 2×x×y×z
Где нашёл?
2×x×y×z = (2, x, y, z)
Тред открывает Самуэль Эйленберг, один из создателей гомологической алгебры и теории категорий. Теория категорий занимает центральное место в современной математике, находя многочисленные применения и за её пределами.
Кроме этого, предлагается 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. Нормальный математик способен решить обе задачи.