Как стать автором
Обновить

Комментарии 202

Ну вот собственно в этом и заключается будущее математики — перевод всей математики в некоторое формальное машинно-поминаемое представление и применение методов искусственного интеллекта — как символьных вычислений для строгой проверки, так и нейросетей — для эвристического поиска нового.
Я не сомневаюсь, будет найдено очень много интересного:)
А само создание такой базы знаний привнесет очень много нового и интересного в исследование Искусственного Интеллекта.
Насколько я понимаю, это скорее прошлое математики, чем её будущее. Полной формализации математики препятствует вторая теорема Гёделя о неполноте. В любом случае останется некий творческий элемент. Но я могу понимать неверно.

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

Вот это все и интересно. Может быть, компьютер сможет «трассировать» систему аксиом до очень высокоуровневых математических абстракций, и «включая» и «отключая» те или иные аксиомы, смотреть как изменяется сама математика на выходе. Я с трудом представляю себе возможности таких систем, но чувствую что там нас ждет немало открытий.
А если еще сюда подключить квантовые вычисления?

Скорее всего упрётся в проблему останова (квантовый кстати тоже)

Разве в этом смысл? Она ведь говорит, что если система непротиворечива (уже), то её средствами нельзя доказать этот факт. Это только значит, что мы не можем знать, все ли противоречия мы устранили или нет.

А я понимал это так, что в непротиворечивой системе всегда есть истинные утверждения, которые нельзя доказать в рамках этой системы. Грубо говоря, мы никогда не сможем доказать ВСЕ теоремы.

Это первая теорема. Вторая даёт один особый пример такого утверждения — об отсутствии в системе противоречий.
А я понимал это так, что это об аксиомах… т.е. для построения теории нужны аксиомы, утверждения, доказательство которых в рамках этой теории не рассматривается, невозможно и т.д.
Продемонстрируйте пожалуйста противоречивое утверждение булевой алгебры.

Ну, не знаю… Тут требуется что-то довольно искусственное.


Пусть существует бесконечный ряд утверждений со случайной истинностью. Требуется проверить, что "аккумуляторное или" взятое по этому ряду является истиной.

В ней нет «случайных истинностей», есть формулы из истино/ложно…

Ну, хорошо. Пусть для каждого утверждения существует следующее за ним. Утверждение является истиной, если следующее ложно и ложно, если следующее истинно. Вопрос истинно ли самое первое утверждение.

Даю подсказку. Булева алгебра, как и огромное количество других формальных систем, непротиворечива.

Оке.

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

Да, я уже понял свою ошибку.

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

Грубо говоря игра идёт на том, что такое «самое большое натуральное число, описываемое фразой не более тысячи букв». В самой это фразе ещё нет криминала (но уже почти), но стоит добавить единичку, чтобы получить «самое большое натуральное число, описываемое фразой не более тысячи букв плюс один»… и всё рассыпается.
Здесь не удаётся формализовать, что значит фраза «описывает» число (в хорошем смысле). :)
ИМХО, речь в статье всё же не про автоматическое доказательство произвольных теорем (тут мы действительно упрёмся в теорему о неполноте), а про автоматическую верификацию представленных математиками доказательств — в которых все утверждения обязаны быть формально доказуемыми.
НЛО прилетело и опубликовало эту надпись здесь
А как проверить и убедиться, что человек не принимает диван за леопарда?
НЛО прилетело и опубликовало эту надпись здесь

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

В задачах поиска есть конкретное решение для конкретного случая. Здесь вопрос цены — очень дорого делать алгоритм на «каждый» запрос. Очень дорогая оценка верности алгоритма(% эффективных решений) и его производительности для каждого случая. Т.е. алгоритм есть, проверить можно, но не целесообразно.
Ага, если такой диван в магазине или в квартире то понятно что человек легко определит, что это скорее диван или просто вещь, чем живой зверь. А вот если в лесу там увидеть часть дивана из-за кустов то обычный человек вряд ли успеет сообразить что там не только ягуар может быть.
После чего наступит технологическая сингулярность.
так и нейросетей — для эвристического поиска нового.
Я не сомневаюсь, будет найдено очень много интересного:)

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

В компьютерных доказательствах могут возникнуть утверждения «очевидно, что из А следует Б». А для проверки этого надо будет взять 100 суждений, и только сопоставив эти 100 суждений, можно будет сделать этот вывод. Поэтому, как говорится, — хочешь, верь, а не хочешь — проверяй сам. :)
Вы никак программу Гильберта изобрели?
Отличные примеры того, что люди подошли к пределу когнитивных способностей мозга. Ну и косвенная демонстрация пропасти между пиковыми возможностями и степенью использования мозга большинством людей.
В математике люди очень успешно архивируют знания. Теорема Лагранжа из теории групп была результатом с доказательством на 45 страниц, а теперь помещается в один параграф.

Конечно, должны быть пределы эффективности архивирования, но пока я сохраняю оптимизм :)
Возможно в этом параграфе каждое второе слово термин, который понятен математикам, потратившим годы на образование, а не среднестатистическому школьнику?
На удивление, именно новое доказательство понятно школьникам. Я как раз две недели назад преподавал в математическом лагере и объяснял старшеклассникам теорему Лагранжа. Было очень интуитивно понятно.

Когда-то давно только самые образованные люди могли сложить дроби 1/7 и 1/11. И это «когда-то давно» было всего пару сотен лет назад :)
угу, а самые необразованные пользовались двенадцатеричной системой, считали яйца дюжинами, знали что в футе 12 дюймов и не парились. Интересно, если они не знали дробей в принципе, то как они делили пищу на заданное количество участников, строили фахверкеры?
Возможно, ближайший путь — делать электронные примочки для мозга: память и т.д. Появятся (за деньги) сверхчеловеки, а остальные будут киберпанками, которые будут жить на мусорных свалках. Такое было лет 500 назад: феодалы питались хорошей едой и были на голову выше черни, которая ела картофель и хлеб.
Возможно, эти люди уже подошли к пределу своей цивилизации, за которым будет её гибель. «Эх, яблочко, куда ты котишься? К чёрту в лапы попадешь — не воротишься.» Природа отдохнёт 100-200 миллионов лет, пока не появится очередной двуногий ублюдок, который овладеет технологиями. :)
Виден эмпирический закон: с новыми открытиями и технологиями существовать нормальному человеку становится ещё противнее.
Возможно, ближайший путь — делать электронные примочки для мозга: память и т.д.

Сейчас такая примочка — это смартфон с доступом в интернет и мгновенной телефонной связью с почти любым человеком (или, как более ограниченный вариант — смарт-часы). С нейроинтерфейсом, конечно, до сих пор грустно, но глаза и пальцы хоть как-то да справляются с вводом-выводом информации.
И не похоже, что в ближайшее время будет изобретён нейроинтерфейс, который нужно будет подключать специальной операцией. А ввод пальцами (или подобным методом) доступен почти каждому. Поэтому отдельные "сверхлюди", скорее всего, не появятся тем путём, что описан в киберпанке.

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

Если я ничего не путаю, это было что-то вроде энцефалограммы, несколько лет назад. Электроды, которые нужно смачивать… Непрактично.
Пока что речи не идёт о массовом применении таких устройств, к сожалению.

НЛО прилетело и опубликовало эту надпись здесь
Автор с вами как раз согласен :) Проблема в том, что даже лучшие математике в своей области не знают наверняка, верны ли их результаты. О каком понимании идей тогда идёт речь?

Автор предлагает использовать компьютеры для формальной верификации математических доказательств, а не для избавления от всей исследовательской деятельности.
Формальную верификацию вряд ли можно рассматривать как вердикт. В противном случае, это только может навредить математике. У Имре Лакатоша по этому поводу есть популярная книга с рассуждениями о формальных системах доказательств. Мне кажется, книга вполне актуальная.
Формальная верификация не вердикт, эксперты не способны отличить верное доказательство от ложного, доказательства либо не публикуются целиком, либо публикуются не полностью — получается магия какая-то, а не математика.
Системы формальной верификации как правило основаны на маленьком ядре, которое считается достаточно надежным. Ошибки вне этого ядра не могут допустить неправильное доказательство, только не пропустить правильное.
линейные операторы Гекке, определенные на канонически изоморфных группах когомологий, коммутируют с каноническим изоморфизмом

Когда читаю подобные математические высказывания, в голове что-то щелкает и через 5 секунд я срываюсь на смех.
Вот уж не подумал бы, что здесь столько математиков, понимающих этот язык…
НЛО прилетело и опубликовало эту надпись здесь
Это не смех над неизвестным, а смех от. От осознания того, насколько заковыристые языковые конструкции может порождать отдельный вид человеческой деятельности. А в математике это наиболее ярко выражено. Мне нравится читать такие вещи, а смех — это только моё личное внешнее проявление моей внутренней реакции. Подобное я испытывал при чтении некоторых коанов. Это скорее восхищение. Когда ребенок проявляет смекалку, не свойственную его возрасту, является ли смех его отца — смехом над ребенком?
Таким образом, часть доказательства остаётся скрытой. И возможно навсегда останется скрытой.
А затем мы получаем ответ 42 и не можем понять, как он был получен. Дуглас Адамс — гений!
> А затем мы получаем ответ 42 и не можем понять, как он был получен.

Почему «не можем понять», если есть оригинальное математическое обоснование?

«You mean that's it?» said Ford.
«That's it.»
«Six by nine. Forty-two.»
«That's it. That's all there is.»

Я имел ввиду сам процесс работы программы, которую считал Вычислитель семь с половиной миллионов лет.

6 x 9 = 54

Э-кхм. Моя цитата была точной. Ничего нового нет в том, что вы нашли «ошибку». Вопрос в том, та же ли математика использовалась в Вычислителе?

Проблема не в том что в цитате есть ошибка, а в том что вы не понимаете ее смысл:


После того как был получен Ответ на Главный Вопрос, Артур пытался узнать в чем же собственно заключается Главный Вопрос. Так как он был последним сохранившийся элементом Земного компьютера, Артур решил вытащить Главный Вопрос из своего подсознания. Для этого он в случайном порядке стал вытаскивать буквы из мешочка для Scrabble, в итоге у него получилась фраза "What do you get if you multiply six by nine?" Но этот вопрос не подходит под Ответ, а значит настоящий Главный Вопрос остался загадкой. Почему так вышло читайте в комментарии ниже ...

> Так как он был последним сохранившийся элементом Земного компьютера, Артур решил вытащить Главный Вопрос из своего подсознания. Для этого он в случайном порядке стал вытаскивать буквы из мешочка для Scrabble

Вот! Вы точно описали суть той математики, что использовалась в этом доказательстве.

А вот предположение об её неверности уже является чистейшим артефактом нашего современного подхода. И речь не о тривиальностях вроде тринадцатеричной системы: мы не знаем, для Главного Вопроса то ли умножение, что у нас? те ли числа? и так далее. И пока мы не знаем, что именно и как было искажено вторжением — см. исходный пост. Может, вопрос искажен, а может, что-то другое?
Тут ещё проблема в том, что значит, что кому-то кажется, что он понял смысл? К примеру, есть такой эффект, как ложные воспоминания. Кто-то считает, что это было, а на самом деле не было.

А по основанию 13?

"Шесть на девять на самом деле пятьдесят четыре; ответ заведомо неверен, потому что вопрос был неправильно рассчитан. Программа на «Земном компьютере» должна была работать правильно, но неожиданное прибытие Голгафринчанов на доисторическую Землю привело к ошибкам ввода в систему и вычислению неправильного вопроса (из-за правила: мусор на входе — мусор на выходе). Поэтому вопрос в подсознании Артура был неверным все это время."
The restaurant at the end of the Universe by Douglas Adams


"Я, может быть, покажусь довольно скучной личностью, но я не использую тринадцатеричную систему в своих шутках" Douglas Adams

Спасибо за перевод презентации.
Следуя логике повествования внесу мелкую правку в перевод :)
Вместо «Формальные доказательства авторства следующих математиков: Gonthier,… и доказательство Théry теоремы Feit–Thompson»
Нужно «Формальное доказательство Gonthier, ..., Théry теоремы Фейта-Томпсона».
Подразумевается данная работа этого коллектива авторов.
Спасибо, поправил!
В 2019 исследователь искусственного интеллекта Christian Szegedy сказал мне, что через 10 лет компьютеры будут доказывать теоремы лучше, чем люди.
На Хабре половина читателей смело могут себя объявить исследователями искусственного интеллекта. Это я к тому, что собственно сами исследования ИИ находятся в предельно зачаточном состоянии и использовать заявления таких исследователей для предсказания в будущем это плохая идея. Научился строить линейные модели — исследователь, научился чему нибудь из ML — исследователь.
Математику я бы определил как науку построения непротиворечивых моделей окружающей среды. Математики еще любят чтобы такие модели были красивыми. Т.е. чтобы найденные модели могли быть применены к максимально большому количеству типов объектов как можно более простым образом. Но сегодня основной рост в областях математики, которые строят модели не окружающей среды, а на основе уже существующих моделей в математике. В результате при некотором злоупотреблении математика неконтролируемо разрастается и вширь и вглубь. В результате появляется своего типа DDoS на человеческое сознание, на человеческое понимание и человеческий интерес к математике. Я бы назвал это основной проблемой математики. И уже потом идут сложность, объемы и ошибки.
Но наиболее почетной и востребованной способностью и вызовом математики я бы назвал создание наиболее фундаментальных моделей именно природного физического окружения.
И да, математика, сколь сложной бы она не была, напрямую к ИИ не имеет никакого отношения. У математики свой набор «популярных» моделей. И свой круг интересов. Про «популярные» работающие модели общего ИИ пока ничего не известно.
Математику я бы определил как науку построения непротиворечивых моделей окружающей среды.

Это физика, математика она про отношения вещей между собой, вообще любых вообразимых вещей в любых вообразимых взаимоотношениях.

Математика — это просто формальная система (вообще говоря, можно придумать сколько угодно таких систем). Благодаря этому, математика не привносит никакой новой информации при математической обработке (имея скорость и время путь уже заложен в них изначально), но лишь производит её преобразование из одной формы в другую. Таким образом, математика — это цепочка тавтологий. Очень интересен вопрос, почему именно наша математика подходит для физики (можно, вообще говоря, придумать такую формальную систему, что она на физику может и не лечь). Судя по всему (как писалось в Техника-Молодёжи в 90-е), это получается посредством констант (и того, что наша математика всё же строилась на основе реального мира).
Так как математика формальная система, то с ней отлично работает компьютер (хотя бы методом перебора вариантов операций мы можем получить новые теоремы). Он по сути оперирует символами (за которыми ничего не стоит) по определённым правилам. Поэтому автоматически доказывать теоремы и выводить новые компьютер однозначно может. Проблема только в том, как заставить компьютер вскрыть именно нужную цепочку, зная теорему (конец цепочки) и исходные данные (начало цепочки).
Проблема в интерпретации символов сгенерированных компьютером. Компьютер может легко проложить путь доказательства от А к В через Б. Но он не способен сгруппировать выкладки, сделать обобщение чтобы перейти от частного к общему. У нас есть человеческий язык, с помощью которого мы абстрагируем понятия вводя новые, машина этого не может. Вот что ей задали, на основе этих символов она и докажет.
Но он не способен сгруппировать выкладки, сделать обобщение чтобы перейти от частного к общему.


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

Мой вузовский диплом выглядел так: была взята реальная научная статья соавтора моего руководителя, выкладки перепроверены… и оказалось, что в одном месте перепутанный знак (самая типичная ошибка!) привёл к неверному результату… просто раскопок этого (и отчёта с исправленными результатами) оказалось достаточно для дипломной работы.

Да, это было давно (статья была за конец 80-х, кажется — какие-нибудь Mathematica/Matlab/etc. были ещё недоступны). Но и сейчас — можно сверить ими, например, формулы в начале и конце цепочки преобразований, но это надо их вырезать, ввести, понять как проверять (подставлять контрольные значения и т.п.)

Если автоматизация «всего лишь» обеспечит

1) Автоматизированный перевод содержимого статей (в идеале — из печатной формы, но годится и Word/LaTeX/etc.) в представление, пригодное для анализа,

2) Воспроизведение сделанных выкладок и выводов, с проверкой выкладок и их допустимости (как, например, проверка областей определений — ещё одна очень распространённая проблема),

и нормальный ход работы с системой будет: скормить статью — поотвечать на пачку глупых вопросов системы — подождать вывода, уже это будет огромным шагом вперёд.
Благодаря этому, математика не привносит никакой новой информации при математической обработке

Чем открытие второго закона Ньютона принципиально отличается от открытия топологических пространств?

Тем что открытие второго закона Ньютона позволяет вам провести опыт, который подтвердит его или опровергнет.

Можно, наверное представить себе вселенную, где он не действует.

Открытие топологических пространств само по себе не даёт нам никаких гопотез для проверки.

Они любо согласуются с аксиомами, либо нет — и всё.

Чем аксиома F=ma отличается от аксиом топологии? Я могу найти процессы в природе, которые описываются в терминах аксиом топологических пространств, поставит ли это аксиомы топологии в один ряд с аксиомами Ньютона?

Поставит, когда выводы из этих аксиом будут иметь предсказательную силу в наблюдениях.

Чем аксиома F=ma отличается от аксиом топологии?


Тем, что она соотносится с физической реальностью (а может и не соотноситься — можно ведь написать и F=ma^2 или ещё что, только это будет верно математически, но не физически), а не является преобразованием букв (помните у Арнольда — «производная — это штрих. результат штриха для разных функций смотрите в таблице»).

поставит ли это аксиомы топологии в один ряд с аксиомами Ньютона?


Нет, не поставит. Это лишь инструмент. Вот если вы откроете новую сущность к которой примените топологию, то вот эта сущность и её взаимосвязь с другими сущностями в один ряд с Ньютоном, может, и встанут. Но сама топология лишь преобразование, инструмент. Более того, если расчёт по этой топологии с реальностью не совпадёт, можно будет ставить вопрос о корректности применения топологии в данном случае.
Чем аксиома F=ma отличается от аксиом топологии?
Тем что это не аксиома. Это эмпирическое правило, которое было проверено тысячи раз и которое всегда выполнялось… до тех пор пока не посмотрели на Меркурий.

Там, правда, было два Ньютоновских закона замешано — и конкретно F=ma «устоял». Но это не значит, что он является аксиомой, в то время как F=G m₁ m₂ / r² — не является.

Они оба имеют одинаковый статус, просто чтобы согласовать наблюдения с теорией оказалось проще пожертвовать вторым.

Я могу найти процессы в природе, которые описываются в терминах аксиом топологических пространств, поставит ли это аксиомы топологии в один ряд с аксиомами Ньютона?
Нет, не поставит. В этом случае аксиомы топологии встанут в один ряд всего лишь с операцией умножения, использованной в законе F=ma. А вот в ряд с законами Ньютона встанет уже непосредственно само выражение, описывающее, с помощью этих аксиом, некое физическое явление.
Чем аксиома F=ma отличается от аксиом топологии?

Вам уже ответили, но повторю. Отличие в том, что законы Ньютона — не аксиома. Это модель, построенная на эмпирических наблюдениях.


Отличие настолько фундаментально, что эти вещи можно считать условно противоположными.

Второй закон Ньютона очень и очень не прост. Чтобы его ввести потребовались две новых (!) сущности. Масса и сила. О, не думайте, что масса — это количество вещества и тут всё очевидно. Это не так. Масса — это вообще не вещество (потому в LT-системе единиц имеет размерность метр в кубе делить на секунду в квадрате — на этом моменте 99% людей офигевают и кричат, что этого не может быть никогда. Но это только потому, что они путают количество вещества и его способность к инертности, а это совершенно разные вещи). Масса во втором законе Ньютона — это способность вещества быть инертным (а в третьем — способность порождать гравитацию — это физически разные массы, но константами их можно сделать взаимозаменяемыми в формулах). До введения такого ой как непросто додуматься. Сила тоже новая категория. Это мера воздействия. Эти две величины, вообще говоря, нифига не интуитивно понятные. Вот эта связь и была введена (получена) Ньютоном. И она нашла отражение в реальном мире и позволила выполнять расчёты.

А топологические пространства всего лишь порождение формальной системы. Там ещё много чего можно породить.

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

Вы комментировали:
не привносит никакой новой информации при математической обработке


Обработка/вычисление F=ma никакой информации не привносит. Но сама идея ввести массу и силу новую информацию привносит (теперь вы с их помощью описываете реальность и, более того, измеряете эту реальность). Законы Ньютона гениальны не математикой (тут обычное умножение), они гениальны введёнными сущностями и их взаимосвязями. А с точки зрения математики это тривиальщина (одна величина равна произведению других — что может быть банальнее?).

, а топология это выдумка кого-то ещё


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


Килограмм нужен чтобы был Ньютон. Нет Ньютона — нет и килограмма.

Благодарю за таблицу и, собственно, информацию об LT-системе.
Кстати, если кому-нибудь захочется что-то про неё почитать, я нагуглил тут некий doc-файл: http://vev50.narod.ru/LT_.doc


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

Массы пропорциональны. Нам повезло или математики предложат формализм, объясняющий почему?

Так уж случилось, что в нашей реальности это так. Вас же не удивляет, что расстояние есть скорость умноженная на время. Почему не квадрат скорости? :) Ну вот так вот. :)
Чтобы его ввести потребовались две новых (!) сущности


Вообще, нет. Т.е. когда-то Ньютон может и вводил (вовсе не всё из того, что он вводил оказалось правильным, так массу он предлагал аксиоматические определять как плотность*объём, что такое «плотность» при этом умалчивалось), но с современной точки зрения плодить сущности нет нужды. Вводится просто масса, как мера инертности, потом импульс — и сразу получается сила. Собственно, второй закон зачастую удобнее рассматривать просто как определение силы — так он гибче и универсальнее. Хотя, обе формы эквиваленты, конечно.

а в третьем — способность порождать гравитацию

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

— и конкретно F=ma «устоял».

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

потому в LT-системе единиц имеет размерность метр в кубе делить на секунду в квадрате

там автор банально константу притяжения единицей объявляет (примерно как пи «в военное время» равно четырём. ну ладно, не совсем так, но близко). При это сама константа никуда не девается, а уходит в определение массы, т.е. его «масса» — уже не обычная масса. В принципе, ничего крамольного в этом нет, есть много разных систем единиц. НО, всегда надо помнить что стоит в их истоках, и что все полученные в них результаты надо преобразовывать обратно в физические величины, где они только и имеют смысл. А судя по объему обрамляющей графомании, автор про это забывает и выдаёт своё «открытие» за новое откровение в науке. Фричеством попахивает.

Upd:
Посмотрел внимательнее — так и есть. Автор выкидывает константу притяжения G, объявляя G=1. Но игнорирует тот факт, что тем самым он нарушает равенство гравитационной и инерционной масс, которые становятся разными величинами с разными размерностями. Что не мешает ему всё равно «по старинке» их приравнять и строить из этого «выводы». Там описанное даже не является полноценной системой единицей. Просто 100% фричество.

Вас же не удивляет, что расстояние есть скорость умноженная на время

Всё с точностью наоборот, это скорость по определению — расстояние, деленное на время.
Вообще, нет.


Вообще-то, вы именно две сущности и ввели: «Вводится просто масса, как мера инертности,...» — это сущность и есть.

Третий закон Ньютона о другом совсем.


Да, по инерции написал.

И их наблюдаемое совпадение


Их наблюдаемое совпадение — результат выбора системы единиц.

а уходит в определение массы, т.е. его «масса» — уже не обычная масса.


А вы никогда не пользовались СГС? Гляньте-ка там, например, закон Кулона. Сравните с Си. Задайте себе вопрос, а куда же делись 4*пи*епсилон0? Вот здесь ровно то же самое. Вообще, физика зависит от систем единиц крайне серьёзно. У Китайгородского в «Электроны» (насколько я помню, там) было объяснение как процесс внедрения новой системы единиц происходит и к чему приводит в итоге. Посмотрите, это действительно очень интересно. В школе и в институтах не рассказывают.

там автор банально константу притяжения единицей объявляет


При построении системы единиц это абсолютно нормально.

А судя по объему обрамляющей графомании, автор про это забывает и выдаёт своё «открытие» за новое откровение в науке. Фричеством попахивает.


История LT-системы началась совсем не с этого автора. :) И да, эта система абсолютно корректная. Только что очень неудобная для практического использования. Зато очень удобная для сравнения разных величин и построения выводов разной степени истинности.

Всё с точностью наоборот, это скорость по определению — расстояние, деленное на время.


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

Вообще-то, вы именно две сущности и ввели: «Вводится просто масса, как мера инертности,...» — это сущность и есть.

Ну а если импульс считать, то уже три сущности появляется. А момент импульса — уже 4 :) И так до бесконечности.
Просто достаточно именно одной сущности, все остальное выражается через нее. Хотя, для большего прояснения физических вопросов, действительно оригинальное введение Ньютона через силу не потеряет актуальности никогда. Потому его до сих пор и преподают.

История LT-системы началась совсем не с этого автора. :)

Значит были фрики и до этого автора.

И да, эта система абсолютно корректная.

Нет, читайте выше.
Сами же пишите, что была введена новая сущность (масса). Без нее: кг или его эквивалента — никак. А автор, грубо говоря, предлагает кг объявить за единицу, вот у него и остается LT

Вообще, физика зависит от систем единиц крайне серьёзно.

Физика НЕ зависит от систем единиц.

Потому вам совершенно не требовалось давать определение скорости.

Это вам надо давать определение понятия «скорости», когда вы говорите, что расстояние — это скорость*время. Иначе это просто слова ни о чём. В реальном мире именно скорость является «вторичной» величиной, определяемой на основе «первичных» времени и расстояния, в обратную сторону это не работает
Ну а если импульс считать, то уже три сущности появляется. А момент импульса — уже 4 :) И так до бесконечности.


Ну так и что? Сущности введены, как я и говорил.

Нет, читайте выше.
Сами же пишите, что была введена новая сущность (масса). Без нее: кг или его эквивалента — никак. А автор, грубо говоря, предлагает кг объявить за единицу, вот у него и остается LT


А зачем он вам, если он выражается через метры и секунды? Например, от калории же избавились, заменив на Джоуль и пересчитав константы. Здесь тоже самое. Килограмм — это не сущность, это единица измерения сущности.

Физика НЕ зависит от систем единиц.


Это физическая реальность не зависит, а физика зависит. Пример с электрической индукцией в СГС и в СИ ниже. А ещё, потому что, например, значения констант и соотношений зависят от точности измерений базовых величин (тех, что выбраны основными). В результате от выбора базовой величины зависят все производные величины и константы переходов. Грубо говоря, если вы возьмёте за основу процесс (скажем, магнитное действие тока) и точность измерения силы (а, следовательно, и тока) окажется низкой, все соотношения так же разбегутся. Вот тут почитайте, как и что получается. Так же сам вид формул зависит от выбранной системы единиц, например, где-то у констант появится размерность, да и значения изменятся. Или появятся новые константы — поляризация вакуума, например.

Это вам надо давать определение понятия «скорости», когда вы говорите, что расстояние — это скорость*время. Иначе это просто слова ни о чём.


Конечно, спорить со своим воображением можно и даже удобно, только вот зачем? ;)
В исходном сообщении речь шла о том, почему массы пропорциональны. Мой ответ сводится к тому, что, вообще говоря, ничего удивительного в этом нет — не удивляет же нас, что чтобы получить расстояние нужно умножить скорость на время (а не на время в квадрате, например). Как видите, я никаких определений не давал и не планировал.

Значит были фрики и до этого автора.


Ну а куда же без них? У нас тут полно народу, бросающихся что-либо опровергать, критиковать и оспаривать с твёрдой уверенностью своего знания физики и что они поняли вообще о чём речь и что вообще происходит.

Посмотрел внимательнее — так и есть. Автор выкидывает константу притяжения G, объявляя G=1. Но игнорирует тот факт, что тем самым он нарушает равенство гравитационной и инерционной масс, которые становятся разными величинами с разными размерностями. Что не мешает ему всё равно «по старинке» их приравнять и строить из этого «выводы». Там описанное даже не является полноценной системой единицей. Просто 100% фричество.


Нет. В СИ равенство этих масс задано как раз константами (этой самой постоянной Кавендиша). Ничто не мешает их просто положить равными, убрать константы и дальше из всего этого исходить при построении системы единиц, что и делается в той статье.
Посмотрите, в СГС вообще нет диэлектрической постоянной вакуума (она мало того, что число, так ещё и с размерностью). Почему? Потому что выбором системы единиц от неё можно избавиться. LT-система существует не одно десятилетие, так что не волнуйтесь, ошибки там нет (насколько я помню, ещё Фарадей указывал, что достаточно лишь метра и секунды — я специально нашёл лет 10 назад его труды и там это было — если найду ссылку, покажу). Просто подставьте в формулы силы размерности массы и размерность силы у вас совпадёт и для гравитационной и для инерционной формул. Никаких коэффициентов не потребуется.

Видите ли в чём дело, разговор с вами не имеет смысла, пока вы не преодолеете инертность мышления, перестанете кивать во фричество (вы настолько уверены в себе, чтобы критиковать то, что пока ещё даже не понимаете?) и задумаетесь о системах единиц, размерностях и коэффициентах более глубоко.
Я вам почему советую поглядеть на СГС? Потому что:
1) она авторитетна (вы не будете подозревать обмана и ошибок на каждом шагу);
2) она разительно отличается от СИ подходом и физическим смыслом величин;
3) вы увидите, как пропадают совершенно привычные в СИ вещи и меняется размерость величин. Скажем, в СГС электрическая индукция и поле имеют одинаковую размерность. В СИ нет, там индукция принципиально иное.

P.S. LT-систему придумал Бартини. О чём и доложил в Бартини Р.О. Некоторые соотношения между физическими константами // Доклады Академии наук СССР. – М.: АН СССР. – 965, том 163, No 4, с .861 – 864. и в Бартини Р.О., Кузнецов П.Г. О множественности геометрий и множественности физик./Проблемы и особенности современной научной методологии. – Свердловск: АН СССР, Урал. науч. центр. – 1978, с .55-65.

А то, что на ней спекулируют, это уже не его вина.
А зачем он вам, если он выражается через метры и секунды?


Нет, не выражается, по крайней мере «вывод» в той статье — глубоко ошибочный, выше я вам написал, почему.

не удивляет же нас, что чтобы получить расстояние нужно умножить скорость на время

а что тут должно удивлять, если это простой результат соглашения? Люди между собой договорились, что v=s/t. Это не фундаментальный закон природы, а просто результат следования единой терминологии. Как пример, со всех сторон неудачный, и в каком-то смысле даже вредный.

Ничто не мешает их просто положить равными

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

Я вам почему советую поглядеть на СГС?

СГС построена корректно, «LT система» — нет.

LT-систему придумал Бартини. О чём и доложил в Бартини Р.О. Некоторые соотношения между физическими константами // Доклады Академии наук СССР. – М.: АН СССР. – 965, том 163, No 4, с .861 – 864


Это пример того как фрик пролез в академический журнал.
Весьма показательно, на самом деле.
Нет, не выражается, по крайней мере «вывод» в той статье — глубоко ошибочный, выше я вам написал, почему.


Ерунду вы написали, вот что.

Мешает их разная физическая природа.

Если вы убираете константу, массы автоматически становятся неравными и разной размерности.


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

Это пример того как фрик пролез в академический журнал.
Весьма показательно, на самом деле.


Думаете, в 1965 легко было пролезть в журнал АН СССР? Да вы оптимист! Вы хоть гляньте, что это за фрик такой. ;)
Весьма показательно ваше выступление, вот это да.

СГС построена корректно, «LT система» — нет.


Правильно, Академия Наук СССР любила доклады о ерунде слушать. Потому Бартини там и представил свою систему — чтобы над ним посмеялись, да? Только все с ней согласились за десятилетия (а так несогласные, конечно, были), но akhalat упорно видит ошибку. Ну пусть дальше видит.
Ерунду вы написали, вот что.

Хороший аргумент, твердый.

Именно потому, что это разные процессы мы можем положить эти массы одинаковыми изначально.

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

Академия Наук СССР любила доклады о ерунде слушать.

Лысенко напомнить?
На вашу статью Бартини выше ответил, если интересно, почитайте как ее приняли.
Хороший аргумент, твердый.


Вы «Идиократию» не смотрели? Вот тут такая же история, как с поливом растений водой.

Процессы физически разные, но массы в них должны быть одинаковыми?


«Хороший аргумент, твердый». ;) «Этого не может быть, потому что не может быть никогда»?

Лысенко напомнить?


Ой, куда вас понесло. Ну тогда скажите на милость, вы в соотношение неопределённостей верите? Не обманывают ли вас? ;)

На вашу статью Бартини выше ответил, если интересно, почитайте как ее приняли.


То есть, вам всё-таки нужен авторитет? ;) А то ведь «Лысенко напомнить?» Посмотрите как принимали критиков Лысенко.
«Этого не может быть»

… потому что там банальная ошибка в формулах, автор не понимает как работать с размерностью и физическими константами, на что я вам указал.
… потому что там банальная ошибка в формулах


Да нет там никакой ошибки в формулах. Там есть положение равенства масс, ну так, если уж вам так интересно, в СИ они так же считаются равными (и это не забыли проверить!), не обращая внимания на то, что равенство задано константами.
Вы хоть читайте на что ссылки находите в спешной попытке гуглежа: «Принцип эквивалентности сил гравитации и инерции». Это принцип физики, а не СИ.
И говорит, что вы не сможете найти разницы в физических явлениях, происходящих в поле той силы или другой. Фундаментальный принцип, положенный Эйнтштейном в основу ОТО, как я уже писал выше.

не обращая внимания на то, что равенство задано константами.

Конечно, сущая мелочь, на которую можно «не обращать внимания»
Это принцип физики, а не СИ.


А вы не зацикливайтесь на этом. Мы говорим о системах единиц — вот потому и в СИ, а не в физике. В данный момент используя СИ обе массы считаются эквивалентными и прошли экспериментальную проверку равенства до какого-то знака. Это означает, что при построении новой системы единиц мы вполне можем принять их эквивалентными. Точка.

Конечно, сущая мелочь, на которую можно «не обращать внимания»


Вот только на это как раз внимание и не обращают. Потому и проводят эксперименты для подтверждения.
Это означает, что при построении новой системы единиц мы вполне можем принять их эквивалентными.

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


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

В физике всё делают аккуратно и осмысленно, от того и появляются коэффициенты, мешающие некоторым фрикам ;)

Найдите где-нибудь хоть малейшее указание, что причина в коэффициенте? Не найдёте.

Плохо гуглили, придётся давать ссылку за вас, хотя она и была всё время у вас под носом: ru.wikipedia.org/wiki/%D0%9C%D0%B0%D1%81%D1%81%D0%B0#%D0%93%D1%80%D0%B0%D0%B2%D0%B8%D1%82%D0%B0%D1%86%D0%B8%D0%BE%D0%BD%D0%BD%D0%B0%D1%8F_%D0%BC%D0%B0%D1%81%D1%81%D0%B0._%D0%9F%D1%80%D0%B8%D0%BD%D1%86%D0%B8%D0%BF_%D1%8D%D0%BA%D0%B2%D0%B8%D0%B2%D0%B0%D0%BB%D0%B5%D0%BD%D1%82%D0%BD%D0%BE%D1%81%D1%82%D0%B8
Плохо гуглили, придётся давать ссылку за вас, хотя она и была всё время у вас под носом:


Я не гуглил, я ориентировался на учебник по физике. Хорошо, значит они так скрыли проверку отношения, но по ссылке сказано «Данное обстоятельство является нетривиальным экспериментальным фактом. ». А раз так, то можно так поделить пропорцию, что обе массы станут равными и вот этой массой и заменить обе массы. И коэффициент не понадобится.
А раз так, то можно так поделить пропорцию, что обе массы станут равными и вот этой массой и заменить обе массы. И коэффициент не понадобится.

Это так не работает. Возьмите листок, если хотите, выпишите две формулы и убедитесь: убирая константу из одного закона, она автоматически перемещается во второй. И не забывайте, что по-умолчанию обе массы не равны, а всего лишь пропорциальны, при том коэффициент пропорциональности размерен.
Я не сомневаюсь, что у вас получится ввести новую «массу» и придать ей произвольную размерность. Только, по факту она будет некоторой математической комбинацией инерционной массы, гравитационной массы, и константы G — и только после разделения на исходные компоненты вернёт физический смысл.
В том-то и дело, что в выводе массы всё абсолютно корректно. Вот смотрите, что Максвелл писал в 1973.
Максвелл «Об электричестве и магнетизме».
Страница 31.


Если же, как в астрономической системе, единица массы выражена через силу её притяжения, то размерность [L3 T-2]


Достаточно вам будет Максвелла, чтобы вы поверили в корректность преобразований? Я несколько устал вести так долго подобные разговоры, очевидные мне, но неочевидные оппоненту.
Вот смотрите, что Максвелл писал в 1973.

Максвелл в 1973 очень давно умер.
Судя по таким пассажам, вы достаточно далеки от физики, если не имеете представлений о временных периодах ее открытий.

Достаточно вам будет Максвелла, чтобы вы поверили в корректность преобразований?

Нет, потому что преобразования некорректные, это показывается в две строчки.

очевидные мне, но неочевидные оппоненту.

Мне очевидно ваше крайне скудное владение матчастью, которое вы пытаетесь маскировать, дергая информацию оттуда-отсюда.

Максвелла

Громкое имя ещё ничего не значит. Даже величайшие из людей были в чём-то не правы. Лорд Кельвин утверждал, что машина тяжелее воздуха никогда не сможет летать, а Ландау говорил о невозможности графена. Максвелл писал это в 19 веке, когда принцип эквивалентности ещё не был сформулирован Эйнштейном.

Ещё раз: все попытки введения LT-системы основаны на идентификации инерционной и гравитационной масс. При этом их авторы забывают, что экспериментально, доказана только пропорциональность этих масс, которые в общем случае имеют разную размерность. Точное числовое и размерное равенство масс обеспечивается надлежащим подбором гравитационной постоянной G.
Самое забавное, что вы сами изначально так и говорили, вспомните ваш ранний комментарий «Их наблюдаемое совпадение — результат выбора системы единиц». Но когда я подтвердил, что этот факт хоронит LT-систему, вы сразу стали утверждать обратное.
Максвелл в 1973 очень давно умер.
Судя по таким пассажам, вы достаточно далеки от физики, если не имеете представлений о временных периодах ее открытий.


А не больно ли вы мелочны? ;) То есть, вам достаточно опечатки, чтобы подобные вердикты ставить?

Мне очевидно ваше крайне скудное владение матчастью, которое вы пытаетесь маскировать, дергая информацию оттуда-отсюда.


А, ну конечно. ;) Сдаётся мне, вы физикой никогда и не занимались. Я-то по образованию физик (квантовая электроника). Там знаете сколько в этой физике нюансов? Всех не упомнишь. А этой темой я интересовался 10 лет назад и, естественно далеко не всё помню.

Самое забавное, что вы сами изначально так и говорили, вспомните ваш ранний комментарий «Их наблюдаемое совпадение — результат выбора системы единиц».


Вот мы и ввели систему единиц, где они равны.

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


Боюсь, что только в вашем воображении (как со скоростью). ;)

Громкое имя ещё ничего не значит.


Громкие заявления akhalat тоже мало чего стоят. Максвелл и остальные хотя бы опубликовались. А akhalat просто зациклился «так нельзя!». Ну а в этом случае зачем тратить на него время и силы? Правильно, незачем. Тем более, что он въедливый и на этом строит далекоидущие выводы, но что критикует не понимает всё равно — это видно. Засим откланяюсь — мне бы не хотелось угробить ещё один вечер на беседу с вами. Dixi.
Я-то по образованию физик (квантовая электроника)

Ну значит, плохо учились, если не можете выписать две формулы и проверить их на противоречивость.

Вот мы и ввели систему единиц, где они равны.

Ага, СИ называется.

Там знаете сколько в этой физике нюансов? Всех не упомнишь

Ну вот вы сами и признались. Один из «ньюансов» есть всего лишь пропорциональность гравитационной и инерционной масс.

А вообще, печально, что даже профильные по образованию физики ведутся на откровенное фричество.
Во избежании дальнейшего распространения лже-науки:
Вот
И вот
Только вот там в той же Википедии приписано «Тем не менее, полноценная научная оценка статье пока не дана».
Так что никакой лженауки там нет. Там есть способ построения системы единиц и не более.
Какая «полноценная научная оценка»? Все посмеялись, покрутили пальцем у виска и забыли.
Уважающий себя журнал изъял бы подобное из печати. В те времена, по очевидным причинам так делать не стали. Сейчас «опровергать» это смысла нет, т.к. никому не надо

Там есть способ построения системы единиц и не более.

Вы сами то статью читали? Очевидно, нет.
Никакого «построения системы единиц» там нет и в помине. Автор претендует на построение математической (ага) модели мира. При том у него время оказывается трехмерным. Это уже всё, что можно сказать про отношение статьи к физической реальности.

С математической точки зрения там изложен чистый бред: просто научноподобный текст из случайной связанной комбинации терминов — в лучших традициях «корчевателя». Или, как сейчас модно было бы сказать: сгенерировано нейросетью.
Какая «полноценная научная оценка»? Все посмеялись, покрутили пальцем у виска и забыли.


А вот это сомнительно. В 1965 непременно бы поставили бы вопрос, почему журнал публикует не то, что должен. А это значит, что никто никаким глубоким анализом и не занимался.

Вы сами то статью читали? Очевидно, нет.


Читал, но с топологией я не знаком. Потому оценить не могу.

Никакого «построения системы единиц» там нет и в помине.


Там конечный результат.

С математической точки зрения там изложен чистый бред


А вот это вряд ли. Даже чтобы просто проверить выкладки, нужно очень неплохо владеть материалом статьи. Вы им владеете? Что такое теорема Стилова знаете?
А вот это сомнительно. В 1965 непременно бы поставили бы вопрос, почему журнал публикует не то, что должен.

Статья была пропихнута в журнал академиком, в таком случае она публикуется без рецензии. Так и было сделано. Раздувать из этого скандал не стали, проще всего было «забыть» о статье.

Даже чтобы просто проверить выкладки

Там нет никаких «выкладок», это набор слов без смысла.
Там нет никаких «выкладок», это набор слов без смысла.


Так я про любую статью, которая мне непонятна, могу сказать.

Так и было сделано. Раздувать из этого скандал не стали, проще всего было «забыть» о статье.


Ага. И в сборнике «Проблемы теории гравитации и элементарных частиц», 1966 г. она тоже оказалась просто так? Ну надо же, куда только не пролез по блату.

Да, кстати, до Бартини такую таблицу уже строили.

Содержание основных результатов о геометрическом, пространственно-временном выражении единиц физически измеримых величин и аналитические формулы для них датированы ученым ноябрем 1940 года. В работе английского исследователя Дж. Бурнистона Брауна фактически так же была введена аналогичная таблица (май 1940) [13]. Ввиду независимости исследований Брауна от работ Ди Бартини и их практической одновременности ее следовало бы назвать таблицей Бартини-Брауна.
(стр.200).

Кстати, вспомнил, не у Фарадея, у Максвелла было про это же.
Вторая статья буквально противоречит первой. Авторы открыто пишут об этом в аннотации. Насколько я знаю, the Annals of Mathematics никогда не публиковала опровержений ни одной из этих работ. Какую из работ считают правильной опытные математики?

Если ни у того, ни у другого утверждения нет практического применения, тогда какая разница, которое из них верно?

Корень из двух — это иррациональное число. У этого факта тоже нет применения, потому что в практических применениях все считают до какого-нибудь знака после запятой.


Тем не менее, я считаю этот факт важным, и более того — прекрасным.

Как же это нет применения? Если бы корень из двух был рациональным числом, то его пытались бы вычислить точно и затем использовать это точное значение в вычислениях. А так как доказано, что его невозможно представить точно в виде дроби, то его никто и не вычисляет точно.

Если бы корень из двух был рациональным числом с тысячей знаков после запятой, люди бы всё равно не использовали все эти знаки.

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


А если вместо «корня из двух» взять «корень из π», то задача о квадратуре круге была бы в учебнике пятого класса по арифметике.

Так эти расчёты будут проводить с символом √2, и сократится он с таким же символом. Вопрос рациональности здесь не нужен?

сократится он с таким же символом

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


Вот смотрите, есть у вас разложение по бесселям каким-нибудь. Тут √2, там √5. Тащим за собой все как рациональные дроби, а потом упрощаем без потери точности. С иррациональными числами так не выйдет.

пользовали, если бы был нужен ТОЧНЫЙ результат. А сейчас мы знаем что это не возможно и приходиться либо округлять либо искать обходные пути

В этом как раз суть математики: она прекрасно может жить без практических применений (я сказал математика, а не математики), но теряет смысл без формальной истинности.
А что с признанием работ японского математика Мотидзуки?
На Хабре ранее было несколько статей, где писали что его работы вроде совершили переворот, но их пока не могут понять и проверить, потому как там сотни страниц совершенно нового математического аппарата.
Все еще его работы не были признаны сообществом проверенными, но он скоро опубликует их в журнале своего университета.
НЛО прилетело и опубликовало эту надпись здесь
Проблема в том, что у людей нет столько времени. Тут точно так же, как с доказательным программированием. Была австралийская фирма NICTA (полугосударственная), они писали маленькую безотказную операционку для медицинской техники. Писали на C, вставляли в программу условия, которые должны быть выполнены в момент, когда до них дойдёт дело (логика Хоара). Например, (x>0) x=x+1; (x>1) Если перед выполнением присваивания x=x+1 было верно предусловие (x>0), то после будет верно (x>1). Затем писали доказательство, что условия действительно выполнены и проверяли его пруфчекером Isabelle. На 7500 строк кода пришлось выписать примерно 200 тысяч строк доказательств, это заняло 11 человеко-лет работы. Пруфчекер нашёл 144 ошибки. Дело хорошее, но ясно, что так мы много не напрограммируем. В математике сейчас доказательства настолько сложные (всё простое давно доказано), что проверять их нет желающих, авторитетам верят на слово. Тот же Воеводский в своей статье нашёл ошибку через 20 лет.

Интересно было бы почитать подробнее об этом и других подобных фактах.

Надо гуглить. Ну, вот непонятный текст из вики-статьи про Воеводского
«В работах 1989—1990 годов по высшим группоидам, написанных в соавторстве с Капрановым, развил идею Гротендика о возможности описания CW-комплексов с гомотопической точки зрения как группоидов. В 1998 году Карлосом Симпсоном построен контрпример к одной из основных конструкций этих работ, который Воеводский с Капрановым изначально не признали, и статья Симпсона не была принята в журналы; лишь в 2013 году Воеводский подтвердил доводы Симпсона.»

Расшифровываю: в 90-м году Воеводский и Капранов «доказали» некую хорошую теорему. В 98-м Симпсон нашёл пример, вроде бы опровергающий эту теорему. Воеводский считал, что Симпсон ошибся и приводил какие-то доводы. И доказательство, и пример Симпсона настолько сложны, что никто не мог проверить до 2013-го года, когда Воеводский сам нашёл ошибку в своей статье (через 23 года). После этого он все свои доказательства проверял пруфчекером.
НЛО прилетело и опубликовало эту надпись здесь

Кажется, что они зря си для этого дела взяли.

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

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

Перед тем, как что-то формализовать вам нужно избавиться от тривиального противоречия (иначе любая тривиальная система проверки именно на него и будет указывать) — а это бывает сделать не так-то просто…

Такие системы уже есть, и не одна.

Математики часто не любят доказывать тривиальные вещи. Например, работая с Coq или Idris многие жалуются, что компьютер слишком придирчив (например, он не пропустит равенство x = y + 1 если требовалось доказать x = 1 + y). А запись в формальном виде это по сути и есть доказательство и программирование.

в современной математике мнение по поводу того, является ли что-то доказательством, меняется с течением времени (например, может пройти путь от “является” до “не является”).

Ещё Томас Кун писал о смене научных парадигм. Думаю, эта изменчивость касается не только современной математики. Да и не только математики.

Как раз у «не только математики» есть вполне себе повод меняться. Наука: это объяснение совокупности экспериментов, грубо говоря.

Получили новые результаты, объяснили их — имеем новую науку.

А математика, вроде как, оперирует с логическими построениями, основы логики не экспериментальны, но аксиоматичны… откуда тут «смена научных парадигм»?

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


В плоскости через точку, не лежащую на данной прямой, можно провести одну и только одну прямую, параллельную данной.

Там же я краем уха что-то слышал про геометрию Лобачевского, где есть другая аксиома:


Через точку, не лежащую на данной прямой, проходят по крайней мере две прямые, лежащие с данной прямой в одной плоскости и не пересекающие её.

В википедии я читаю следующее:


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

То есть, до Н.И. Лобачевского математическое (и не только) сообщество считало, что можно провести только одну прямую, параллельную данной и исходя из этого строило свои доказательства. После специалистам стало ясно, что в принципе таких параллельных прямых можно провести несколько. В связи с этим у меня, как у неспециалиста, возник вопрос: можно ли считать появление неевклидовой геометрии научной революцией и, соответственно, сменой научных парадигм?

Извините, решил написать реплику, поскольку ваш оппонент не ответил. В студенческие годы я интересовался темой альтернативных аксиоматик, например, есть разделы математики, изучающие последствия удаления или замены некоторых «стандартных» аксиом, например, аксиомы выбора в аксиоматике теории множеств, или логического закона исключения третьего. Так вот, в моём понимании собственно изобретение неевклидовых геометрий в XIX веке было существенным, но только фрагментом «смены парадигм» в математике, растянувшейся на многие десятилетия; о «революции» можно наверно говорить только в применении к конкретному разделу математики, геометрии. Лобачевский и другие авторы неевклидовых геометрий дали неожиданные ответ на трудный вопрос в геометрии: действительно ли постулат о единственности линии, параллельной данной и проходящей через данную точку, является аксиомой? Геометры прошлого строили доказательство этого постулата (пятого постулата «Начал» Евклида), базирующееся на остальных аксиомах геометрии (таким образом низводя его статус от аксиомы к теореме), но позднее в этих доказательствах обнаруживали ошибки. Работы Лобачевского (и других авторов) продемонстрировали независимость пятого постулата от других аксиом — посредством построения моделей альтернативных аксиоматик, в которых пятый постулат заменен одним или другим противоречащим ему утверждением (или «несколько», как написано у вас — гиперболические геометрии — или «ни одной» — эллиптические геометрии).

Эта частная геометрическая история (заметьте, ваша фраза «в принципе таких параллельных прямых можно провести несколько» относится не к евклидовой геометрии, её никто не опровергал — она относится к альтернативным аксиоматикам, описывающим не евклидову плоскость / пространство, а другой математический объект, в котором определённое подмножество фактов евклидовой геометрии сохранено, но другое — заменено или удалено) подтолкнула интерес к построению и изучению формальных аксиоматических систем в других областях математики.

Кстати, вспомнил переводную книгу, изданную в СССР где-то в середине 80-х, «Математика: утрата определённости» Мориса Клайна, сейчас поищу — о, про неё даже заметка в Википедии: ru.wikipedia.org/wiki/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D0%BA%D0%B0._%D0%A3%D1%82%D1%80%D0%B0%D1%82%D0%B0_%D0%BE%D0%BF%D1%80%D0%B5%D0%B4%D0%B5%D0%BB%D1%91%D0%BD%D0%BD%D0%BE%D1%81%D1%82%D0%B8 (интересная книга, насколько я помню).

Дискуссия идет не за геометрию, а за философию науки. Я просто привел пример, который лежит на поверхности и может проиллюстрировать эту самую смену научных парадигм. Судя по всему, аргумент в моем изложении неправильно понимают, поэтому я хотел бы прояснить идею.


Я и не говорю, что евклидову геометрию кто-то опроверг. Я хочу сказать, что с появлением неевклидовой геометрии сильно изменилось пространство маневра для доказательств. Покажу на примере. До появления неевклидовых геометрий сумма углов треугольника была строго равна 180 градусов. Этому есть доказательство, основанное на свойствах параллельных прямых. С появлением геометрии Лобачевского ситуация в математике изменилась. Мы уже имеем два частных случая, которые являются верными и научно обоснованными при условии соблюдения четко определенных условий:


  1. Для эвклидовой геометрии, где сумма углов все еще равна 180 гр.
  2. Для геометрии Лобачевского, где сумма углов треугольника меньше 180 гр.

Именно в таком изменении интеллектуального пространства для доказательства (а так же прогноза или объяснения) и заключается смена научных парадигм. Здесь как в физике. Несмотря на появление теории относительности, классическая механика тоже не перестает работать в тех условиях, в которых она когда-то создавалась. Релятивистская механика расширила объясняющие, прогностические и доказательные возможности науки физики, как неевклидова геометрия расширила возможности математики.


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

Здесь как в физике.
Нет. Ровно наоборот, по отношению к физике. Вы же сами пишите:
Я и не говорю, что евклидову геометрию кто-то опроверг.
А потом:
Релятивистская механика расширила объясняющие, прогностические и доказательные возможности науки физики, как неевклидова геометрия расширила возможности математики.
Но ведь релятивистская механика не просто что-то там «расширила». Она сделала предшествовавшую теорию неверной. Вот просто неверной — и всё.

Да, в математике могут (и регулярно появляются) новые конструкции. Однако момента, потобному «закрытию» теплорода — нет и быть не может.

Эксперименты на БАК позволили выбрать одну из теорий (а десятки, если не сотни, других «остались не у дел») — но сферическая геометрия не отменила Евклидову! Более того — геометрия Лобачевского легко «вкладывается» в Евклидову… в математике — но в физике а выбор между тремя возможностями вполне детерминирован.

Но это в физике… в математике евклидова геометрия, по прежнему, рассматривается не как «приближение для малых размеров и скоростей» (таков сейчас статус у Ньютоновой механики), а как вполне самостоятельная сущность.

В физике были закрыты десятки, сотни, тысячи теорий — просто потому, что они не согласовывались с опытом. А не потому что они были внутренне противоречивыми.

Мы уже имеем два частных случая, которые являются верными и научно обоснованными при условии соблюдения четко определенных условий:
И вот ровно это и невозможно в физике. Там не бывает двух разных «одинаково верных» физик. Физический закон либо верен, либо неверен… и всё.

Нет никаких «альтернативных физик» (вне рамок фантастических романов, по крайней мере). В тех случаях, когда у нас есть две несовместымых теории (квантовая механика и теория относительности, да) — это просто обозначает, что мы провели недостаточно опытов, чтобы построить одну теорию, их объединяющюю.

Словом, утверждение о том, что в математике есть только одна, неизменная со времен царя Гороха, научная парадигма неверно.
Конечно неверно — где я вообще такое писал? Там существует ноль научных парадигм!

Потому что математика — это не наука! Это — инструмент, применяемый наукой. Также, как русский или английский языки не содержат в себе никаких «парадигм» — точно так же и математика их не содержит.

А вот уже книги, написанные на русском языки или химические теории, описанные на математическом — они могут содержать «парадигмы»…
==Но ведь релятивистская механика не просто что-то там «расширила». Она сделала предшествовавшую теорию неверной.==

Нет, не сделала. Думать, будто открытия ХХ века ниспровергают предшествующую физику — грубейшая ошибка. Неверной оказалась теория флогистона. Статус механики Ньютона гораздо выше.

Во-первых, второй закон Ньютона, изложенный самим Ньютоном в «Началах» в форме dp/dt=F=-dU/dx есть сразу одно из уравнений Гамильтона и формально верно и во всей современной физике.

В-вторых, механика Ньютона — это формально-операционный базис всей современной физики: понятия гамильтониана, лагранжиана, состояния, потенциала, поля, введённого самим Ньютоном в своих «Началах», невозможно последовательно ввести без механики Ньютона.

В-третьих, и в главных. Механика Ньютона — это пока единственное связующее звено между квантовой механикой и теорией относительности. Это её центральное положение ставит пока механику Ньютона в совершенно исключительное положение. Все основные понятия, введённые Ньютоном, претерпев в каждой из физик свои интерпретации, по-прежнему являются ключевыми: масса, пространство, время, материя, вакуум.

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

В-пятых, без механики Ньютона не только формально, но и физически становится неясным, во всяком случае, для людей, содержание и вывод теоремы Нётер, лежащей в основе, в т.ч., КЭД.

В-шестых, сам по себе факт того, что механика Ньютона — предельная физическая теория по отношению к КМ и ТО, никак не влечёт вывод, что она неверна (скорее наоборот). Утверждать обратное, всё равно что из временной обратимости элементарных уравнений физики, делать вывод, что 2-й закон термодинамики неверен: последний с позиций статистической физики тоже является пределом. Тем не менее, верно и то, и то. Из того, что механика Ньютона — это предел (причём квадратичный по v/c и h/S) каких-то других теорий, само по себе не может следовать ничего критического по отношению к МН.

В отличие, однако, от последнего примера, аппарат и понятия механики Ньютона существенным образом используются и КМ, и ТО.

И, наконец, геометрию Евклида ничто не препятствует рассматривать именно как предел других геометрий, особенно если, следуя Эйнштейну, смотреть на ЕГ как на «первую физическую теорию». То, что математики это делают редко, — это проблема этих математиков; как говорил великий Арнольд «математика — часть физики».
"В плоскости через точку, не лежащую на данной прямой, можно провести одну и только одну прямую, параллельную данной." [...] краем уха что-то слышал про геометрию Лобачевского, где есть другая аксиома: "Через точку, не лежащую на данной прямой, проходят по крайней мере две прямые, лежащие с данной прямой в одной плоскости и не пересекающие её." [...] То есть, до Н.И. Лобачевского математическое (и не только) сообщество считало, что можно провести только одну прямую, параллельную данной

Всё Вы перепутали. Лобачевский ничего не опровергал — он просто задумался: "ну, интуитивно понятно, что в плоскости так оно и есть — а придумаю-ка я каку-нибудь другую конфигурацию, в которой это будет не так!". И придумал. И тем самым вписал своё имя в историю.

К примеру, как раз взгляд на математику как на дисциплину, оперирующую логическими построениями, сформировался в относительно недавнее историческое время (меньше двух веков) в результате… «смены научных парадигм»? Вы можете спорить, что это не было «сменой научных парадигм», предлагать другой термин — тем не менее, процессы, похожие на смены научных парадигм (лучше всего иллюстрируемые примерами из других наук) происходили и происходят и в математике тоже. Приведу небольшой частный пример несостоявшейся смены научных парадигм в математическом анализе (ну или по крайней мере в преподавании математического анализа) — так называемый «нестандартный анализ». Он предлагает использование расширенной числовой прямой, в которой бесконечно малые величины — реальны (а не являются языковой конструкцией, скрывающей довольно громоздкий дельта / эпсилон аппарат «стандартного» анализа). Набор доказываемых фактов такая смена аксиоматики не меняет, но доказательства и преобразования становятся значительно легче и понятнее. Не прижился (критики внедрения этого подхода в преподавании взяли верх, насколько я понял), но влияние оказал (в частности, прояснил вопрос, как математикам прошлых веков — до появления строгого логического базиса стандартного анализа — могли добиваться верных результатов, оперируя мутными понятиями вроде «бесконечно малые величины», и не надоказывать ложных теорем).
НЛО прилетело и опубликовало эту надпись здесь
Строго говоря, в техническом вузе не обязательно понимать, почему нестандартный анализ эквивалентен стандартному (именно для этого нужны всякие аксиомы Лося и прочий хардкор). В практических целях достаточно знать аксиоматику нестандартного анализа и принять на веру, что он эквивалентен стандартному.
Строго говоря, в техническом вузе не обязательно понимать, почему нестандартный анализ эквивалентен стандартному (именно для этого нужны всякие аксиомы Лося и прочий хардкор).

Нестандартный анализ без матлога — это просто анализ Лейбница (собственно, Робинсон просто нашел подходящую формализацию для этого подхода). А вести в 21 веке изложение в рамках языка 17 века с соответствующим уровнем строгости — такая себе идея.


В практических целях достаточно знать аксиоматику нестандартного анализа и принять на веру, что он эквивалентен стандартному.

Совсем недостаточно. Вы внутри нестандартной модели не можете рассуждать о бесконечно малых величинах, они там не существуют. Любой нетривиальный результат нестандартного анализа — это метатеоретическое рассуждение, когда вы на нестандартную модель смотрите из какой-то метатеории.

Слушайте, я нестандартным анализом интересовался постольку-поскольку, так что могу ошибаться. Но сходу не пойму, где именно. Вроде у нас есть ZFC, мы её надстраиваем аксиоматикой нестандартных элементов, и дальше оттуда всё выводим. Разве для этого требуется знание матлога большее, чем уметь пользоваться модус поненс?

Можно конкретный пример, когда у нас есть нестандартный анализ, есть здравый смысл, нет знания матлога, и на выходе получается чепуха?
Вроде у нас есть ZFC, мы её надстраиваем аксиоматикой нестандартных элементов, и дальше оттуда всё выводим.

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


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

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

У меня такое чувство, что мы про какие-то разные вещи говорил. Тот нестандартный анализ, которым интересовался я, был основан на расширенной аксиоматике Цермело-Френкеля. Ну да, мы строим особую модель с нестандартными элементами. Мы делаем некие утверждения относительно нестандартных элементов (что я подразумевал под расширением аксиоматики). Потом хоба — и говорим, что всё, что мы доказали там, будет работать и здесь. Там какая-то магия математической логики, которую я понимал когда-то, но забыл.

И вроде там можно было вполне спокойно доказывать теоремы из матана на птичьем языке, и переключаться между птичьим и человечьим, чтобы понять, что именно мы содержательно доказали. И это можно было делать вполне строго, даже не понимая механизм связи между двумя моделями. Или я путаю?
У меня такое чувство, что мы про какие-то разные вещи говорил. Тот нестандартный анализ, которым интересовался я, был основан на расширенной аксиоматике Цермело-Френкеля.
Мы делаем некие утверждения относительно нестандартных элементов (что я подразумевал под расширением аксиоматики). Потом хоба — и говорим, что всё, что мы доказали там, будет работать и здесь.

Это работает следующим образом. У вас есть некоторая теория Т — это одна теория. Вы можете построить две модели для этой теории — стандартную и нестандартную (для любой модели можно построить ее нестандартный вариант при помощи операции ультрастепени) и эти модели будут элементарно эквивалентными (утверждение истинное на одной модели истинно и на другой, например, континуум-гипотеза либо верна либо неверна одновременно на обеих. элементарная эквивалентность модели и ее ультрастепени — прямое следствие теоремы Лося). В первой модели у вас обозначающие множества символы из теории Т ставятся в соответствие "обычным" множествам (простому множество натуральных, например), во втором случае — собственно, нестандартным (множество гипернатуральных, например). При этом сами формулы и теоремы теории Т остаются теми же самыми — вы меняете просто смысл используемых там символов. По-этому, находясь "внутри" теории Т вы нетривиальную структуру нестандартного анализа не видите, на самом деле вы даже не можете сформулировать какое-то содержательное утверждение о нестандартных элементах или сформировать какое-то множество которое эти элементы содержит нетривиальным образом.


Дальше, однако, вы можете взять метатеорию метаТ (в рамках которой описывалась Т и ее модели, эта теория может даже совпадать с Т) и увидеть, что структура нестандартной модели богаче — т.е. о множествах нестандартной модели вы можете делать утверждение не только те, которые у вас есть в Т, но еще и другие. В итоге, используя эти утверждения вы можете доказать некоторое утверждение о нестандартной модели — и вот далее, если это утверждение о модели будет соответствовать интерпретации некоторой формулы из Т, то, раз эта формула истинна в нестандартной модели, то она автоматически истинна и в стандартной (примерно как — получили в середине выкладок корень из -1, но потом его сократили). Ключевой момент здесь — это, конечно, убедиться в том, что ваше итоговое утверждение действительно является какой-то нестандартной интерпретаций утверждения из Т (т.е. не содержит sqrt(-1), например, утвержедниео существовании в множестве гипернатуральных бесконечно больших чисел — это утверждение в метаТ о нестандартной модели, формулой в Т оно не является). Аксиоматика о которой вы говорите просто описывает некоторые правила работы с утверждениями такие, чтобы полученные утверждения как раз и соответствовали этому требованию.


Проблема в том, что вся содержательная часть формализация остается за бортом, а сама аксиоматизация весьма искусственна. С тем же успехом можно было бы вместо е-д формализма давать в качестве аксиома десяток базовых теорем классического анализа и из них все выводить.
Но цель курса-то как раз в том чтобы объяснить все начиная с самых низкоуровневых аспектов. Дать жэе нестандартный анализ с аксиоматики — это то же самое, что начать с середины, т.к. откуда возникнет у студента понимание, почему это вообще работает? Откуда взялись эти правила работы с утверждениями? Почему они именно такие? Это все останется где-то там, далеко.

Да, похоже, теперь мы говорим об одном и том же. Тогда мой тезис в следующем: бывают люди, которым матан пригодится, а лезть в основания математики не пригодится. Физики там всякие. И для них может быть полезен формализм нестандартного анализа даже без его строгого обоснования. Это лучше, чем эпсилон-дельта, в плане перевариваемости, и лучше, чем наивный матан а ля 18 век, в плане строгости.

Это лучше, чем эпсилон-дельта, в плане перевариваемости

Так вы можете давать классический анализ без е-д формализма тогда, просто зафиксировав базовые теоремы в качестве аксиом. Это будет равносильно даже в плане подачи. Аналог е-д формализма в нестандартном анализе — это и есть соответствующий матлог.


Тет же проблема еще в том что сам по себе нестандартный анализ не особо осмысленно работает, пока вы не показываете эквивалентность классическому. Т.е. — допустим, вы дали нестандартное определение предела. Но как теперь прокинуть мост к классическим пределам, если классического определения предела студент не знает?

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

При этом подразумевают в разговоре как раз е-д рассуждения :)


И нестандартное определение предела, в общем-то, проще стандартного, если мне не изменяет память.

Так а что дальше-то делать с этим определением? 99% литературы используют классический анализ в R. Допустим, вы доказали какой-то факт о непрерывной ф-и hyperR -> hyperR, каким образом теперь перенести это на факт о непрерывной ф-и R -> R если вы не знаете, что такое непрерывная ф-я R -> R? :)

При этом подразумевают в разговоре как раз е-д рассуждения :)
А вот неочевидно. Возможно, е-д рассуждения — это такая постылая необходимость. Типа, «ну тут всё и так понятно, но чтобы не докопались, давайте проговорим на языке эпсилон-дельта».

99% литературы используют классический анализ в R
Это поправимо)
А вот неочевидно.

Очевидно, ведь речь идет про R :)


Это поправимо)

Как? Все сжечь? :)
Опять же это сразу в школах надо с нестандартного анализа начинать, вместо обычных чисел.

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

Ну так я и говорю — можно без нестандартного анализа давать все то же самое, но на R, а не на hyperR. Результат один, но проблем — меньше.

Рассказывать про всякие монады нуля детишкам, которым школьная математика и так избыточна? Хитрый план. А продвинутым школьникам почему бы и нет, в принципе.
Рассказывать про всякие монады нуля детишкам

Зачем? Рассказывать ровно то, что рассказывается сейчас.

Тогда что вообще изменится?

А почему что-то должно измениться?

По идее не важно чему он там эквивалентен. Важно позволяет ли он моделировать всякие траектории, токи, энергии и прочее. Что вполне можно продемонстрировать на лабах. Не?
Набор доказываемых фактов такая смена аксиоматики не меняет
… собственно и всё. Это то, что отличает «смену парадигмы» в науке от «отсутствия смены парадигмы» в математике.

Понимаете — в науке парадигма — это некий «набор правил», которые мы считаем применимыми к окружающему миру. Меняется наша информация о том, как устроен мир — меняется и парадигма.

Вот вот вот:
Не прижился (критики внедрения этого подхода в преподавании взяли верх, насколько я понял), но влияние оказал
в науке невозможно. Никакие «критики внедрения этого подхода» не могут затормозить изменение парадигмы в физике если старая парадигма не согласуется, более, с опытами — а новая согласуется.

Эфир был изгнан из физики не потому, что он оказался «недостаточно изящным», а потому что соотвествующие опыты показали его отсутствие. А если новые опыты покажут его наличие — он вернётся. Опять-таки независимо от «критиков внедрения этого подхода».

в частности, прояснил вопрос, как математикам прошлых веков — до появления строгого логического базиса стандартного анализа — могли добиваться верных результатов, оперируя мутными понятиями вроде «бесконечно малые величины», и не надоказывать ложных теорем
А вот это уже — не математика, а психология. Тут мы исследуем не вопрос «как из этих аксиом что-то вывести», а совсем другой, психологический феномен «как, имея базис в виде противоречивых аксиом, которые позволяют понадоказывать много разной чуши, математики прошлого, тем не менее, получали полезные и правильные математические результаты». Психология — плюс-минус наука (с воспроизводимостью результатов не слишком хорошо, потому не вполне точная), так что тут «смена парадигмы» возможна… правда к «математикам прошлых веков» она имеет косвенное отношение: о том, как они, на самом деле, думали — мы можем только догадываться.

А это вообще возможно, описать все возможные логические переходы? Помню в бытность студентом приходил в восхищение от того, какой интересный логический прием был в каком-то доказательстве.


Или язык будет применим для "стандартных" переходов, а для новых идейных конструкций придется дорабатывать сам язык? Тот же Мотидзуки — взял и изобрел свой мат. аппарат. Все ли способы доказательств уже хотя бы раз были использованы кем-то еще?

Вот да, математика не сухая наука, в ней есть простор для творчества. Как например машина сможет придумать принцип двух милиционеров или изобрести интегральное исчисление, для этого нужен куда более обширный опыт человека.
> А это вообще возможно, описать все возможные логические переходы?

Если цель — заставить машину найти логический переход для доказательства — то ещё долго до этого (хотя простейшие случаи отработаны были очень давно — например, доказательство равенства углов равнобедренного треугольника по трём сторонам было открыто компьютером в 1968, и после этого попало в учебник Погорелова).
Если же просто проверить доказательство, которое уже написано человеком, тут, грубо говоря, достаточно modus ponens + modus tollens + силлогизм + сверка областей допустимости каждой посылки (которая тут будет, вероятно, самым неавтоматизируемым местом).
Разработаны языки, позволяющие строго записывать математические доказательства (с той же строгостью, с какой мы записываем алгоритмы в языках программирования). Длина такого доказательства обычно раз в двадцать больше длины обычного (какое мы излагаем в статье). Зато правильность его легко проверить автоматически (проверяет простая программка «пруфчекер»). Дело в том, что ни у кого нет времени и желания формализовать доказательство Мотидзуки.
Строго говоря, нет большой проблемы в том, что статья ссылается на недоказанные/сомнительные результаты. Такую статью можно легко исправить, добавив требуемое (сомнительное) условие в заголовок/аннотацию: «Если теорема Римана верна, то…» или даже «Если Луна сделана из сыра, то…». Разумеется, потенциальная полезность такого результата будет ниже, чем результата, не опирающегося на гипотезы, но зато утверждение становится формально корректным.

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


Конечно, в статье могут быть полезные методы и так далее.

Полезность не нулевая, если в будущем докажут справедливость недоказанных на данный момент посылок. В целом такие работы могут «набивать цену» посылкам, объясняя какая практическая польза будет от доказательства.

Есть и более конкретные примеры
В теории алгоритмов существует много теорем вида «наличие полиномиального алгоритма для задачи распознавания влечёт наличие полиномиального алгоритма для оптимизационной задачи». Как правило, такие теоремы имеют конструктивные доказательства, которые полезны и без полиномиальных алгоритмов для задач распознавания.
На мой взгляд, хорошая математика — это поиск метода доказательства, который сложно найти, но относительно легко проверить, когда он найден.
Эта идея перекликается с теорией сложности, определением NP и всем таким.

Обычно после доказательства новых результатов математики переписывают определения, чтобы результаты были тривиальными :)

12 томов доказательства… это как писать операционку на динамически типизированном языке ни разу не запуская и не допустив ни единого бага.

Судя потому, что там в названии работы «классификация», то 12 томов это не доказательство, а перечисление возможных вариантов с их свойствами. Типа как в биологии есть огромные книги с классификацией живых организмов.

Ок, разверну мысль: в математике много доказательств на сотни и тысячи листов. А люди порой и однострочную функцию написать без багов не могут. Математики, конечно, более прокачаны в плане ментального статического анализа, но они тоже люди.

НЛО прилетело и опубликовало эту надпись здесь
Мне кажется автор путает. У математики нет этих проблем. Проблема в том что математики ленятся и филонят, используют непроверенные результаты других, верят кому-то на слово. Их можно понять — кому хочется всю жизнь проверять одну теорему от и до.
Но тем не менее.

У математики нет проблем. Но у математиков есть. Чем дальше мы идём, тем больше результатов надо проверять.


Поэтому автор и предлагает перенести часть нагрузки на формальные верификаторы.


Я не согласен, что это лень. В физике мы тоже не можем повторить все эксперименты прошлого. Это просто новые реалии, и научное сообщество пытается найти решение новых проблем.

Люди разные. Одни любят факты, другие любят принципы, которым следуют факты, третьи любят доказательства принципов, которым следуют факты, а четвёртые так вообще выделяют для себя то, что может произвести доказательство. А есть и такие что просто любят спрашивать.

отдельное спасибо за то, что совершенно нечитаемую презентацию перевели в хорошо структурированную статью, сделали преамбулу про xkcd, да и сам перевод по языку очень хорош

заумно по-моему… а тема занятная

Приятно видеть, что разработку моего универа Isabelle используют. Профф от этого департамента мега круто чувак. Его лекции по Изабель скорей для нердов или математиков(как я), но ведёт и организует он их бомбезно

Эх, ладно там математика. Вот бы дожить до возможность формально верифицировать законы и подзаконные акты на непротиворечивость друг другу и вышестоящим документам. Захотели депутаты протолкнуть ограничение свобод — а нифига, законопроект просто в базу не кладётся, отбивка по ошибке «не соответствие конституции». Захотел чиновник лямчик вывести на знакомую фирму без тендера — а фиг там, платёжка в бухгалтерии не создаётся, «не соответствует закону такому-то». Вот куда ИИ копать надо. А математики пока и сами неплохо справляются.
Вот бы дожить до возможность формально верифицировать законы и подзаконные акты на непротиворечивость друг другу и вышестоящим документам.
Эк вы размахнулись. Для того, чтобы это стало возможным нужно, как минимум, иметь полную и законченную физическую теорию вообще всего мироздания.

Захотели депутаты протолкнуть ограничение свобод — а нифига, законопроект просто в базу не кладётся, отбивка по ошибке «не соответствие конституции».
Законы физики, как несложно догадаться, имеют приоритет над конституцией, потому пока у нас нет полного свода всех законов физики, химии, биологии и так далее — это утопия. А хочу ли я, в принципе, дожить до момента, когда всё-всё-всё в этом мире будет открыто и изучать больше нечего… даже если это и возможно в принципе — не факт, что это будет хорошее время.

Вовсе не факт, что в этом раскладе вообще сохранится конституция и какие-либо подзаконные акты… не факт, что и свобода воли в этом «дивном новом мире» будет существовать…

Вот куда ИИ копать надо.
Вы уверены?

Захотел чиновник лямчик вывести на знакомую фирму без тендера — а фиг там, платёжка в бухгалтерии не создаётся, «не соответствует закону такому-то».
Стоп. Вы, надеюсь, понимаете, что достижение указанной вами «нирванны» невозможно, в принципе невозможно, пока существуют такие понятия как «чиновник», «ламчик», «фирма», «тендер», «платёжка», «бухгалтерия»… вот это вот всё — существует только ввиду неполноценности нашего знания о мире!

Не факт, что и люди, как независимые субъекты сохранятся вообще.

P.S. И да: бойтесь ваших желаний — они имеют свойство сбываться. Если мы и доживём до чего-либо подобного (а шансы, на самом деле, есть) — то вам меньше всего будет хотеться, чобы какой-то там «чиновник» не вывел какой-то там «лямчик»… очень может быть, что вы ещё будете вспоминать о временах, когда это вас волновало с ностальгией…
Для того, чтобы это стало возможным нужно, как минимум, иметь полную и законченную физическую теорию вообще всего мироздания.
Зачем?
Какая связь между законами мироздания и человеческими законами сформулированными для регулирования общественных отношений?

Возможно, комментатор имел в виду, что для применения формальной верификации, необходимо сначала формально описать деяние, которое требуется формально верифицировать на законность. И если проверить финансовые операции или непротиворечивость одних актов другим, быть может, возможно (не берусь утверждать), то для большинства дел это… затруднительно. Например, человек случайно убил нападавшего. Было ли это превышением допустимой самообороны? Требуется рассмотреть большое количество фактов, и далеко не факт, что удастся формализовать. Так же как и сейчас, спорные дела могут зависеть от того или иного решения в рамках трактовки фактов и закона. Таким образом есть предположение, что формальная верификация рассыплется на самом ненадежном звене — вводе исходных данных. Мусор на входе — мусор на выходе.

Возможно, комментатор имел в виду
Я там описал что я имел в виду. Буквально в следующем абзаце.

Например, человек случайно убил нападавшего.
Рассмотрите более простой вопрос: фура на автостраде сбила человека? Кто виноват? Водитель или тот, кого сбили?

А всё зависит от того, мог ли водитель, в принципе, избежать этого. Законы физики, в некотором смысле, «выше» любого закона и, в том числе, «выше» конституции.

Они — фундамент всей нашей деятельности… и соблюдение и несоблюдение законов — зависит тоже он них, родимых.

Потому никакая формально верифицируемая система никогда и не сможет ничего сказать на тему законности или незаконности в 100% случаев.

Таким образом есть предположение, что формальная верификация рассыплется на самом ненадежном звене — вводе исходных данных.
Не предположение — уверенность. Законы просто насквозь пропитаны фразами типа «возможные меры» или «опасность для движения, которую водитель в состоянии обнаружить».

Какие-то простые случаи — да, компьютер в состонии «разрулить». Но чуть шаг в сторону, ситуация слегка нестандартна — и всё, рассыпалась ваша «строго верифицируемая система».

Уж до уровня запрета депутатам что-то там принимать — она точно без полной структуры мира не доберётся.

Можно забить аксиомой что виноват всегда водитель и всё.


Для того чтобы написать верифицированную систему законов доказывать все законы физики не нужно.




Другой вопрос, что существует известное изречение: Социальная проблема не может быть решена инженерным способом.

Социальная проблема не может быть решена инженерным способом.

А как же массовые расстрелы? :)

Законы физики, как несложно догадаться, имеют приоритет над конституцией,


Это смотря где. В Австралии законы Австралии первичны. Именно так один из местных руководителей заявлял.

И вообще — классика:
«Прошла зима, настало лето.
Спасибо Партии за это!»
Очень интересная статься, причём поднимающая достаточно фундаментальные проблемы дисциплины!

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

В голову приходит Geant4, там настраиваются взаимодействия, которые подлежат расмотрению, но всё-таки сфера применения ограничена монтекарловским моделированием
И как после этого инженера, программисты и математики могут утверждать, что математика это мерило научности? Конечно если математики выполняют свои доказательства имеющие огромные пробелы, то есть доказательства не завершенные, то как они могут сравнивать свою науку с исторической наукой, у которой все эти проблемы решены. А те которые есть, во многом вызваны вмешательством технарей в историю?
Я согласен, что в математике есть проблемы, но, судя по всему, у нас до сих пор нет ничего надёжнее математики. Но я совершенно не согласен, что в исторической науке эти проблемы решены!
В математике законен плагиат, а в истории нет. В истории есть историография, которая позволяет отследить кто что писал. Изучение, что написали другие историки важнее чем собственные исследования, и это изучение историографии вопроса дает понимание в целесообразности собственного исследования.
Прямо противоположные взгляды и результаты исследований историков и востоковедов обуславливаются либо разными подборками фактологии. Либо точками зрения противоборствующих групп. Либо прямыми фальсификациями. И что то мне подсказывает, что прямая фальсификация выгоднее именно технарям. Историк предпочтет давать негативную оценку, замалчивать, но не лгать напрямую. Хотя и такое случается.
Но, его легче разоблачить, чем профессора физики.
Историки признают, что все знания в той степени конечно субъективны, но они стремятся к объективности искусственно. Сам специалист должен отделить свое личное мнение от результатов исследования.
А что наши физики? Они просто признали, что наблюдатель влияет на явление и остались довольны своей объективности.
Проблема в том, что нет негуманитарной науки, даже машиностроитель без своего гуманитарного опыта и изучения примеров других станков (а это и есть историческое изучение), не сможет сконструировать хороший в эксплуатации станок.
А технари по сути это не более чем умельцы крутить гайки. Инженер -конструктор не может быть технарем!
Если инженера считают себя технарями то пусть не плачут о зарплатах ниже зарплат рабочих!
Для Конструктора назвать себя технарем это значит панибратствовать с рабочими. В СССР было развито панибратство в адрес рабочих, через их чрезмерное восхваление в научпопе.
Пример: Монархи изобрели дворян для борьбы с знатью. Но, как только король или царь стал первым дворянином, то не продержались и двухсот лет как их свергли. Потому, что дворянин это дворня. А помазанник божий не может быть первым из слуг. Так и с инженерным делом и вычислительной техникой.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий

Публикации

Истории