Офигенно вам. Я бы тогда сразу писала на английском — и аудитория расширится и не придётся мудрить.

Двуязычный, и даже трехязычный текст - это хорошо. Берите пример с классиков XIX века.

Lost-in-TARDIS
"всё придумано не нами и до нас"
Ага, и в том числе и это.

Буквально просится идея книги, которую читают ровно одну жизнь. С самого детства и до последних дней старости. Такого я еще не встречал, зато видел эссе про не-человеческую литературу, написанную не-людьми для не-людей, произведения настолько сложные или настолько обширные, что люди не могут даже надеяться объять их пониманием.
И надо сказать, что это уже не совсем фантастика. 1976 - первое Computer-assisted proof, доказана теорема о четырех красках. Некоторые математики опасаются, что со временем большую часть доказательств будут делать программы, проверять которые тоже будут программы.

"Некоторые математики опасаются, что со временем большую часть доказательств будут делать программы, проверять которые тоже будут программы." - а другие этому радуются и учатся метапрограммированию.

Хотел написать про машущего ручкой Джойса, а тут уже.
С другой стороны, "Поминки"-то и действительно не нужны!

Матемаг
Это не технический вопрос, а принципиальный.

Что если в этой программе будет ошибка? Что если в проверяющей программе тоже будет ошибка? Математика всегда была единственной чистой наукой, которая претендовала на то, чтобы быть независимой ни от оборудования, ни от погрешности измерений, ни от конъюнктуры. Была.

Заяц
А что если математик ошибется?

*погрешность измерений ты тут вообще к чему приплел*

Заяц, а если в математическом рассуждении будет ошибка? В том-то и суть, что сначала вышлифовываются автоматические методы проверки программ, потом программы с их помощью, а потом на их основе теоремы автоматически доказываются. Чем это отличается от современной математики и вообще науки, где поздние утверждения и теории стоят на плечах тысяч ранних? Могут ли ранние ошибаться? Да. Поздние? Да. Ошибка в середине? Тоже да. Тогда почему же наука работает? Потому что проверяют, хех. Тут разница будет в том, что проверять будут методы проверки, а методы проверки будут проверять уже не с помощью исполнителя-математика, а с помощью исполнителя-компьютера. Замечу, что компьютер в роли исполнителя методов проверки доказательств теорем - надёжнее.

пока читал червя мня замучило это грёбаное fucked up которое применяется всеми везде и в любой ситуации. По контексту понятно что имеется ввиду, но на русский всегда переводится как-нибудь по особому.

Оказался в жопе - fucked up. Виновен в каком то серьёзном косяке - fucked up. Про кого-то говорят что он опасный для окружающих псих - fucked up. Обстоятельства сломали человеку жизнь - fucked up.

Lost-in-TARDIS
А что если ошибутся одновременно все математики? Но это ладно, тогда никто вообще ничего не заметит.
Что если ошибется ровно половина всех математиков?
Что если не ошибется только один математик, и этот математик - ты?

К тому, что стандартная оценка достоверности открытия в физике элементарных частиц - пять стандартных отклонений. Если накопленной статистики не хватает - сиди, копи дальше. Вот и получается, что физики зависят от многолетней бесперебойной работы БАК. Многие эксперименты поэтому и не состоялись - слишком долго набирать статистику.

Я еще хотел Гилеин теорический мир приплести, но это уже совсем непонятно будет.

Матемаг
И снова принципиальный момент. Ты неявно полагаешь, что компьютеры - точнее. Я... ну, скажем, ретранслирую мнение поколения, которое выросло, когда компьютеры только еще появлялись, соответственно, абсолютизировало возможности разума и его точность.

Как оно на самом деле?

А хрен его знает. Я после "Ложной слепоты" и еще пары книжек на вопросы типа "А как на самом деле?" и "Что есть истина?" реагирую улыбкой.

Впрочем, думаю, что практически, а не философски, проблему надежности как-нибудь решат. Да уже решают во всяких частных случаях. Коды Рида - Соломона, контрольные суммы, методика построения доказательства с нулевым разглашением. И так далее.

Понимаю вас про два языка. Иногда думаю такой дикой смесью немецкого, русского и английского, что лучше бы вообще не думала))

Заяц
Это риск, который мы принимаем и от которого мы пытаемся застраховываться, юзая научный метод, рациональность и перепроверяя свои открытия. Однако, несмотря на опасность, мы всё же с известной осторожностью идем вперед, потому что сидеть на месте из-за мизерной вероятности того, что мы все вдруг ошибемся - глупо.

А как физика элементарных частиц связана с возведением научного здания математики?

Заяц, в случае механических действиях - да, точнее. Например, в случае перебора с простыми эвристиками или в случае проверки математического доказательства.

Надо бы её всё же зачесть...

Эм, стой. Я же тут вроде как к человеческому разуму и склоняю всё! Просто из-за возросшей сложности теорем и доказательств, матаппарата в целом, напрямую генерировать и проверять доказательства уже неэффективно. Возможно, но баги быстро копятся, слишком много рутинной работы, а в доказательстве одна-единственная ошибка может порушить всю изящную конструкцию. Зато теперь можно работать с инструментами. Описать, как бы ты работал механически вот с этим участком задачи, а затем заставить выполнить эти действия микросхемного друга. Разница только в появлении одной прослойки из двух компонентов - алгоритма и исполнителя к нему, проги и компа. Да, оба компонента надо проверять. Комп - не математиково дело, а вот прогу всё равно надо будет проверять самому математику. В итоге мы имеем, что всё равно придётся делать умственные усилия на своеобразное доказательство - но уже доказательство работы программы, а не теоремы напрямую. Так сказать, через лемму делаем. Чем это не могущество человеческого разума? Или нам надо податься в докаменные века и в качестве инструментов использовать подобранные палки? Или даже от них отказаться, мол, только разум и природные способности, только хардкор?

Lost-in-TARDIS
"А как физика элементарных частиц связана с возведением научного здания математики?"

Я говорил. Математика считалась "чистой". Наукой, которая опирается только на разум. Строгой, однозначной. Идеальной, в каком-то смысле. (Вот тут я и хотел упомянуть Гилеин теорический мир из "Анафема" Стивенсона.) Это в физике есть погрешности и всякие условности, а в математике прямые либо параллельны, либо пересекаются. До недавнего времени, вопрос ошибок разума как-то не вставал. Введение дополнительной сущности - компьютера - нарушает изначальную чистоту концепции.

После того, как компьютерные программы окончательно слили человека в шахматах, появились шахматы адванс - дисцплина, в которой можно использовать помощь любой (как вариант - части) компьютерной программы. Но они пока так и не стали мейнстримом. Пока что в шахматы продолжают играть люди.

"мы всё же с известной осторожностью идем вперед, потому что сидеть на месте из-за мизерной вероятности того, что мы все вдруг ошибемся - глупо."

Это у нас просто такая юга сейчас. Это у нас такая юга...

В европейском Средневековье люди вообще никуда не шли - считали, что все и так хорошо, надо лишь бороться с дьяволом в себе. Сейчас "концепция изменилась", (с).

Но она еще не раз поменяется. Даже жаль, что у меня нет лишних трехсот-четырехсот лет - посмотреть, что потом останется от нашего времени.

Мы дети своего времени, которое ставит нам задачи и награждает усилия тех, кто работает в том направлении, которое нужно всему человечеству как целому.

Сейчас человечеству больше всего нужен фейсбучек и айфоны. Ну еще авианосцы, но это всегда так было. Первый оружейный стартап затеял еще Хайрем Максим - и добился оглушительного успеха. Науку сейчас тоже прилично поддерживают.

Последнее время, в некоторых кругах стали рассуждать, что на дне тоннеля эго на самом деле ничего нет. Что мы сами это всего лишь что-то, что кажется нам. Один из главных теоретиков этого подхода - Томас Метцингер.
Но я думаю, что эта концепция тоже пройдет - или изменится - так же, как все прочие.
Еще ни один солипсист не отказался от еды, воды, гигиены и работы на основании своего солипсизма. Если же и отказался, то был очень быстро отбракован.

"Это риск, который мы принимаем и от которого мы пытаемся застраховываться, юзая научный метод, рациональность и перепроверяя свои открытия. Однако, несмотря на опасность, мы всё же с известной осторожностью идем вперед, потому что сидеть на месте из-за мизерной вероятности того, что мы все вдруг ошибемся - глупо."

Я и говорю, что практически это все так или иначе будет решено.
Ну просто потому, что надо же куда-то идти. Система все равно продолжает двигаться вперед как целое, даже если у отдельных элементов будут какие-то свои соображения.

Матемаг
"Или нам надо податься в докаменные века и в качестве инструментов использовать подобранные палки? Или даже от них отказаться, мол, только разум и природные способности, только хардкор?"
Ты же понимаешь, что никто не будет так делать? Ну и я понимаю.
Нет, теперь инструментальная база сменилась окончательно. Возвращение к предыдущим этапам возможно только как форма искусства или хобби. Или в рамках решения какой-то специфической задачи. Например, группа выживальщиков хочет смоделировать способ восстановления индустрии после Большого Пиздеца с использованием исключительно камней и палок.
Хотя пока еще шахматы не проиграли адвансу. Но там концепция сложнее. Слишком много в этом истории значит внерациональное. А вот если бы это был не конфликт культур, а военное столкновение или чисто рыночная конкуренция, которую выигрывает самый эффективный, то адванс быстро съел бы шахматы.
И это очень любопытная деталь. Чем-то похоже на "Дознание" Лема.

Заяц
>>>Я говорил.
Ты не говорил, как это связано с математикой.

Наука, которая опирается только на разум - это не наука, которая использует только большой кусок неприспособленного органического желе, а остальное считает ересью.
Использование компьютеров ни чем не отличается от использования калькуляторов или органического желе. Никаких погрешностей и условностей, кроме тех, что точно так же может сделать человеческий разум, не появилось.
В самом основном процессе математики ничего не изменилось, кроме количества операций в секунду.

И, пожалуйста, не надо переводить спор в новую плоскость про то, куда идет человечество, подобные приемы - это демагогия чистой воды.
ЗЫ. А пример с шахматами был вообще ни к селу ни к городу.

Mikie
"суть проблемы века девятнадцатого, емнип"
Программа Гильберта это 1920-30ые.

>Отсюда растут ноги таких мерзких социальных явлений как переход от "каждый имеет право на свою истину" к "все истины равны".
Все истины несравнимы. Не придумали пока оператора, который в пространстве истин дает расстояние между ними.

Lost-in-TARDIS
>Ты не говорил, как это связано с математикой.
Надеюсь, теперь это стало яснее. Но если что еще не, я прокомментирую.

>Использование компьютеров ни чем не отличается от использования калькуляторов или органического желе. Никаких погрешностей и условностей, кроме тех, что точно так же может сделать человеческий разум, не появилось.
Дополнительные погрешности появляются
https://en.wikipedia.org/wiki/Pentium_FDIV_bug

>И, пожалуйста, не надо переводить спор в новую плоскость про то, куда идет человечество, подобные приемы - это демагогия чистой воды.
Это не демагогия, а философия. Или идеология. На уровне философии одного ответа нет. В отличии от математики и физики. То есть спор не сводится к решению некоторой задачи, где ответ либо "да", либо "нет", либо "ответа не существует".

Думаю, что на практическом уровне все будет доказано либо точно, либо настолько точно, что исключения не будут иметь значения. Но может быть и нет. И тогда для кого-то это будет такое же потрясение, как стала квантовая теория - операторы импульса и координаты не коммутируют и всё, а значит реальность всегда основана на неопределенности, которую никогда нельзя сделать менее строго заданного предела. Но потом все привыкли.

Так вот, на практическом уровне, скорее всего, больших проблем не будет. А на уровне философии - не знаю. Но именно на этом уровне человек всегда был свободен, свободен придумывать и представлять, на нем не было таких ограничений, как второе начало термодинамики, которое мешает нам извлекать энергию, или специфика СТО, которая превращает путешествия через космос в путешествия-в-будущее-в-один-конец.

Mikie
Почему же это не при чём?

>при чём тут расстояние?
Метрика - один из способов упорядочивания множества.

Какой у твоего пространства истин будет нулевой элемент?

>Недопустимый редукционизм.
Раз уж критикуешь, предлагай что-нибудь.

"Нет, теперь инструментальная база сменилась окончательно. Возвращение к предыдущим этапам возможно только как форма искусства или хобби." - ну вот ты сам и ответил. Часть математиков хочет сохранить математику как искусство. Не понимая, что делая математику с помощью программирования, они тоже делают искусство. Другое, конечно. Это уже не руками лепить, а 3D-модель объекта рисовать. Но и возможности открываются гораздо шире.

> Дополнительные погрешности появляются

Ничем не отличается от "ой, я случайно сотцатую итерацию и все знаки числа пи, начиная с пятьсот пятого зафаршмачены на ближайшие двести лет".
Или от опечатки в таблицах Брадиса.

Более того, конкретно fdiv-баг на доказательное программирование вообще не особо влияет, потому как ему от числодробилок вообще ничего не надо.

Относительно же охуительных доводов про компьютерные доказательства, в которых нет души, они не внушают любви и не дарят радости - вам вообще шашечки или ехать? (энивей, возможность стать самому себе компьютером и пройти генерированное доказательство от строчки к строчке никуда не девается)