>Уже не за горами то время, когда быть Перельманом станет диковинкой
Ну наконец-то. А то заебали уже эти Перельманы на каждом углу.
>>187536
Влажные фантазии detected. Нет никакой принципиальной трудности обучить обезьяну компьютер отыскивать пруфы. Это в сущности не сложнее (разве что технически чуть позаковырестей), чем создание шахматных программ, которые уже десятилетиями выносят гроссмейстеров на раз. Только почему-то никто не трубит о конце человеческих шахмат, лол. В математике -- аналогично. Ну, будет у тебя суперкалькулятор, тупо доказывающий теоремы, и чо? Он создаст за тебя новую стройную теорию? Скреативит аксиоматику? Усмотрит нетривиальные связи между разными областями математики и приложения в смежных областях? Придумает красивые задачи, ошарашивающие лаконичностью, эстетикой и изяществом решения? Это, блять, творческая деятельность иного уровня, чем тупо-механические правила вывода по уже заданным правилам игры. А правила эти по-любому установит тот, кто этой машиной будет управлять и нетривиально шарить в матчасти на метауровне. Т.е. человек-математик. Трубить о конце человеческой математики с появлением пруверов - это как вещать о конце математики с появлением компов вообще (и Maple с Mathematica в частности), избавляющих ученого от нудных технических вычислений.
И потом, кто-то же должен будет быть в состоянии эти пруверы создавать и проверять, лол.
>>187576
Зачем кичится этим? Отсутствия внятной системы доказательств, вместо собрания методов, - извечная беда всей математики, главная, ящитаю, ее проблема. Ведь никто не доказал, что творческая деятельность не есть почти чистый рандом, с оценочной системой приоритетов на основе левой пятки. В мозге человека нет волшебной коробочки, просто наши тупомеханические правила, сдобренные гормонами и постоянными наблюдениями, оказываются совершенней машин.
Ты опять выходишь на связь, наркоман?
Лучше поясни, как этот твой неровный высер, противоречит идеям Платона, суть которых, если мне не изменяет память, в том что абстракции существуют в своем собственном "мирке" и не требуют человеческого участия для существования.
Он скорее это подтверждает. Хотя любому нормальному человеку, кроме самых упоротых философов, на это в общем-то похуй
>>187576
>не трубит о конце человеческих шахмат, лол
Потому что они фактически уже закончились, по крайней мере профессиональные и по переписке. Если у тебя не просто спор ради спора, погугли скандалы на последних чемпионатах мира, когда никому не известные петушки вдруг начинали обыгрывать чемпионов мира. Если мировые чемпионаты по шахматам превращаются в чемпионаты по поиску коммуникационного оборудования, можешь представить, что будет твориться на соревнованиях местного уровня. Но лично тебе да, никто не запрещает вечерами выяснять с соседом дядей Васей кто из вас тупее, так что можешь продолжать гордиться полетом своей творческой фантазии при постановке детских матов.
И тут я такой с первой теоремой Гёделя о неполноте.
В данном случае близко перекликается с фактом существования алгоритмически неразрешимых задач в теории алгоритмов.
Мы даже никогда не сможем доказать, что прувер сам по себе безглючен и действительно выдает верный выхлоп (теорема Райса).
>>187616
Мы не сможем доказать это, пользуясь только самим прувером, но мы можем использовать метаязык же.
>>187536
Отлично, на подходе техножрецы, ордо меканикус и цивилизация ex machina.
>>187536>>187576
Столько влажных фантазий ИТТ. Если с пруфф ассистантами мы в самом деле имеем постепенный прогресс и можно ожидать, что и в самом деле не за горами времена, когда технические части доказательств, как правило, будут проводиться лишь с помощью пруфф ассистантов. Но вряд ли это само по себе это так уж кардинально изменит деятельность математиков - вместо написания и вычитки подробных доказательств будем ебаться с пруфф ассистантами (хотя здесь остаётся вопрос о том, как будут излагаться и извлекаться содержательные идеи доказательств). И где вы увидели предпосылки для скорого появления систем автоматического поиска вывода, способных заменить математика в деле решения сложных проблем, для меня остаётся загадкой.
> кококо прорыв, люди не нужны, слава роботам
> Plingeling did not return any answer on the encodings of discrepancy 3 problems for sequences of length 14 000 and 16 000 even within 1 550 000 and 2 280 000 seconds, respectively; the computations are still going on and the problem is still open.
проиграл в этом месте
поясните каким вообще хуем утверждение
> No sequence of length 1161 has discrepancy 2
пересекается с
> The Erdos discrepancy conjecture holds true for C = 2.
>>187655
Машинный супер-разум поведет человечество от победы к победе!
СЛАВА РОБОТАМ!
>>187660
Продолжает бомбить? Иди, занимайся творчеством ёпт.
>>187636
>Привет :) Давно не виделись.
Если ты имеешь в виду тот спор - http://2ch.hk/sci/res/181922.html - то я в нем не участвовал.
>>187661
>Иди, занимайся творчеством ёпт.
Как будто что-то плохое. По сути, познание и творчество и есть основные и самые достойные виды деятельности человеков (не согласен - иди соси хуи, это аксиома и она не обсуждается). Вся остальная хуйня с пруверами и пр. - это лишь подсобный инструментарий для облегчения творческих задач. Надо быть абсолютно невменяемым чуваком, чтобы всерьез верить, что инструмент приобретет самодостаточность и заменит во всех аспектах того, для чьих нужд он и был им же создан.
Алсо, я вообще не понимаю, при чем здесь платонизм. Сдается мне, здесь как обычно никто нихуя не владеет терминами, зато все горазды ими понтоваться.
Неплатоник.
Какой-то ты дурачок, если считаешь, что работа математика заключается в проверке истинности никому не нужных теорем путем производства каких-нибудь ебанутых доказательств. Это у олимпиадников и второкультурщиков всяких так (да и то у них есть какие-то критерии красивого решения и важной задачи). Это примерно как считать, что работа писателя состоит в производстве грамматически верного текста.
В первую очередь важно создавать теории и развивать их. Все доказательства в идеале должны быть вообще очевидными. Большие доказательства должны осмысляться и преобразовываться в новую теории, превращаясь со временем в очевидные.
>>187665
> Неплатоник
Так испугался, что теперь воткрытую это отрицаешь?
> Как будто что-то плохое. По сути, познание и творчество и есть основные и самые достойные виды деятельности человеков (не согласен - иди соси хуи, это аксиома и она не обсуждается). Вся остальная хуйня с пруверами и пр. - это лишь подсобный инструментарий для облегчения творческих задач. Надо быть абсолютно невменяемым чуваком, чтобы всерьез верить, что инструмент приобретет самодостаточность и заменит во всех аспектах того, для чьих нужд он и был им же создан.
кококо кекеке куд кудах
ни трошьти маю душу, ДУША ЕТА ГЛАВНАЕ А КАНЛУПТЕРЫ ОТ СОТОНЫ
ясно
>>187683
Дебил, ты вообще хоть одну книжку по математике видел? Definition-Theorem-Proof-Corollary-Remark эврива
> развивать
Лол
> превращаясь со временем в очевидные.
Это ты про то как некогда вполне очевидные теоремы превращаются в abstract nonsense через обобщения обобщений?
>>187736
>Так испугался, что теперь воткрытую это отрицаешь
>Теперь
Товарищ убежден, что я где-то ранее с кем-то на эту тему здесь спорил. Пиздец диванный телепат.
>кококо кекеке куд кудах
>ни трошьти маю душу
Я рад, что паясничество - это всё, что ты можешь, петушок. Давай, дрочи на своих робатов в /re/.
Как я рад, что можно обсудить это - как раз читаю HoTT.
1) я не профи, но вроде как раз подвержает учение Платона о "мире идей" - есть некоторые выражения, по отношению к которым нельзя использовать консьркции "если верно, то..., если не верно, то". Но это не наука и не моё дело.
2) Я читаю на английском, трудно, но тема интересная. какие книжки порекомендуете на русском?
3) Мне хочется вот чего: единого красивого подхода для разных математических направлений.
Я хочу предположительно невозможного: единой стройной системы правил вывода, чтобы углубить своё понимание сути математики.
4) Всё-таки проблема пока у них есть, пришлось вводить аксиомЫ, в том числе одну про унивалентность. Пусть ладно, одну можно потерпеть, но несеолько(тут могу ошибаться - пока не разобрался в предмете)
5) Запомнилась фраза "как-то с самого начала было ясно, что это не шизофрения", к сожалению, Воеводский съехал с катушек и спёкся.
6) Реквестирую каких-нибудь статей или даже книг по этой же тематике, критику особнно, но рад буду всему
>>187736
>Definition-Theorem-Proof-Corollary-Remark
Ты правда думаешь, что часть Proof это ключевое (а остальные четыре из воздуха взялись, наверное)? Proof вообще чуть ли не в половине случаев должен быть "легким упражнением читателю".
>Это ты про то как некогда вполне очевидные теоремы превращаются в abstract nonsense через обобщения обобщений?
Докажи мне, пожалуйста, точность тензорного произведения справа без абстрактной чепухи. Потом докажи, что S^n и S^m (m != n) не гомеоморфны без зачаточной гомологической алгебры. Заодно докажи 101 частный случай теоремы Стокса по отдельности (еще попробуй их запомнить).
Все три примера совершенно очевидны при понимании разного рода "обобщений обобщений", все три можно доказать как-то через жопу и примитивными средствами.
>>187813
>единой стройной системы правил вывода
http://rutracker.org/forum/viewtopic.php?t=2953115
Но ИИ в перспективе заменит вообще любую профессию. Люди станут либо совсем не нужны, либо будешь в виде домашнего животного развлекать своего нового бога.
>>187864
Мы сделаем ИИ именно таким каким мы его сделаем.
Ты бы стал делать ИИ, который будет считать тебя домашним животным? Нет. И никто не будет.
Так что иди нахуй в детский сад с такими рассуждениями.
>>187738
Припекло тебе. Ответить-то нечего. "Роботы" (пиздец, слово-то какое подобрал) продолжают свою экспансию в твой уютный анус мирок.
>>187855
> "легким упражнением читателю"
Ну а ты почитай что-нибудь посерьёзнее учебников.
> Докажи мне, пожалуйста, точность тензорного произведения справа без абстрактной чепухи. Потом докажи, что S^n и S^m (m != n) не гомеоморфны без зачаточной гомологической алгебры. Заодно докажи 101 частный случай теоремы Стокса по отдельности (еще попробуй их запомнить).
> Все три примера совершенно очевидны при понимании разного рода "обобщений обобщений", все три можно доказать как-то через жопу и примитивными средствами.
Так это всё простые вещи.
Мы же речь ведём о таких доказательствах, например, как Гришино, Мочидзукино, Уайльсино.
>>187861
Пикрелейтед
>>187864
Не скатывай в ИИ-срач. Ты играешь на руку платонисту. Пусть у него ещё побомбит.
Речь идёт конкретно о неизбежной ненужности его труда и развитии теорем пруверов.
>>187877
>Припекло тебе.
Ну ладно. Теперь внимательно смотрим мой пост >>187665, твой ответ на него (>>187736) и по соотношению конструктива/паясничства в этих постах делаем неиллюзорный выводо том, кому чего здесь нечего ответить. Алсо, диалог в форме "припекло, кудахкудах, бомбануло, платоник (хотя оппонент им ни в хуй не является) и т.д." -- это уровень улюлюкающей школоты. Я с нею общаться не нанимался. Можешь срочно защитать мне слив, и поярче-поярче, а то вдруг не догадаются.
>>187877
>Ну а ты почитай что-нибудь посерьёзнее учебников.
А ты почитай что-нибудь посерьезней унылых проблемсолверов.
>Так это всё простые вещи.
Ну, так детские примеры (и как их простота опровергает необходимость разного рода абстрактной чепухи, наоборот - даже в простейших вещах жизненно необходима). Хотя в свое время последнее было сложным и с кучей невнятных формул. Наверняка второе тоже исторически появилось с совершенно хардкорным малопонятным доказательством. Сейчас же это даже школьникам можно объяснить. Если хочешь серьезного примера, то гипотезы Вейля.
В общем, еще раз. Цель занятий математикой не в производстве абы каких доказательств абы каких фактов. Во-первых нужно правильно выбирать и формулировать интересующие науку задачи, а во-вторых добиваться того, чтобы доказательства встраивались в стройную теорию, в рамках которой были очевидны. Гротендик же уже все пояснил. А вам бы все доказывать всякую хуйню с помощью компьютера.
>>187877
Для того, чтобы запрограммировать хотя бы даже условие какой-нибудь сложной задачи, необходимо самому владеть понятиями данной области математики, уметь интерпретировать полученные результаты и встраивать их в контекст общей теории и/или ее приложений. Так что нужда в квалифицированных математиках не пропадет уже хотя бы поэтому. А в целом математики переориентируются на прикладные и творческие вещи, переложив рутинные доказательства или проверку каких-то теорем и гипотез на машину, как сегодня перекладывают взятие интегралов на Вольфрам.
>>187884
Гротендик это тот еблан, у которого от занятий возвышенной математикой наебнулись мозги и он истинно уверовал в Господа и Математику Высокодуховную, Данную Им (сотни тысяч страниц высеров созданных им до того опустим за явной их бесмыссленностью)?
Когда наши машинные владыки придут к власти (а этого ждать уже не долго), я буду ходатайствовать о том, чтоб тебя, и тебе подобных, посадили в специальный отдел зоопарка, отведенный для псевдо-разумных существ.
>>187900
>Гротендик это тот еблан
>Когда наши машинные владыки придут к власти
Здесь я проиграл.
>>187878
> хотя оппонент им ни в хуй не является
Ниразу ни платанист.
Я тебе не собирался сливы считать, я точно также жду содержательного ответа на мой вброс. Почему, по твоему мнению, НоТТ и пруверы не взлетят (хотя уже взлетают, вспомнить хотя бы задачу о 4-х цветах, над которой бились столетие). Пока была только истерика про душу, творчество вот это всё.
>>187884
> унылых проблемсолверов
> вспомнить хотя бы задачу о 4-х цветах, над которой бились столетие
Дальше ты сыпешь очень пространно очень общими фразами, но я постараюсь вычленить рациональное зерно. Итак, пример с Гротендиком и вообще любым Бурбаком -- это, конечно, пиздец какой пример "красоты и очевидности" в математике. Надром Бурбаки слились, а Гротендик уебал куда-то в Индию и ушёл из матеши.
> А вам бы все доказывать всякую хуйню с помощью компьютера.
Эмоции.
>>187887
> Свечники переквалицицируются и будут заниматься творческими задачами, пока фонари сами буду загораться от электричества ...
> Пахари найдут виртуозный творческий способ боронить почву плугом с быком, пока трактор будет лишь выполнять рутину ...
>>187990
>Почему, по твоему мнению, НоТТ и пруверы не взлетят
Никто не утверждал, что они совсем не взлетят.
>Свечники
>Пахари
Ок, предлагаю остаться при своих футурологических убеждениях (которые все равно не проверишь). Тем более что дискашен на уровне троллинга (Гротендик еблан, машинные владыки) и передергиваний (свечники-пахари) мне не интересен. Пусть с тобой другой твой собеседник ебётся культурно и аргументированно разговаривает.
>>187990
Алсо, более трезвую (имхо) и реалистичную точку зрения, не отвергающую преимуществ пруверов, но и не приводящую к их абсолютизации в стиле "люди-математики не нужны, слава робатам", я изложил здесь>>187665 и >>187887. Я считаю эти соображения интуитивно очевидными как дважды два, и реально не знаю, как их более обосновать, чтобы они были еще больше очевидными. Тебе они не очевидны - ну ок, значит, у нас с тбобй совершенно разные интуиции и взгляд на математику, творчество и жизнь.
Обратите внимание два британских питуха высрали какое-то говно на 10GB и препринт и про них уже написали в википедии, в отличии от Отелбаева
Такая вот дискриминация
Тут есть кто-нибудь, хоть немного в теме, относительно того что они там доказали, или только одни кукареки?
[url]Покидаю видео от Воеводского для нагнетания обстановки :)
>>187994
А вот это уже попахивает сливой.
Ты не понял смысл троллинга. Дело в том, что профиль какого-нибудь закоронелего set-theorist'а, да ещё с платоном головного мозга, настолько далёк от НоТТ, функционального программирования, всяких кложур, монад, зависимых типов, комбинаторов, что перестроиться такому человеку может помочь только лоботомия. А религиозная предвзятость только усугубляет дело.
Именно о батрухе таких я и говорил, а не о батрухе математиков вообще. Математик математику рознь. И компсаентисты пользуются в среде старомодных математиков дурной славой. Поэтому для очень многих дальнейший тренд не пройдёт гладко, как бы этого ни хотелось.
>>187995
Пока ты не define творчество, говорить не о чем. Мочидзука -- видимо, весьма творческий человек. Где он сейчас? Гротендик -- весьма творческий человек. Где он сейчас?
> запрограммировать хотя бы даже условие какой-нибудь сложной задачи
На 99.5% ниже затраты труда, чем доказательство всего ручками. При условии использования прувера, конечно.
> А в целом математики переориентируются на прикладные и творческие вещи
> прикладные
Лол, я думаю те редкие теоремы, что встречаются в прикладной математике, как раз subject для кога и агды.
> творческие
Всё никак не могу понять, на что ты намекаешь. Уж не на эту ли хуету:
http://en.wikipedia.org/wiki/Heuristic_%28computer_science%29?
>>188006
Обосрался твой козлопас уже.
>>188014
>Мочидзука
Есть мнение что он таки написал прототип ИИ, который делает за него всю работу. Также есть мнение что биткоины замутил он, но под псевдонимом Накамото.
http://www.computerra.ru/89483/satoshi/
>>188026
> В интересах самого Сатоши (если, конечно, он вменяем) явить себя миру
быдлотерра такая быдлотерра
>>187990
Прости, но ты совсем дурачок (или толстый). Я привел вполне конкретное и понятное утверждение, а не "общую фразу". Во-первых нужно правильно выбирать и формулировать интересующие науку задачи, а во-вторых добиваться того, чтобы доказательства встраивались в стройную теорию, в рамках которой были очевидны.
Также совершенно очевидно, что о Бурбаки и Гротендике ты слышал только из википедии и анекдотов. А слился твой анус. Гипотезы Вейля, схемный язык, гомологическая алгебра - заслуги компашки только около Гротендки, а не всех Бурбаки. А это уже чуть ли не половина великой математики 20го века. Я привел три простых примера того, как работает математика, могу еще много. Сложные или непонятные доказательства ненужны. Точнее, нужны только затем, чтобы разбираться в том, что на самом деле в них содержательного скрыто. Соответственно компьютерные доказательства совершенно бесполезны, так как не дают никакого понимания.
1. Точность тензорного умножения справа. Простейшие определения из теории категорий делают это естественным и очевидным утверждением (а раньше это был непонятный и сложный факт).
2. Негомеомофность сфер разной размерности. Правильный язык делает это очевидным, а неправильный превращает в кучу страниц невнятных вычислений.
3. Теорема Стокса. То, что раньше было набором слоных и неясно как связанный формул становится одной очевидной формулой.
Вот тебе совсем простой пример (так как математики ты, очевидно, не знаешь).
4. Определение абстрактного поля превращает задачу о удвоении куба, над которой бились тысячелетия, в упражнение для школьника.
>>188047
> Прости, но ты совсем дурачок (или толстый)
Ты в своём эмоциональном стиле.
> то о Бурбаки и Гротендике ты слышал только из википедии
...
Они слились, что сами же признали. После драки руками не машут. Если б их подход победил, математика, её преподавание и исследования были бы совсем другими.
Впрочем, хватит о них, это не предмет дискуссии.
> Сложные или непонятные доказательства ненужны.
Тогда давай отбросим доказательство великой теоремы Ферма, к примеру. Инбифо: кококо ано прастое.
А заодно и Перельмана. Потому что "простыми" такие вещи назвать трудно. Во всяком случае, в сравнении.
> Соответственно компьютерные доказательства совершенно бесполезны, так как не дают никакого понимания.
Чистый батруха как он есть. Можешь сколько угодно жаловаться и говорить, что я толщу, но это чистые эмоции, ничем не подкреплённые.
> так как математики ты, очевидно, не знаешь
Ты, кстати, тоже не знаешь. Когда-то давно года два назад мы решали задачу из Путнамовской олимпиады и в конце треда ты выдал "решение", которое просто кишило очевидными ошибками. То же самое ты продемонстрировал в треде про китайца. Ты ошибаешься на каждом шагу, в самых элементарных вещах. Зато любишь общие абстрактные термины.
Все приведённые примеры обсуждать смысла нет. Обобщение не облегчает решение задачи, а лишь "сворачивает" или "заменяет" ряд простых шагов в один сложный, но короткий. Чтобы, например, студенту доказать точность тензорного умножения справа, используя методы гомологической алгебры, ему нужно сначала разобрать, что есть группа, поле, кольцо, идеал кольца, топологическое пространство, выучить основные теоремы из этих областей, потом ещё въезжать и вырабатывать интуицию для понимания катов. Или ты считаешь, что каты можно наскоком выучить? Идея теории типов как раз заключается в том, что от простых посылок существует путь к решению (доказательству теоремы). Нахуй вводить сущности? Ты же просто пытаешься вытянуть себя за волосы.
Использование гомол. алгебры только внешне якобы "облегчает" доказательство, а на деле его сложность и трудоёмкость остаётся прежней.
Поэтому "куча страниц невнятных вычислений" -- это понятие СУБЪЕКТИВНОЕ. Но твой баттхёрт не даёт тебе этого понять.
Субъективно тяжело пахать землю плугом, но легко трактором.
>но легко трактором.
Перед этим изучив как им управлять.
>>188091
Что делается за 15 минут.
Водил современный трактор
>>188047
математики ты, очевидно, не знаешь
"Знать всю математику"
>>188152
Ой, бля, этого чувака я еще год-два назад смарел, очень своеобразный и не дурак, но какой-то слегка одиозный.
>>188154
> не дурак
У него куча работ по теории Ли. Не дурак однозначно. Это не Катющег.
> своеобразный
Он просто почти первый (с 2006-го года на тытрубе), кто эти темы стал затрагивать для большой публики. Но он далеко не единственный.
>>188047
>Определение абстрактного поля превращает задачу о удвоении куба, над которой бились тысячелетия, в упражнение для школьника
Покажи, плиз. В чём суть задачи? Как в ней используется коммутативное тело?
>>188152
Да ну, хуйня это и софизмы.
Он что, хочет сказать, что если взять побольше цифр чтобы посчитать пи*е, то внезапно может выясниться, что первая цифра там не 8? Или что первые две не 8.5? Или может первые пять не 8.5397? Хуйня же. Ну да, количество цифр, которые нужно брать в множителях больше требуемой точности результата. И чо? Да ничо, а у него какие-то гуманитарные прогоны из этого: "строка цифр растворяется в тумане неоднозначности..." Фубля.
>>188198
Ты прав. Я зашел в какую-то петушатню, а веду себя как среди нормальных людей.
[url]Что-то мне подсказывает, что платошлюха слился. Кукарекнул про душу и красоту что-то и слился. Чего и требовалось доказать.
>>187990
Если хочешь передергивать - упомяни лучше художников. Вот уж кто совсем стал не нужен при появлении фотографии и компьютера, не так ли?
>>188230
Подъебал я тебя насчёт знания математики. Ты ведь знатно тогда обосрался и даже сам признал, что не умеешь в точные формулировки
> Вот уж кто совсем стал не нужен при появлении фотографии и компьютера, не так ли?
В весьма значительной степени. Теперь практически невозможно стать миллионером при жизни как Дали.
Ещё примеры: Цирк почти ушёл в историю, бумажные книги отживают своё ...
Можно кратко изложить суть срача, чтоб было понятно непосвященному.
>>188248
Короче, в разделе есть два оппонента по части математики: я, конструктивист, и он, платонист.
Я выступаю за конкретное содержание в математике, которе выражается, если свести к одному слову, в алгоритмах.
Я вижу в математике только отношения и правила, а сами объекты (множества, пространства етц) без отношений и правил считаю пустышками. Я также считаю, что мозг заменяет пустоту, выраженную в незнании алгоритма, верой и опорой на опыт.
Он выступает за "красоту", интуицию и обосновывает веру тем, что вышеперечисленные мной объекты реально существуют, поэтому и не надо так париться с алгоритмами. Их существование он обосновывает тем, что у разных людей (математиков) представления о них сходятся.
Тред посвящён самой трендовой области современной математики, гомотопической теории типов, от которой у него, как он сам признался, баттхёрт. Это потому, что НоТТ в основе конструктивна и нацелена на формализацию и алгоритмизацию в первую очередь самых фундаментальных объектов математики - доказательств. В ТТ доказательство складывается в цепочку термов определённых типов, которая ничем принципиально не оличается от какой-нибудь привычной формулы, например, для корней квадратного полинома. В НоТТ адаптируется понятие гомотопии из топологии для установления равенства типов. Эта теория находится в разработке под начальством Воеводского, выходца из Совка, где, кстати, очень любили и сделали большой вклад в конструктивную математику.
Вобщем, этим занимаются теорем-пруверы типа coq'a, агды, изабеллы етц
Очевидно, что математика здесь сильно сливается с computer science и кодингом, к которым классические математики традиционно относятся с лёгким пренебрежением. От того и батруха. Представь, если тебе на замену постепенно готовят некий автомат, а для его обслуживания, если хочешь, тебе нужно, фактически, заново переучиваться и переквалифицироваться.
>>188254
Болею за тебя, тогда. Жаль, самому уже поздно разбираться во всей этой математике, школьные годы проебал
>>188255
Замечу, что у гомотопической теории типов нет полезного выхлопа, тогда как у нормальной математики он есть. НоТТ - это просто суходрочка на основания. Пока приличные люди пилят квантовую теорию поля, черви-фундаменталисты пишут миллионстраничные доказательства, что 2+2=4.
>>188256
Не знаю о практических применения гомотопической теории типов. Но если взять область шире, то сейчас обсуждается по крайней мере одно практическое применение пруверов. А именно - формальное доказательство корректности работы критически важных кусков программ и защищённых протоколов. Мне лень искать ссылку, но уже был случай, когда в результате попытки формальной проверки одного протокола была найдена уязвимость.
>>188254
С механизацией процесса доказательства - соглашусь. Но доказательство лишь инструмент проверки консистентности идей и положений. Математика не в этом. Ноты идут после музыки. Для того чтобы что-либо доказать надо об этом прежде всего подумать, вообразить, представить. А вот этого ни один алгоритм не сможет никогда.
>>188258
Да господи, model checking еще в 80-х родился. Вы не о том и это все зола. Суть математики - уметь видеть. А уж потом облачать в рамку того или иного формализма.
>>188260
>Да господи, model checking еще в 80-х родился.
Я не достаточно хорошо знаю детали старых подходов, но насколько я понимаю там оставалось больше пространства для человеческой ошибки.
>Вы не о том и это все зола.
Я говорил о практических применениях, а не о том нужны ли они.
>Суть математики - уметь видеть. А уж потом облачать в рамку того или иного формализма.
Хотя я с этим не так уж сильно не согласен (я считаю, что нужны и видение и формализм), но это вопрос вкуса. Если отвлечься от практических применений, то с внешней точки зрения разные видения математики это примерно тоже, что и разные стили музыки или живописи.
>>188259
Ну, человека тоже можно рассматривать как алгоритм, по одной из теорий.
>>188266
Человек способен действовать алгоритмически. Отождествлять его с алгоритмом - глупость и вульгаризм. На всякий случай: под понятием "алгоритм" я подразумеваю одну из детерминированных выч. моделей. (например детерминированную машину Тьюринга).
>человека тоже можно рассматривать как алгоритм, по одной из теорий.
По какой?
Вся ебаная теория платонистов строится на том, что человек это нечто такое с трансцедентальной апперцепцией. Ну построим мы человека из железа - он будет лучше всех решать задачи?
>>188254
> есть два оппонента по части математики: я, конструктивист, и он, платонист.
Ох блять. Здесь как минимум 3-4 анона с тобой спорили. Причем один из них (я, которого ты походу так и не отучился платонистом называть) подчеркивал, что он ни разу не платонист (а напротив, если хочешь знать, симпатизирую конструктивистам). Алсо, абсолютно не понимая смысла слова "платонизм", ты пытаешься подвести под него любую точку зрения, отличную от твоей, которая состоит в том, что когда будут изобретены крутые пруверы, человеческие занятия математикой и ее развитие как богатой человеческой творчески-интеллектуальной сферы деятельности станут якобы вовсе не нужны.
>>188245
>практически невозможно стать миллионером при жизни как Дали.
А Сафронов-то и не знал.
>>188257
Серьёзно вполне. Хассл -- необходимый шаг к изучению агды, например (даже синтаксис у них почти одинаковый). Это чистый ФЯП со статической типизацией.
>>188256
> как у нормальной математики
Платонист не палится.
>>188259
Взаимозацикленное утверждение, полагающееся на скрытый тезис, взятый за аксиому. Догадайся, какой именно.
>>188281
> Отождествлять его с алгоритмом - глупость и вульгаризм
Эмоциональный бред платониста. Это ещё надо строго доказать, что мозг не является Тьюринг-машиной.
>>188294
Да всё куда прозаичнее. Вся вера платонистов описывается одним словом: привидение Каспер: оно взаимодействует в физическом мире (открывает двери, пишет формулы на бумаге), но может обитать и в мире идей Платона, где "летают" множества (проходит сквозь стены). И я вообще удивляюсь, как можно быть дуалистом, если эта позиция полностью несостоятельна и была разгромлена уже множество раз. Но, видимо, дрочка на "красоту" сильнее.
>>188335
> (я, которого ты походу так и не отучился платонистом называть)
Атятя
И что я подразумеваю под плантонизмом -- читай выше.
> что когда будут изобретены крутые пруверы, человеческие занятия математикой и ее развитие как богатой человеческой творчески-интеллектуальной сферы деятельности станут якобы вовсе не нужны.
Это необходимое и неизбежное следствие настоящего тренда, нравится кому-то или нет. Никакие эмоции и вера в душу на тенденцию не повлияют.
>>188358
> Сафронов
> Художник
pick one
>>188248
ОП-хуй утверждает что вот-вот и компьютеры заменят математиков, на что ему в разных вариация отвечают почему это не так. На всех кто с ним не согласен ОП-хуй кидается как бешеный петух и называет платонистом (да именно так - в единственном числе)
>>188382
Щито поделать, десу. Тут уже и Гедель с Райсом проскакивали. Я могу еще про Re, CoRe сказать. И про проблему эквивалентности. И про... Не. ОП упоролся Хаскелем, Агдой с теорией типов и непроходимо убежден, что сие зохавает вселенную сделает математика - ненужным. Путая идеологию с методологией.
>>188361
И тут пришло зарени, что и как рисовать Художнику. Что мы имеем отсель и по наше время? Мы имеем Художника, который воплощает все свои замыслы, рисунок и композицию, само написание на холст в виде исполнителя в одном лице. Однако, в Музыке как важнейшем искусстве мы имеем совсем другое - композитор композиционирует, аранжировщик аранжионирует, испольнитель и певец исполняет на сцене. Тут еще и звукорежиссер притаился в углу, хотя есмь ключевая фигура в процессе. В итоге мы получаем продукт с вершин чартров и с чатлов, пацаки ликуют, ну а эцилопы в натуре в восторге.
Что же мы имеем в изобразительном искусстве? Он сам и жнец, и на дуде игрец, да еще жена беременная. Вместо картины и первоначального азмысла мы видим на холсте проекции Автора на обыденную повседневность. Поэтому, предлагаю: Художник должен работать и создавать картины в соавторстве с другим носителем мысли - Композиционером Картин, и даже с Концептуалистом. Возьмем Сафронова. Хороший Художник, но с воображением у него нихуя - дитя крестьян или что в этом роде. Ну совершенно не хватает голубой крови, ну хотя бы 0,5%. Но крестьянин не значит плохой. Среди Господ крестьянин очень даже гармонирует. Так к чему это... Сафронову нужен концептуалист, и созданные картины именовать и подписывать именно как творчество авторов: такая то картина, создана Ивановым-Сафроновым. Ну или картина маслом, концептуалист Перджельский, художник Сафронов. Это Гениально! - воскликнут поклонники таланта.
Дело в том, что у любого человека мозг под завязку набит определенными штампами и шаблонами поведения - это заметно у всех артистов и людей искусство, если внимательно приглядется. Мы называли это манерой письма, или исполнения, на деле же это границы того, что может данный автор. Выйти за границы будет трудно, и обычно будет безвкусица. Поэтому концептуалист - это тот, который видит будущую картину в более колоритном разнообразии, до каких высот не дойти самому художнику. Лучше назовем этого предтечу Композитором картин, чтобы выразить яснее.
В кинопроизводстве совсем по уму - есть первоначальный сюжет писателя, есть режиссер, есть сценарист, есть толпа народу, кто делает кинокартину. Получается хорошо или плохо. А то бы хотел Васян какой-нибудь все сам сделать и получить все лавры, бегая с одной камерой вместо оператора - все оскары в руки.
Я щитаю, что толпе бездельников - быть! Композиционеров тоже, пора открыть факультет в каком-нибудь столичном вузе.
>>188281
По теории Жюльена Ламетри и его последователей, конечно.
>>188393
>Это необходимое и неизбежное следствие настоящего тренда, нравится кому-то или нет.
Ок, нет проблем. Только странно слышать от человека с математическим образованием (я надеюсь) столь неприкрыто-вульгарные футурологические утверждения (ясновидящий в треде штоль?), да еще и снабжать их эпитетом "необходимый".
>>188388
>В кинопроизводстве совсем по уму
САМЫЙ ЛУДШИЙ ФИЛЬМ 3
Вообще кстати меня глубоко поразили твои охуительные познания о создании музыки.
мимо/mu/дак
>>187536
Вы тупой. Можно научить было комьютеры проверять доказательства и до Воеводского, который просто сделал многие доказательства конструктивными. (Писать составлять док-ва они, естественно, не научатся.)
Wikipedia-size maths proof too big for humans to check
Так звучит заголовок недавней новости на newscientist. Да-да, речь снова о тех самых пруверах, которые перевернут мир математики и многим клоунам с бумажкой и карандашом придётся подискивать себе новую работу.
Когда взлетит HoTT, разрабатываемая Воеводским и его командой, у большой доли старомодных математиков бабахнет попочка. Cобственно, уже бабахает.
Мы уже знакомы с одним большим фейлом классической матеши -- доказательством Мочидзуки гипотезы ABC, на которое все положили жирный хуй.
А вот если бы это сделал прувер, никаких вопросов не было бы.
Уже не за горами то время, когда быть Перельманом станет диковинкой, а всякие кодомакаки будут побираться на улицах, потому что и тех, и тех заменят автоматы, создаваемые бравыми компьютерсаентистами.
Так что, ты либо запрыгиваешь на Бэндвэгон, либо лососнёшь.
И учите Хачкель, посони!
http://www.newscientist.com/article/dn25068-wikipediasize-maths-proof-too-big-for-humans-to-check.html