Совсем невмоготу? До 1-го апреля-то всего ничего ж осталось!

>>4863704

>Можно тут математика-тред устроить?

Если только это будет /b/акотред.

>Люблю поболтать о математике.

/sci/

>Если только это будет /b/акотред.

На такой и рассчитываю!

>/sci/

Пускай будет филиалом!

Образ гомомрфизма изоморфен факторгруппе по ядру гомомрфизма!

>>4863715

> Пускай будет филиалом!

Ещё не закрыли, чтобы филиалы открывать.

>>4863720
Говоря проще, кообраз изоморфен образу!

>>4863721
Разве филиалы это нечто, что открывается, когда закрывается то, по отношению к чему филиал является филиалом?

Какая вам больше нравится математика: непрерывная или дискретная?

>>4863734
Та, которую сложно поместить в одну из этих двух категорий.

Мне арифметика больше по душе. Так что наверное дискретная. Хотя и у непрерывной математики есть своя романтика. Нечто неуловимо напоминающее космологию и квантовую физику.
А вам какая арифметика больше нравится, теоретическая или формальная?

>>4863758
Квантовые штуки это как раз нечто между дискретным и непрерывным мне кажется! А арифметика мне никакая не нравится, она вгоняет меня в тоску!

>>4863762
На этом тред можно закрывать но перед этим скинь пак на Курису, если не бака

>>4863764
На этом нужно закрывать обсуждение того, что тред нужно закрывать! Пак собираю по ходу дела сам, если будешь в треде активным, то скину!

>Гуманитарии беснуюстя

>>4863775
Кого цитируешь?

>>4863775
Слово "гуманитарий" воспринимаю исключительно как комплимент, а не как пейоративность! Тем не менее, мог бы задать какие-нибудь вопросы, чтобы поднять беснование на тот нужный дискурсивный уровень, который не вызывал бы у тебя отторжения, заодно бы и другим пример подал!

>>4863781
Не вижу смысла, математика для меня - ещё та бесовщина. И поднимать уровень дискуссии - только раздражать себя же самого. Я лучше выпью чаю да съем бутерброд с арахисовым маслом.

>>4863780
Себя из другого треда с другой борды.

>>4863782
Что по-твоему тебя должно раздражить? Сама математика или проявление чьей-то в ней некомпетентности? В любом случае, слишком уж легко ты раздражаешься по слишком невинным поводам, раздражение слишком ценный ресурс, чтобы вот так им туда-сюда разбрасываться!

>>4863723
Образ-кообраз.

>>4863790
Ядро-коядро
Алгебра-коалгебра
Модуль-комодуль
Предел-копредел
Декартво квадрат-кодекартов квадрат
Кофе-фе
Коко-кококо

>>4863762

> А арифметика мне никакая не нравится, она вгоняет меня в тоску!

Даже теория чисел?

>>4863796
А кроме теории чисел бывает какая-то ещё?

Предлагаю заставить ОПа считать в слух до числа Грэма.

>>4863800
Хорошо, что не до числа райо!

>>4863785
Сама математика как объект интереса.

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

>>4863804
Рад, что твоё желание того, чтобы наш тред выполнял образовательную функцию удовлетворено, хотя оно мне и кажется странным!
>>4863803
Тебе важно, чтобы мы придерживались некоторых рамок приличия в отношении своего интереса математики потому же почему и, скажем, стыдно взрослым состоятельным мужчинам увлекаться комиксами или по какой-то другой причине?

>>4863814
Причина сугубо религиозная. Даже капча указывает на это.

>>4863817
Может это обозначения синуса и она наоборот указывает на то, что тебе нужно написать в кои-то веки нечто математичное!

>>4863825
Вычислять синусы - грешно

>>4863832
Тогда не стоит их вычислять!

>>4863834
Однозначно. Матетматика - величайший грех. Я очищу этот тред!

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

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

>>4863837
Это хорошо, люди для которых математика невыносима, определенно добавят интересности!
>>4863839>>4863840
Это да, школьная математика вообще странное образование.

>>4863840
Э? Но ведь тригонометрические функции от действительных чисел всегда действительные. И эти функции в действительных числах имеют простое и понятное приложение в геометрии. Какой смысл менять их на комплексную экспоненту? Конечно, она полезна, когда у тебя там частота и фаза, но всё же.

>>4863849

>математика

Теория типов — это математика?

>>4863855
А каких типов, стрёмных?

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

>>4863849
Ага, а последовавшие за ними пределы, логарифмы, матрицы воспринимались только как «извините, я вернулся в первый класс?», очень странное ощущение.

С чего начинать изучать фило^Wматематику?

>>4863855
Думаю всё же компьютер саенс, чисто математических вопросов там нету.
>>4863852
По модулю всего сказанного не очень даже понятно, зачем тригонометрические неравенства нужно решать даже с точки зрения математического образования, не говоря уже о практике!
>>4863862
Это да!

А что думаете по поводу Metamath Proof Explorer
http://us.metamath.org/
http://us.metamath.org/mpegif/mmset.html
http://us.metamath.org/downloads/metamath.pdf
Система для формализации и верификации математических доказательств, работающая через систему переписывающих правил

>>4863865
А какие вопросы являются чисто математическими?

>>4863873
Я думаю, что Пролог сделали лет тридцать назад.

>>4863864
Мне кажется Гельфанд Шень "Алгебра" хороший старт. Можешь ещё попробовать разные системы типа khan academy и brilliant org, с ними не очень знаком, но вроде беглым взглядом показалось, что для новичков норм.
>>4863873
Гильберт стайл пруф чекеры, да ещё и которые кодируют всё в ZFC это, мягко говоря, прошлый век.
>>4863875
В этом контексте: вопросы о всяких выразительных и доказательных силах, о семантиках и моделях и такое всё, а вопросы об эффективных программных реализациях о том, как что-то конкретное закодировать и вопросы типа "можно ли придумать какой-то ещё синтаксис, чтобы кодировать стало ещё удобнее" мне кажется всё же больше по части CS

>>4863878

> Гильберт стайл пруф чекеры, да ещё и которые кодируют всё в ZFC это, мягко говоря, прошлый век.

Что значит "Гильберт стайл"?
Там нет встроенного обязательного ZFC. Ты вместо ZFC можешь свою аксиоматику придумать, описать как набор переписывающих правил, и из нее выводить следствия (леммы, теоремы).

>мягко говоря, прошлый век.

А что не прошлый век?

>>4863878
Но ведь как минимум гомотопическая теория типов уж точно не про реализацию, а как раз таки про доказательства. Изоморфизм Карри–Ховарда и вот это вот всё.

>>4863879
Гильберт-стайл значит отсутствие типов, малое количество правил вывода, схемы аксиом. Это всё конечно да, но основная база знаний в которой наиболее нетривиальные теоремы доказаны у них на ZFC, а обязательна она или нет - какая, в общем-то, разница. По-поводу ноу-хау в пруф-чекинге я точно не знаю, но думаю всякие HoTT и её вычислительные интерпретации, вроде кубических типов от того ученика Воеводского, которого я забыл как звать.

>>4863864
С Демидовича и Финкельштейна.

>>4863882
А почему ты противопоставил доказательства и реализацию? Как раз задача вида "закодируйте доказательство чего-то там" она очень реализационная, если такое слово есть. Не знаю ни одной чётко сформулированной проблемы касательно HoTT, даже тот самый список на нлабе меня не устраивает, потому что все формулировки там очень wishy-washy, что среди математиков неприемлимо, а в среде CS - как раз.

>>4863889
Ты явно в этом больше разбираешься, но насколько я знаю, HoTT по крайней мере кто-то планировал использовать в качестве фундамента для всей математики (вместо теории множеств сто лет назад и чего там ещё). Но при этом сам он математикой не является?..

>>4863891
Ну ты как-то слишком серьезно к слову "математика" относишься, я лишь говорил, что оно для меня не ощущается как математика и люди, которые занимаются HOTT тусят среди CS и публикуются чаще всего в СS журналах, но наверняка этим кто-то и на математических факультетах тоже занимается, поэтому пусть будет математика, мне не жалко!

>>4863886

>Гильберт-стайл значит отсутствие типов, малое количество правил вывода, схемы аксиом.

Что значит "отсутствие типов"? Через системы переписывающих правил ты можешь себе сделать любые мыслимые типы. Знаешь что такое "система переписывающих правил?"

Что значит "малое количество правил вывода"? Каждая лемма/теорема это новое правило вывода, т.е. новый способ переписывания, т.е. новый способ замены X на Y. Если например надо доказать что 1 + 1 = 2 и у тебя где-то есть доказанная теорема вида
Если мы видим X + 1 Где X - один единственный символ из множества от 0 до 8 включительно, то вот набор правил замены
0 + 1 -> 1
1 + 1 -> 2
2 + 1 -> 3
...
8 + 1 -> 9
Но если X это 9 то замена будет
9 + 1 -> 10

Применяем это правило (теорему) к выражению 1 + 1 = 2 - получаем 2 = 2
А потом находим правило, что если слева и справа у нас два одинаковых числа, то это правда. Все, мы доказали что 1 + 1 = 2

>схемы аксиом

А что и как ты собираешься доказывать (выводить) без аксиом?

>>4863892
Просто я со стороны думал, что вся современная математика скорее такая. А какая на самом деле современная математика?

>>4863894

>Что значит "отсутствие типов"? Через системы переписывающих правил ты можешь себе сделать любые мыслимые типы.

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

>Что значит "малое количество правил вывода"?

Значит то, что они же сами пишут в строчке " the only rules of inference are the (infinite) specific instances of the modus ponens and generalization schemes", то есть у них только 2 правила вывода, в противовес системам с натуральным выводом, где наоборот правил вывода много, а схем аксиом мало.

>А что и как ты собираешься доказывать (выводить) без аксиом?

Я не про аксиомы, а про схемы аксиом. Почитай на их же сайте абзац "axioms vs axiom schemes".

Вообще ты странный мод для разговора включил: будто я тебя сейчас в чём-то убеждать буду. Запомни: тут никто ни на что не претендует!

>>4863892
Ты так это сказал, будто бы мне жалко, и будто бы это я захотел тебе непременно доказать, что это математика. Мне как бы гораздо более всё равно.

>>4863901

>Вообще ты странный мод для разговора включил: будто я тебя сейчас в чём-то убеждать буду. Запомни: тут никто ни на что не претендует!

Почему тогда у тебя аватарка такое серьёзное лицо делает?

>>4863895
Слишком широкий вопрос, но вот мне кажется что вопросы кодирования чего-то там в каком-то там синтаксисе - это точно мимо.
>>4863903
Мне показалось, что тебе показалось, будто бы я HoTT чем-то обидеть хотел когда сказал, что это CS. Но если нет, то и хорошо?
>>4863904
Разве же серьезное? Мне кажется что это лицо в смятении. А вообще я никогда не подбираю аватарку специально под сообщение.

>>4863913

> Слишком широкий вопрос, но вот мне кажется что вопросы кодирования чего-то там в каком-то там синтаксисе - это точно мимо.

А если хотя бы кусочек?

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

>>4863901

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

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

>Значит то, что они же сами пишут в строчке " the only rules of inference are the (infinite) specific instances of the modus ponens and generalization schemes", то есть у них только 2 правила вывода, в противовес системам с натуральным выводом, где наоборот правил вывода много, а схем аксиом мало.

Почему это плохо? В чем системы с натуральным выводом лучше этого? Там есть сквозное доказательство всего и вся, начиная с самых основ?

>Вобще ты странный мод для разговора включил: будто я тебя сейчас в чём-то убеждать буду. Запомни: тут никто ни на что не претендует!

Ты неправильно интерпретируешь мое поведение. Я просто хочу разобраться, что тут лучше и что тут хуже. Например, нужны ли все эти типизации, или они только мешают и усложняют реализацию? А что насчет всяких SMT решателей, Coq, Isabelle/HOL, Idris, Agda? Почему их так много, и насколько им можно доверять? https://github.com/clarus/falso вот например в Coq смогли доказать ложь из-за бага в реализации самого Coq, ну куда это годится?

>>4863932
Ну а какой всё-таки раздел математики сейчас генерирует больше всего инноваций?

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

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

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

>>4863938
Ну давай я скажу "программа ленглендса" (алгебра + геометрия), если тебе совсем-совсем конкретика нужна.

Test

Слишком серьёзно. А говорили что баковать будете.

>>4863946
Так а ты побакуй, а я поддержу!

>>4863942

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

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

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

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

Кстати, что вообще лучше почитать про основания математике, чтоб прям на пальцах всё объяснялось?

>>4863959

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

Ну так этим как раз программисты и занимаются в основном! А как оно работает я знаю, но за ревью спасибо всё равно!

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

Естественно ничего такого нет, естественно все могут ошибаться, обещаю, что мои подколки если и не будут не злые, то по крайней мере в них тоже не будет ничего такого! Но программы проверки нужно делать такими, чтобы в них удобно было, собственно, кодировать сложные доказательства, а аккуратную реализацию оставлять на откуп хорошим CSникам. В конце концов, 100%ой уверенности не достигнуть никогда, потому что вдруг в ядре процессора ошибка (которое устроено ой как сложно, по крайней мере документации современных процессоров часто занимают несколько тысяч страниц)?

>Кстати, что вообще лучше почитать про основания математике, чтоб прям на пальцах всё объяснялось?

Это хороший вопрос, есть область знаний связанная с метаматематикой, то есть с метаматематическими свойствами теорий, вроде теорем Гёделя, Лёба, Тарского, Тенненбаума и тд, это лучше в Cori Lascar "Mathematical Logic course with exercises" мне кажется очень хороший учебник, но в сети вроде нету, есть ещё пост Тао https://terrytao.wordpress.com/2009/04/10/the-completeness-and-compactness-theorems-of-first-order-logic/ очень хорошее ревью на основые теоремы мат.логики. А если ты конкретно об синтаксисе оснований, кодировании и всём таком, то не знаю даже, читай оригинальные работы мартина лёфа и после этого HoTT book (она очень хорошо написана и легко читается).

>>4863855
Да. Любая работа с/в формальные языки - математика.

>>4863991
Любой формальный язык, есть алгоритм. Алгоритм, это программа для некоторой машины Тьюринга. Любую машину Тьюринга можно привести к другой, в том числе, построенной на чистой математике.

Всё, что можно представить формальным языком, есть математика.

Видел где-то такое.

>>4863991
Надеюсь хоть, что не любая математика - это работа, а то работать не люблю очень!
>>4863994
Машинна Тьюринга - это и есть программа, а не приёмник программ, и это и есть математическая абстракция программы на языке программирования, а не так, что некоторые машины тьюринга "внутри математики", а некоторые "вне её". А про "всё что можно представить формальным языком - математика" мне кажется что нет! Думаю математика находится на уровне той истории, для которой нужно придумать формальный язык, чтобы её красиво оформить, а не на уровне самого формального языка, поэтому матматики основания и не очень чтут.

>>4863984

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

Нет, я тут не согласен.
Процитирую фрагмент с сайта Metamath http://us.metamath.org/

> Unlike most other systems, Metamath attempts to use the minimum possible framework needed to express mathematics and its proofs. Other systems do not consider that aspect necessarily important, and their underlying computer programs can be large and complex in order to perform mathematical reasoning at a higher level. Metamath's proofs are often quite long compared to those of other systems, but they are completely transparent with nothing hidden from the user. All reasoning is done directly in the proof itself rather than by algorithms embedded in the verification program. Metamath is unique in this sense, offering an alternative approach for those attracted to its philosophy of simplicity.

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

>В конце концов, 100%ой уверенности не достигнуть никогда, потому что вдруг в ядре процессора ошибка (которое устроено ой как сложно, по крайней мере документации современных процессоров часто занимают несколько тысяч страниц)?

Ядра процессоров кстати доказывают с помощью формальных методов, тех же SMT решателей. Можно спроектировать очень простой процессор, доказать его корректность (т.е. сооветствие некоторой спецификации) и потом на нем же запустить пруфчекер, проверить доказательство корректности его самого. Если так сделать, то уверенность будет хоть и не 100%, но очень большая.

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

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

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

Грубо говоря, утрируя ситуацию в бесконечность раз, представим глупый синтаксис следующего рода: он любой текст переводит в тождественную истину, или любую другую тождественно чекаемую теорему на МЛТТ, и вот я пишу на этом более сложном синтаксисе "гипотеза Римана верна, мамой клянус" а оно хоп и скомплировалось мне, уверенность какого толка это должно мне дать?

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

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

Это всё только моё мнение, конечно.

>>4864011

>на МЛТТ

не на млтт, а на метамате, ну тут неважно конечно

>>4863704
Математика — царица полей.

>>4864011

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

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

>Как я узнаю, что промежуточные препроцессорно-сгенерированные теоремы на метамате логически соответствуют той теореме, которую я доказываю и в более сложном синтаксисе?

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

>>4864011

>Грубо говоря, утрируя ситуацию в бесконечность раз, представим глупый синтаксис следующего рода: он любой текст переводит в тождественную истину, или любую другую тождественно чекаемую теорему на МЛТТ, и вот я пишу на этом более сложном синтаксисе "гипотеза Римана верна, мамой клянус" а оно хоп и скомплировалось мне, уверенность какого толка это должно мне дать?

Ну очень просто. Если у тебя доказано что "он любой текст переводит в тождественную истину, или любую другую тождественно чекаемую теорему на МЛТТ" то все супер, и гипотеза Римана верна.

>>4864017

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

И как ты собираешься не доказать, но хотя бы даже сформулировать утверждение об этом? Чтобы хотя бы сформулировать "это было по смыслу в точности то же самое", то наверное у них должен быть один смысл слова "смысл" иначе говоря, у них должна быть одна и та же семантика, но если у них одна и та же семантика, то наверное "более сложный синтаксис" не такой уж более и сложный? Ведь более сложный синтаксис заводят, чтобы думать о более сложных объектах, я работаю в HoTT, чтобы думать о его термах как об именах объектов и морфизмов некоторого специфического (\infty,1)-топоса, каким образом я хотя бы сформулирую "такая-то интерпретация HoTT в metamath сохраняет смысл", если я даже не могу насытить термы metamath тем же смыслом, что и термы HoTT?

Даже не утрируя ситуацию, представим что у нас есть язык metamath и машинный код, все валидные термы которого, - это просто конечные строки из 0 и 1. Каким образом по твоему можно доказать, что отображение некоторого доказательства того, что 2+2=4 cо всеми шагами в строку вида "0010111010100111...00101" сохраняет смысл? И вообще, какой самостоятельный смысл у строки "0010111010100111...00101" может быть в отрыве от всякого кодирования? Или доказательством будет ссылка на факт, что "0010111010100111...00101" это код соответствующего доказательства в metamath, при чём тут смысл тогда?

>Ну очень просто. Если у тебя доказано что "он любой текст переводит в тождественную истину, или любую другую тождественно чекаемую теорему на МЛТТ" то все супер, и гипотеза Римана верна.

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

>>4864020

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

Это про проекции Футамуры-Турчина, суперкомпиляция, преобразование программ
https://ru.wikibooks.org/wiki/Основы_функционального_программирования/Трансформация_программ
https://youtu.be/UWgBqQvj1gc https://habr.com/ru/post/47418/
Теория компиляции... У меня от нее голова кружится. Но я попробую сформулировать. Не уверен что всё напишу правильно, если что - переспроси.
Вот допустим HoTT - некий язык. Есть интерпретатор HoTT которому если скармливаем доказательства на языке HoTT и он говорит "True" если доказательство верно или "False" если нет. Пусть он будет вообще мамой клянус 100% корректный (ЭТО ВАЖНО. Будем считать что реализация интерпретатора это его спецификация и есть. Иначе надо тогда понять, в какой теории описана спецификация самого языка, т.е. описано то, как или каким образом формулируется ответ "True" или "False" на ту или иную входную строку, и это надо перевести в интерпретатор)
То же самое, есть у нас интерпретатор Metamath которому скармливаем доказательства на соотв. языке и он говорит: "True" если доказательство верно или "False" если нет. Он тоже 100% корректный. Транслятор из HoTT языка в Metamath язык - какими он свойствами должен обладать? Очень просто - он должен в ответ на любую корректную с т.з. языка HoTT строку выдавать корректную с т.з. языка Metamath строку такую, которая будучи переданная на вход интерпретатору Metamath, то он будет выдавать "True" если "True" выдаст на исходную строку сам интерпретатор языка HoTT, и выдаст "False" если в точности то же самое выдаст HoTT интерпретатор в ответ на исходную строку HoTT. Это свойство транслятора и надо доказывать.
И получается, что если например в HoTT языке ты докажешь гипотезу Римана, и если даже при трансляции из HoTT в Metamath ты получаешь какую-то ерунду, типа доказательства для равенства 2+2=4 то это даже и неважно, т.к. у тебя есть доказательство для транслятора, что если там правда, то и там правда. Этого уже будет достаточно. Хотя это и нафиг не надо, раз у тебя есть по условию 100% гарантия корректности интерпретатора HoTT. Но ты спрашивал как это сформулировать - я ответил. Надеюсь, не слишком всё запутано.

>Даже не утрируя ситуацию, представим что у нас есть язык metamath и машинный код, все валидные термы которого, - это просто конечные строки из 0 и 1. Каким образом по твоему можно доказать, что отображение некоторого доказательства того, что 2+2=4 cо всеми шагами в строку вида "0010111010100111...00101" сохраняет смысл?

Ну ок, попробуем. Первый вопрос - откуда взялась строка вида "0010111010100111...00101"?
Допустим, существует некая функция f(x) написанная в тех же машинных кодах, которая принимает строку на языке Metamath, и возвращает "00100..." который делает то же самое, что и Metamath, которому скормили такую же точно строку на языке Metamath. Вопрос - как это доказать?
Можно действовать следующим образом. У нас есть документация на машинный код. Описываем его в metamath т.е. пишем интерпретатор машинного кода внутри Metamath на языке Metamath. Потом цепляем нашу функцию f(x) к этому интерпретатору, чтобы она им исполнялась. Дальше пишем теорему, что для любой строки справедливо, что если ее подставить в функцию f(x) (которая интерпретируется интерпретатором машинного кода) то она сгенерирует такую строку "00100..." которая будучи проинтерпретированной интерпретатором машинного кода, выдаст тот же результат, что и выдаст сам метамат, который, если надо, тоже можно в самом метамате описать.
Вообще, Машину Тьюринга (МТ) вполне можно описать на метамате. В МТ можно написать реализацию точно такой же МТ и потом можно даже доказать, что та МТ запущенная внутри МТ в ответ на любой код будет такая же по поведению, как и МТ сама по себе, лол.

>>4864054
Ещё раз, если он 100% корректный, то зачем мне metamath в качестве предыдущего шага? Если он не 100% корректный и мне нужен metamath чтобы повысить свою уверенность в том, что он корректный, то какого сорта уверенность я получу от того, что гипотеза Римана на HoTT транслируется в доказательство "2+2=4" на metamath?

А давайте вместо "metamath" говорить "me tomato"?

>>4864130
Хорошая идея!

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

>>4864138
Ты молодец всё равно отдельную историю можешь рассказать, если хочешь! Но ещё никто вроде не умничал!

>>4864015
Математика — царица лолей.

>>4864155
Царица с интегралом!

>>4864125

>Ещё раз, если он 100% корректный, то зачем мне metamath в качестве предыдущего шага? Если он не 100% корректный и мне нужен metamath чтобы повысить свою уверенность в том, что он корректный, то какого сорта уверенность я получу от того, что гипотеза Римана на HoTT транслируется в доказательство "2+2=4" на metamath?

Есть более глубокий вопрос. Достаточно ли ты четко сам понимаешь, что именно представляет из себя HoTT, чтобы на основании спецификации HoTT и реализации самого проверятеля-решений-через HoTT убедиться в ее безошибочности? https://github.com/HoTT/HoTT вот у нас этот самый HoTT описан на языке Coq. Как я уже показывал, в Coq иногда бывают баги, из-за которых можно доказать ложь. Откуда мне знать, что в процессе описания HoTT теории там нигде никто не доказал ложь? В корректность самого Coq можно только уверовать, а сам Coq запрограммирован на языке OCaml в который тоже нет 100% уверенности...
Попробую через аналогию. Намного проще написать 100% корректный интерпретатор языка Brainfuck, чем написать 100% корректный интерпретатор машинного кода для некоторого нетривиального процессора. Так вот, интерпретатор языка Brainfuck это считай что Metamath, а HoTT (который описывается в Coq теории) это как интерпретатор машинного кода для процессора. И там и там у нас будет тьюринг-полнота, т.е. не будет вообще ничего, что можно выразить там, но нельзя там.
Если у тебя есть некая теория (язык) HoTT и существует способ на машине Тьюринга за конечное число шагов для синтаксически корректного (well formed formula) доказальства на HoTT точно понять, правильное это док-во или нет, то этот процесс проверки корректности доказательства вполне может быть переписан в Metamath, и у тебя будет больше уверенности, чем от Coq + OCaml в котором этот HoTT сейчас реализован. Надеюсь, так более понятно...

>>4864160
Собственным или несобственным?

>>4864165
Неопределенным!

>>4864163
Вопрос о том, насколько я убеждён в безошибочности HoTT мне не кажется интересным, потому что для меня кодирование доказательства на любом пруфере не делает его более убедительным. А то, что в какой-то уровень всё равно придётся поверить без всяких аргументов и так понятно, просто для меня это уровень "доказательства написанного на английском языке, и проверенным сообществом профессиональных математиков".

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

>>4864165
Тот, который спаривание цепи с коцепью!

>>4864170

>Вопрос о том, насколько я убеждён в безошибочности HoTT мне не кажется интересным, потому что для меня кодирование доказательства на любом пруфере не делает его более убедительным.

А что делает?

>А то, что в какой-то уровень всё равно придётся поверить без всяких аргументов и так понятно, просто для меня это уровень "доказательства написанного на английском языке, и проверенным сообществом профессиональных математиков".

Да. И желательно чтоб тот уровень, в который надо верить, был как можно более маленьким. И Metamath в этом плане лучше, чем HoTT работающий через Coq.

>(хоть она и не совсем корректна, потому что у языков программирования общая семантика более-менее есть, в отличии от пруверов)

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

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

Ну хотя бы потому, что сам брейнфак намного проще, чем аппаратный уровень. В него как-то проще поверить.

>Да. И желательно чтоб тот уровень, в который надо верить, был как можно более маленьким. И Metamath в этом плане лучше, чем HoTT работающий через Coq.

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

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

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

>>4864185

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

Лол, вспомнилась цитата:
«Есть два подхода к программированию. Первый — сделать программу настолько простой, чтобы в ней очевидно не было ошибок. А второй — сделать её настолько сложной, чтобы в ней не было очевидных ошибок.»
Tony Hoare. Профессор, занимался реализацией Алгол 60, сейчас исследователь в Microsoft Research.

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

Второй вариант мне кажется лучше первого

>>4864170

> для меня это уровень "доказательства написанного на английском языке, и проверенным сообществом профессиональных математиков".

Слышал про замощение плоскости пятиугольным паркетом? Давно было "доказано", что вот только такими вариантами выпуклыми прямоугольниками можно замостить плоскость, потом какая-то домохозяйка прочитала об этом в каком-то журнале и придумала контрпример. Сейчас вроде бы появилось окончательное доказательство, что типов замощений ровно 15
https://youtu.be/hkhaipY3JmU?t=5064 https://ru.wikipedia.org/wiki/Пятиугольный_паркет

Никогда не любил математику в школе. Сейчас бы с каким-нибудь преподавателем с радостью разбирал задачки с самого 4-го класса и выше.
Детство, всё-таки, странная вещь. Вроде говорят, что в детстве проще всего учиться, больше всего информации впитываешь, но даже если вспомнить предметы, которые мне нравились, я точно помню, что как-то осознанно не учился. А сейчас вот с радостью. И во сколько же лучше всего учиться? Это ещё вопрос Во какой! Его надо задать, а потом на него ответить. Ну, собственно, я его уже задал.
Такая вот математика.

>>4864185

>Осталось только найти оракула, который скажет, что функция проверки корректности на бреинфаке - это действительно функция проверки корректности на бреинфаке, а не что либо ещё.

Что-то мне подсказывает, что оракул тут не требуется. Это можно попробовать доказать теми же самыми теорем чекерами, и это должно быть доказуемым утверждением.

>>4864194
Имеешь право, но если что я не верю интуиции программистов в вопросах математических доказательств.

>>4864198
Слышал, я кстати сейчас заглянул на энвики, и чего-то не увидел этой самой истории с несколькими итерациями доказательств опубликованных в журналах и последующих контрпримеров предъявленных домохозяйкой, о которой так любят все рассказывать. Но в любом случае, даже если она и была, то мне не кажется, будто бы если заставить каждого математика кодировать свои доказательства в пруфчекерах таких историй станет меньше, просто ошибки переместятся с уровня фактиеских на уровень "закодировано было совсем не то, что заявлялось", потому что я вот сейчас зашёл на метамас посмотреть fundamental theorem of algebra и вообще не понял, как в тех 20 строчках метамасного кода (пусть даже хорошо откомментированного) её там можно разглядеть, так что эти пруверы просто увеличат количество рабочих мест для умных программистов (что хорошо) и количество бюрократии (что плохо).

>>4864202

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

Но в корректность самого Coq ты почему-то веришь.

>>4864200
Думаю в том возрасте, когда чувствуешь любовь к знаниям и не чувствуешь отторжения от процесса обучения!
>>4864201
А мне кажется, что это принципиально неформулируемое утверждение, потому что то, что семантика для языка является семантикой ты можешь только объявить и постулировать.

>>4864210
Не верю и не не верю, вообще плевать на всё это мероприятие с пруферами если честно!

>>4864212

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

Что тогда эта семантика значит, если из нее нельзя вывести правила того, как пруфчекнуть (или иными словами, как проинтерпретировать) то, что в ней описано? Зачем и о чем она?
>>4864213

>Не верю и не не верю

Интуиционистская логика какая-то.

>>4864227
Не очень понял вопроса, семантика - это всегда некоторые абстрактные сущности мира идей, именами которых термы твоего языка эти сущности помечают, есть терм "2+2" как трёхсимвольная строка, а есть та самая четвёрека из стандартной модели натуральных чисел, которая и помечается этим термом, как именем. (Конечно можно рассмотреть всё с тз метаязыка в котором и семантика и синтаксис будут в одной вселенной, но это тут не имеет значения). Семантику никак не пруфчекнуть, иначе она была бы синтаксисом, ты можешь придумать некоторый синтаксис, который бы твою семантику описывал и пруфчекнуть его. Но если два синтаксиса придумывались с тем, чтобы описывать разные семантики, то у тебя нету никакого способа проверить, хороша ли твоя интерпретация одного языка в другой или плоха, кроме того, чтобы пользуясь своим чутьем построить некоторую интерпретацию и постулировать, что она хороша и при всех последующих рассуждениях нужно сверяться именно с ней.

>Интуиционистская логика какая-то.

Да, сходство есть! Тут она очень естественно вылезла и понятна даже на бытовом уровне, действительно, почему я должен решать, верно ли в моём мире А или верно не А, если меня это не очень-то и волнует?

>>4864227

> пик

Очень нехорошая формулировка, даже если это рассчитано школьников.

>>4864238
А какая формулировка правильная?

>>4864240
"Из высказывания и отрицания этого высказывания...", например.

Утверждения "У кафки рыжие волосы" и "У Кафки голубые волосы" противоречат друг другу, но оба ложны, потому что волосы Кафки -- черные.

В то же время, из утверждений "У Кафки рыжие волосы" и "У кафки не рыжие волосы" как раз верно ровно одно.

>>4864245
Теперь ясно, постараюсь так и запомнить!

>>4864245
Или у него нет волос!
так что нуже квалификатор - "у кафки есть волосы и ..."

>>4864247
А вдруг волосы не имеют цвета? Нужен ещё один квалификатор, вроде "у кафки есть волосы и они имеют цвет и ..."!

>>4864251

И вообще может и сам Кафка не существует

>>4864252
А обязательно ли нужно существовать, чтобы иметь волосы черного цвета? Что на этот счёт говорит логика?

>>4864254

Наверно да. если предполагается что кафка может или не может существовать, значит надо писать утверждение что он существует

>>4864254
https://math.stackexchange.com/questions/202452/why-is-predicate-all-as-in-allset-true-if-the-set-is-empty

>>4864255
Тогда лучше не предполагать, а то не люблю когда писать надо много!

>>4864257
Интересный факт, постараюсь так и запомнить!

>>4864257

здесь не all. если бы было "у всех кафок" тогда да, all.

>>4864247
Существуют волосы такие, что они растут из головы Кафки, при этом они рыжие!

А отрицанием тогда будет:

Не существует волос таких, что они растут из головы Кафки, или же эти волосы не рыжие!

>>4864262
Думаю нет, но спорить не буду!

>>4864261

>"у всех кафок"

>>4864267
Я взял на себя труд развернуть отрицание конъюнкции двух утверждений в дизъюнкцию их отрицаний. Какие умные слова-то!

Не знаю, как это делают настоящие математики, но зато я точно знаю, что not (a and b) == not a or not b

А спорить очень весело, просто не все это понимают!

>>4864237

>Не очень понял вопроса, семантика - это всегда некоторые абстрактные сущности мира идей, именами которых термы твоего языка эти сущности помечают, есть терм "2+2" как трёхсимвольная строка, а есть та самая четвёрека из стандартной модели натуральных чисел, которая и помечается этим термом, как именем.

Ну мы должны понимать, что именно закодировано в строке "2+2=4". Если семантика нам этого понять не позволяет, то непонятно вообще, что с этим делать. Вот например возьмем человека из прошлого, знающего допустим только римские цифры, но не знающего десятичной системы счисления с арабскими цифрами 0123456789, не знающего смыслов + и =. Что он сможет понять из строки "2+2=4"? Для него она не будет иметь вообще никакого смысла. Но если мы на понятном для него языке опишем ему смысл этого, то это тогда будет ему понятно, и он тогда сможет сказать, что это выражение, при таком смысле отдельных символов, является справедливым. Нужны синтаксис и семантика.
Вообще, что ты понимаешь под семантикой? Возьмем определение из вики https://ru.wikipedia.org/wiki/Семантика_(программирование)

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

Если твое определение таковым и является, то да, из знания синтаксиса и семантики будут следовать некие правила преобразования (переписывания), которыми можно доказать корректность выражения "2+2=4"
Например, путем последовательной трансформации "2+2=4" -> "3+1=4" -> "4=4" -> "4-1=4-1" -> "3=3" ... = "0=0" -> "TRUE"
Или я где-то ошибаюсь?

>>4864261
Если множество всех Кафок пустое то это то же самое по смыслу, что и "Кафки не существовует".

>>4864280
Возьми отрицание от \exists x (P(x) /\ Q(x) /\ R(x)) где P(x) = "x - волосы", Q(x) = "x - растут из головы Кафки", R(x) = "x - рыжие" тогда! Мне наоборот кажется, что немногие понимают, что спорить - не весело!
>>4864283
Позже напишу, но если коротко, определение на вики мне не нравится. Под семантикой, как я говорил, понимают ситуацию, когда некоторые абстрактные объекты именуются термами некоторого языка, сами эти абстрактные объекты частью языка не являются. Есть "идея числа 4" - это семантика, а есть термы "2+2" или "IIII" или "IV" - это синтаксис. В некотором смысле это понятие метаматематическое, но его можно сделать математическим поднявшись на уровень метаязыка и тогда можно работать с языком как с объектом и, скажем, можно в ZFC записать утверждение в духе "натуральные числа N являются моделью для языка PA", впрочем если мы так сделаем, семантика самой ZFC, которая на уровне метаязыка всё равно останется понятием метаматематическим.

>>4864262

>Не существует волос таких, что они растут из головы Кафки, или же эти волосы не рыжие!

Как-то слишком сложно. Лучше так:
Волосы на голове Кафки если и есть (их может и не быть!), то они точно не рыжие.
Вообще, вот интересный тест на логическое мышление: https://hr-portal.ru/pages/hu/logika.php

>>4864300
Думаю неправильно, либо "не существует рыжих волос на голове кафки" либо "любой объект или находится не на голове кафки, или не рыжий, или не является волосами", но спорить не буду!

>>4864297

> \exists x (P(x) /\ Q(x) /\ R(x)) где P(x) = "x - волосы", Q(x) = "x - растут из головы Кафки", R(x) = "x - рыжие"

"Для любого х: отрицание (P(x) /\ Q(x) /\ R(x))"
или же:
"Для любого х: отрицание (P(x) /\ Q(x)) \/ отрицание R(x)"

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

Попробуем так: "если множество волос, крепящихся к голове Кафки непустое, то это рыжее множество волос". Рыжее множество волос мы можем определить, например, по средней длине отраженных волн солнечного света, но это мелочи.

>>4864318
Это эквивалентно тому, что "все волосы на голове кафки рыжие", потому что, как скидыввали тут пытливые умы, для пустого множества любое утверждение верно. В моих обозначениях это \forall x ((P(x) /\ Q(x)) -> R(x))

>Но я не уверен, что предложенная тобой модель подходит.

А подходит для чего? Мы какую-то цель преследуем? Я просто не в курсе!

>>4864319
Так ты же придумал большую формулу с функциями и уголочками как аналог утверждения про рыжесть Кафки!

> Это эквивалентно тому, что

Что -- "это"? Я не понимат. Видишь как весело!

>>4864300
Да, скорее всего это подходит. А этот тест мне уже кидали, он показался мне скучным.

>>4864333
Действительно я придумал!

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

Если мы хотим получить отрицание, можно сказать так: "подмножество из множества всех рыжих волос, для которого было бы верно, что они растут из головы Кафки - пустое!". Или "нет таких рыжих волос, которые б росли из головы Кафки"

>>4864237

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

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

>>4864376
Не знаю что такое "свойство корректности доказательств", хотт не о доказательствах, а о высших индуктивных типах, а в metamath естественным образом никаких высших индуктивных типов нету.

>>4863704
А по каким материалам можно начать изучение математики, если отрывками знания есть и со школы, и с университета, но много пробелов и хотелось бы получить хороший уровень знаний математики и понимания тоже?

>>4864378
Гельфанд Шень "Алгебра" для вката, если всё оттуда знаешь, то наверное какой-то хороший учебник по алгебре типа aluffi algebra: chapter 0. Я не знаю, на твоём месте я бы больше кусочно развивался, читай блоги, матоверфлоу, гугли какие-нибудь обзоры по темам, о которых слышал краем уха, смотри лекции на лекториуме и тд и тд

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

>>4864384
Я бы советовал решать проблемы по мере их возникновения и подучивать какие-то темы когда ты обнаружишь, что твоего знания фатально не хватает. Посмотри khan academy или brilliant org, там весь энтрилевел довольно неплохо собран. А в учебниках по математике не для математиков плохо разбираюсь, к сожалению.

>>4864391
Спасибо за советы.

Напишите вопросы какие-нибудь, а я утром посмотрю и мне будет очень приятно!

>>4864377

>Не знаю что такое "свойство корректности доказательств", хотт не о доказательствах, а о высших индуктивных типах, а в metamath естественным образом никаких высших индуктивных типов нету.

В metamath естественным образом вообще почти ничего нет, кроме переписывания.
The complete specification of the Metamath language is only four pages long (Section 4.1, p. 106). http://us.metamath.org/downloads/metamath.pdf#page.106
Все эти высшие индуктивные типы там тоже вполне представимы. Теория зависимых типов для Metamath описана: https://github.com/digama0/dtt.mm . HoTT этот тоже можно описать, тут нет никакой проблемы. Зависимые типы и этот HoTT могут добавить выразительности, но разве они позволяют доказать что-то, что без них доказать никак нельзя (не считая доказательств, связанных с самой теорией зависимых типов и HoTT) ? Т.е. например если доказывать теорему Пифагора, то это можно доказать хоть с HoTT, хоть без HoTT, просто с этой теорией типов это может быть удобнее, и можно например проще обобщить теорему пифагора на более общий случай (например пространственная теорема пифагора, можно и для 4-5-6 мерного пространства что-то такое описать, пользуясь зависимыми типами для координат точек в n-мерном пространстве, которые специализируются (зависимы от) "мерностью" пространства, точки в котором они описывают).

>>4864433
Можешь объяснить значение теорем Гёделя о неполноте? Я правильно понимаю, что теоретически внезапно может оказаться, что большая часть знаний о математике не верна? И есть ли такие направления в математике, на которые эти теоремы не влияют?

>>4864368

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

Мне кажется, что необходимо рассмотреть множество всех волос на голове, а остальное -- вопрос технический.

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

Или вообще, определять цвет волос по паспорту. Как пол или год рождения, только цвет волос. И заморачиваться не придется!

>>4864384
Верь в себя и решай проблемы по мере их возникновения! Я бы еще посоветовал тебе освежить знания в линейной алгебре, чтобы работать с векторами и матрицами.

А так, в ML есть готовые библиотеки, порой позволяющие решать задачи, вообще не зная, как это внутри работает.

>>4864464
Конечно всё можно сэмулировать на всём, мне просто не кажется это интересным и не кажется что эмуляция на метамасе должна добавлять мне больше уверенности, чем на С. Про теорему пифагора - принципиально наверное можно, но будет довольно сложно доказывать вещи такого толка, по крайней мере я с наскоку не знаю как, HoTT она больше под всякую топологию заточена скорее.
>>4864549
Теоремы Гёделя говорят, что истинность не тождественна доказуемости, и что в принципе есть недоказуемые утверждения, которые тем не менее истинны. В принципе то, что найдётся противоречие в арифметике Пеано, скажем так, ничему не противоречит, то есть ничему не противоречит что используя всякие простые рассуждения про натуральные числа кто-то получит, что 0=1. Но на такое надеется было бы слишком оптимистично, всё-таки метаматематические интересности такого большого размаха - это не нечто, что находится каждый день. Нет, теорема Гёделя сугубо метаматематический эффект, свойственный любому достаточно выразительному синтаксису, поэтому просто так от неё отмахнуться не получится.

>>4863804

>полезный

Практически бесполезный для человека, который не занимается этим профессионально каждый день.
Все расчудесные знания выветрятся без упорной практики.
>>4863803
Смысл типа "интересоваться", если

>Все расчудесные знания выветрятся без упорной практики.

?

>>4864719
А почему у тебя такое сильное желание удерживать всё то, что ты однажды узнал?

>>4864725
Зачем изучать особо изощренную математику, если ты не хочешь внести свой личный вклад либо искусно приложить математику к науке?

>удерживать всё то, что ты однажды узнал

Тот же вопрос. Зачем? Надеюсь, ты не будешь оправдывать бесплодное умственное напряжение примитивным гедонизмом.

>>4864731
За тем же, зачем и некоторые люди годами изучают лор каких-нибудь звёздных воин или властелина колец, думаю.

>>4864731

>>удерживать всё то, что ты однажды узнал
>Тот же вопрос. Зачем?

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

>>4864738
Глупости. Во-первых, у тебя не настроен детектор. Во-вторых, "продукты по пять кило" это дикая редукция, практически нигилизм по отношению к интеллектуальным ценностям. Предположу, что ты это понаписал лишь бы вставить свои пять копеек дешёвого развесного мнения Сырны, но эти мнения может высказать любой гимназист, а вот решение актуальной задачи либо какое-то другое принципиально новое знание под ногами не валяется. Вот и назревает вопрос: зачем интересоваться просто так, не пытаясь ничего достичь и не ставя целей, упиваясь посредственным удовлетворением праздного любопытства? Это уровень NPC, а не человека мыслящего.

>>4864756
Терпеть не могу интеллектуальные ценности, человеков мыслящих и актуальные задачи. Глупости так глупости, что же поделать, если ты не хочешь меня понимать!

>>4864763
Хм, думаю здесь ты прав. Извини, что побеспокоил.

>>4864769
Можешь беспокоить и дальше, только не требуя от меня при этом, чтобы я тебя в чём-то убеждал! Хотя можешь и требовать, просто боюсь что отказ ты воспримешь на свой счёт и обидешься, а я этого не хочу!

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

>>4864778
Ландо: Введение в дискретную математику и Axler: Linear Algebra Done Right, не знаю насколько они помогут или не помогут тебе вкатиться, но учебники хорошие. Посмотри ещё видосы 3blue1brown по линейной алгебре, там анимации красивые и несколько важных интуиций объяснено.

>>4864641

>HoTT она больше под всякую топологию заточена скорее.

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

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

Топология редко нужна для прикладных вещей, она, по отношению к прикладным вещам, играет более описательную роль, чем вычислительную. Но с этой задачей она справляется неплохо, даже вон нобелевку по физике в 16 дали за формализм описывающий всякие toplogical phases of metter, не совсем понял о чём это, но выглядело не оч интересно, поэтому я не учил. Кроме фундаментальной физики приложений не знаю. (Если только всякие доказательство существования и единственности всяких диффуров через какие-то техники типа h-принципа или лефшеца не считать за приложения, но я в доказательствах существования ничего прикладного не вижу)

Сегодня всю ночь не сплю, поэтому можем болтать!

>>4864913
Ну ок, раз тут затрагивалась тема с доказывателями теорем, то какой софт для математиков еще нужен? Чем ты сам лично пользуешься, и что можешь посоветовать для своей области? Есть например Wolfram Mathematica, Maple, MATLAB, Maxima, Sage. Ты занимаешься исключительно проблемами, связанными с топологией, или есть что-то еще?

>>4864930
Я не занимаюсь проблемами связанными с топологией, я начал говорить о ХоТТ потому что так разговор зашёл, я занимаюсь абстрактной алг.геометрией и теорией представлений. Я никакой софт не использую, так что ничего не могу посоветовать, пару раз использовал вольфрам математику чтобы домашки делать на каких-то младших курсах и всё.

>>4864936

>я занимаюсь абстрактной алг.геометрией и теорией представлений.

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

>>4864936

> Я никакой софт не использую

Даже LaTeX? Или таки Word? (Понятно, что это не совсем тот софт, о котором спрашивали, но всё-таки в чём пишешь?)

>>4864950
Понимаю, но занимаюсь чем-то другим, не связанным с этим, криптография на эл.кривых использует алг.геометрию довольно примитивного уровня. Не знаю, в какой-то момент решил, что люблю её и стал ею заниматься. Про приложения - да, наверное только во всяких кодированиях и криптографии.
>>4864951
Латех на оверлифе.

Що у меня нашлось одначе.

>>4864966
Что кто-то жив я рад, но карта глупая!

>>4864966
Я бы поделил на Bullshit и Usable instrument.

мимохейтер

>>4864641

>Теоремы Гёделя говорят, что истинность не тождественна доказуемости, и что в принципе есть недоказуемые утверждения, которые тем не менее истинны.

Мне кажется, ты сильно упрощаешь. Например, имеют ли какое-то отношения теоремы Гёделя к парадоксу Рассела, канторову диагональному процессу и проблеме останова для машины Тьюринга? Мне кажется, имеют. https://web.archive.org/web/20170215130846/https://inf.1september.ru/2000/5/art/turing.htm
Только связь не очень очевидна. Походу, неразрешимость проблемы останова как раз следствие этой теоремы Гёделя о неполноте, и наоборот! А понять неразрешимость проблемы останова куда проще

>>4864981
Знаешь, что делают, когда кажется?

>>4864982
Зачем же что-то делать, если можно погуглить? https://cs.stackexchange.com/q/419 https://www.scottaaronson.com/blog/?p=710

>>4864983
Во-первых, вопрос переадресовывается >>4864981. Во-вторых, это более слабое утверждение:

>suppose we had a sound and complete (and recursively-axiomatizable, yadda yadda yadda) formal system F, which was powerful enough to reason about Turing machines

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

>>4864966
Это что-то похлеще китайской классификации животных от Борхеса.

>>4865015
Очень хорошая классификация, кстати.

>>4864966

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

Могли бы и экономику включить, почему нет?

Уноси где взял.

>>4865053

>Могли бы и экономику включить, почему нет?

А она там есть

>>4865068
Тогда надо аниме добавить.

>>4864979
Я бы делил на derived categories и bullshit. :з
>>4864981
Да конечно оно связано, вообще есть такая шутка, что самореферентность - это единственный инструмент для генерирования теорем в мат.логике. Но гёделя из проблемы останова действительно не очень тяжело вывести: достаточно запустить программу, которая запускает текст программы и одновременно ищет доказательство того, что эта самая программа не остановится в (скажем) формальной арифметике, если арифметика полна, то либо когда-то программа остановится из-за того, что мы её запустили, либо когда-нибудь будет найдено доказательство того, что она не остановится, то есть мы решили проблему останова, но мы же знаем что она не решается, значит арифметика неполна. С высокой точки зрения это всё инстанции изоморфизма карри-говарда, который говорит, что мат.логика и теория вычислимости это примерно о том же самом. Рассел это тоже по структуре аргумент в духе "самоприменимость всё ломает", поэтому ощущается похожим образом, но как его чисто формально свести к проблеме останова или гёделю не очень представляю.
>>4864985
Прям уж более слабое!

>>4865053>>4864966
Вот карта получше, только курису из-за неё не влезла.

Я бампну тред пусть тут так и не принято!

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

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

>>4865160
Функциональное программирование было по выбору (на Лиспе и на F#). Была математическая логика, логические основы программирования, рассказывали про лямбда-исчисление, про частично рекурсивные функции (и про машину Тьюринга само собой). Но про категории умолчали.

>>4865161
Плохо сделали, выходит!

>>4865160
А сам ты на чем-нибудь умеешь программировать?

>>4865164
На самом деле у меня этот вопрос всплыл, потому что я случайно наткнулся (не спрашивайте как) на печатную статью из журнала 1983 года под заголовком "О природе программирования" (хотя я её целиком не прочитал). Так там уже упоминается теория категорий. Значит нельзя сослаться на то, что курсы устаревшие, потому что даже в устаревших уже могло бы это быть. Вот мне интересно, почему тогда.

>>4865168
Да, умею, на плюсах, питоне, джаваскрипте, хаскелле и немного на агде и лине - немного пробовал их реализацию hott, но я скорее на upper-любительском уровне, а не профессиональном. Немного интересовался спортивным программированием и всякими алгоритмическими головоломками, поэтому даже знаю стандартный набор алгоритмов для этих самых соревнований.

>>4865169
Не знаю даже! Выучи её не в университете, если тебе интересно!

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

>>4865172

> Выучи её не в университете, если тебе интересно!

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

>>4865173
Если бы ты писал, например, на Rust, то мог бы использовать тип Result, который удовлетворяет монадическим законам, для более удобной, чем в C, обработки ошибок. Хотя для этого, в общем-то, не нужно знать, что он им удовлетворяет. И тем более не нужно про то, что монада это моноид в категории эндофункторов.

>>4865173
Это да, обидно наверное, когда учишь нечто, а потом оно тебе не понадобляется.
>>4865176
Ну это какие-то хитрые технические изыски, а если хочешь основной панчлайн, то почитай про syntax-sematics duality где-нибудь, и про категорные семантики каждой вершины лямбда-куба.

>>4865172

>Да, умею, на плюсах, питоне, джаваскрипте, хаскелле и немного на агде и лине - немного пробовал их реализацию hott, но я скорее на upper-любительском уровне, а не профессиональном

"лине" - это Gallina из Coq? Как соотносится программирования и математика, если говорить о языках неспециализированных (не Agda, не Gallina, а просто обычные языки для обычных программистов, вроде той же джавы)? Помогают ли они понимать математику, и помогает ли математика понимать их?

>>4865185
Не, майкрософтовский Lean https://leanprover.github.io/about/

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

>>4865187
А есть какие-нибудь книжки для тех, кто хорошо разбирается в программировании, но плохо разбирается в математике, чтоб в них описывалась математика языком компьютерных программ? Чтоб например вместо пикрилейтеда, числа фибоначчи описывались как-нибудь так
unsigned int fib(unsigned int n)
{

return (n == 0 || n == 1) ? 1 : fib(n - 1) + fib(n - 2);

}
или:
unsigned int numbers[10] = {1,1};
for (size_t i = 2; i < 10; ++i)
{

numbers[i] = numbers[i-1] + numbers[i-2];

}
Потому что многие программисты не понимаю весь этот математический синтаксис. Где вообще пожно про него почитать? Вот например кто-то пишет ab(b+c) и это надо понимать как a×b×(b+c), а когда мы пишем cos(x) то мы уже не понимаем это как c×o×s×(x) и даже не понимаем это как некую cos×(x). А когда проходят интегралы ∫x²dx (в TeX это будет \int_{}^{}{x^2}dx ) то вообще неясно, можно подумать что мы берем интеграл от некоторого выражения "x²×d×x" хотя на самом-то деле dx это элемент интегрирования. Почему так запутано?

>>4863840
Алло, а как юзать тригоном формулы в комплексных, без тригонома?

>>4863878

>о том, как что-то конкретное закодировать и вопросы типа "можно ли придумать какой-то ещё синтаксис, чтобы кодировать стало ещё удобнее" мне кажется всё же больше по части CS

А разве cs не о алгоритмах и структурах данных, есле да, то при чем тут кодирование

>>4865218
Первый раз такой странный реквест слышу, синтаксис абузят в целях удобночитаемости. В твоём примере с интегралом мы и так берём интеграл от выражения (диф.формы) x^2 × d(x), диф.формы и функции ведут себя существенно разным образом при замене переменных, поэтому приписка dx тут существенна.

Единственное что по сути реквеста помню, была такая книжка Contemporary Abstract Algebra от Gallion (или как-то так автора звали, думаю найдешь), там было некоторое количество упражнений, делать которые нужно было на компьютере. Ещё на курсере был курс по лин.алу для программистов тоже почти весь на компьютере, но все объяснения всё равно делались в привычном для всех синтаксисе, думаю, тебе придётся к нему привыкнуть поверив в то, что как привыкнешь - станут очевидны его профиты.
>>4865223
Не понял о чём ты!
>>4865228
Думаю, что есть CS об алгоритмах и структурах данных, а есть CS о кодировании мат.доказательств в термы какого-то синтаксиса, а есть CS о чём-то ещё - наверняка!

>>4865230
Как ты собираешься считать геометрию в комплексных без тригонома?

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

>>4865218
Лучше предложи сразу всю математику на Лисп заменить.

>>4865218
Часто всё-таки cos пишут другим шрифтом, чтобы было понятно, что это один токен.

>>4865218
Лучше бы постыдился такой код показывать!

>>4865235
Зачем ограничиваться математикой? Все инструкции писать кодом.

>>4865218

>Потому что многие программисты не понимаю весь этот математический синтаксис

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

>Где вообще пожно про него почитать?

В школьных учебниках по математике. Ты как с луны свалился.

>>4865237

>Часто всё-таки cos пишут другим шрифтом, чтобы было понятно, что это один токен.

Хорошо, что мне ни в языках программирования не приходится писать cos другим шрифтом, чтобы было ясно, что это не c×o×s а именно функция cos
>>4865277

>Программисты прекрасно понимают весь этот синтаксис, поскольку кончали и старшую школу и университет, не надо тут наговаривать.

Есть те, которые не понимают.
Язык математики, в отличии от языка программирования, допускает неоднозначность интерпретации написанного на нем. Вот я приводил простой пример с косинусом. Если мне надо записать выражение "косинус от a плюс b" то я напишу cos(a+b) и всё будет понято правильно, а если мне надо написать "c умножить на o умножить на s и умножить на выражение a плюс b" то я не могу это записать как cos(a+b) потому что меня могут неправильно понять, и мне надо записывать cos другим шрифтом или придется записывать как-нибудь по-другому, явно обозначая умножения т.е. c×o×s×(a+b). В языках программирования не возникает подобных неприятных неоднозначностей, там не надо что-то писать другими шрифтами, чтобы мою запись можно было правильно проинтерпретировать.

>В школьных учебниках по математике. Ты как с луны свалился.

Я не помню чтоб в учебниках математики учили, что чтоб было понятно, что последовательность латинских букв "cos" это именно косинус, то надо записывать это каким-то особым шрифтом в тетрадке, там видимо просто расчитывают на то, что у тебя переменные не будут называться c o s и ты не будешь их перемножение записывать как "cos". Там вообще нет формального определения синтаксиса и семантики математических выражений и точного, однозначного способа интерпретировать их!

>>4865294
Эту проблему с неоднозначностью можно было бы решить, если б математики все внезапно договорились бы, что теперь давайте писать cos(x) как {cos}(x), log(x) как {log}(x) и так далее, и тогда было бы понятно, что выражение в {} скобках это название функции, которую применяем к выражению в () скобках, но вот по-моему такого никогда не произойдет.

>>4865294

>Есть те, которые не понимают.

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

>Язык математики, в отличии от языка программирования, допускает неоднозначность интерпретации написанного на нем.

Что ты несешь?! Дальще даже и читать не буду.

>>4865294

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

Что такое undefined behavior?

>>4865296

>Что ты несешь?! Дальще даже и читать не буду.

А что не так? Каким образом мне понять, что если кто-то на бумажке рукой написал выражение cos(x+y), то cos это именно косинус, а не c умножить на o умножить на s?

>>4865298

1. Есть языки, в которых UB нет
2. Если UB все же есть, то ситуации с UB определены в стандарте соответствующего языка. Где мне почитать официальный стандарт на язык математики?

>>4865299
Таким же образом, как и все остальные надписи -- из контекста.
Ты решил покормиться на тупости?

>>4865300

Попробуй взглянуть на своё существование более философски: отвлечься от истинности/ложности или важности/неважности своего мнения и задуматься, что вообще происходит. Человек, видящий перед собой только математические закорючки, при виде человеческого языка превратится в формалиста (ведь там нет закорючек, которые он видит 99% времени; видящий идеи за закорючками может не превратиться). В этом поколении уже программисты пытаются "взгромоздиться" на математиков: прямо N десятков минут назад видел, как кто-то заметил что в математике ещё и не должно быть "неопределяемых понятий", а должно быть всё как в программировании. Суть в том что это не процесс мышления, а процесс подобный схождению оползней грязи после дождя. Перекладывание слов изо рта в рот, где участники не субъекты а объекты процесса

(Хотя ты вроде просто спросил что-то, но тогда сам виноват что начал говорить так будто что-то утверждаешь)

>>4865300
Ну то есть в реальности таки порядочно ситуаций где написано так, а что выполнится зависит от компилятора, системы или вообще рандома.

>>4865300

>Где мне почитать официальный стандарт на язык математики?

Попробуй с Бурбаки начать.

Вверх!

>>4865421

Сегодня снова не сплю, походу

Какие есть полностью асимметричные выпуклые правильносторонние четырехмерные многоячеечники?

>>4865526
А что значит "полностью асимметричный"? Просто группа симметрий тривиальна (как у множества) или что-то посильнее? Я думал что все правильносторонние политопы ещё в начале XX века классифицировали.

>>4865537
Ну в трехмерном случае это будут многогранники Джонсона. И среди них нету такого чтобы группа симметрий была тривиальна, хоть какое-нибудь отражение или поворот найдётся. Не совсем очевидно почему, но так получилось.
А вот если обобщить на четырехмерные многогранники с правильными сторонами, то найдётся ли асимметричный? Там вариантов сильно больше, поэтому почему бы нет?

>>4865546
Осталось их всех перерисовать в анимешных девочек. Наращенных и усеченных!

>>4865543
http://mathieudutour.altervista.org/Regular/index.html так вот классификация всех правильносторонних политопов во всех размерностях нужно аккуратно чекать, но вроде 0_21+Pyr(октаэдр) удовлетворяет твоему реквесту, так как 0_21 не имеет осевых симметрий, а после того как мы одну из граней видоизменили, то каких-то других симметрий, которые меняют грани местами остаться не должно. Там же z-структура выписана полностью - сядь да посчитай группу симметрий, что мешает!

>>4865554
Интересно, спасибо за наводку. Вообще это получается аналогично полностью усеченному пятиячеечнику у которого одна октаэдральная грань остается на месте. Сейчас прикину, можно ли ее вертеть на месте не мешая остальному.

>>4865613
Режим сбит и работать надо.
Никак, это открытая проблема, такое свойство (ну, почти такое) называется "нормальность числа в десятичной системе", на сегодняшний момент нету никаких подходов доказывать нормальность каких-нибудь не искуственно придуманных чисел, насколько мне известно.

>>4865620
А в чем заключается твоя работа как математика? Ты доказываешь какие-то теоремы, или выводишь какие-то свойства, или что?

>>4865637
Доказываю какие-то теоремы и вывожу какие-то свойства.

>>4865643
Ну а можешь поподробнее объяснить, что означает быть математиком? Надо регулярно какие-то научные журналы по математике читать, читать какие-то чужие бумаги, писать и отправлять свои бумаги на проверку, и кто-то потом говорит что у тебя вот там и там ошибка, и ты потом это исправляешь? Или как это всё происходит примерно?

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

>>4865657
А если кто-то занимается математикой на любительском уровне и у него нет никаких научных руководителей, но он совершил (или думает что совершил) какое-то серьезное математическое открытие, например доказал гипотезу Римана, то куда ему лучше всего обращаться? В https://arxiv.org/ ?

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

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

Проснулся - можно и дальше в треде сидеть.

>>4865311

>Попробуй с Бурбаки начать.

>An extreme example is Bourbaki’s language for set theory, which requires 4,523,659,424,929 symbols plus 1,179,618,517,981 disambiguatory links (lines connecting symbol pairs,usually drawn below or above the formula) to express the number “one”

Не, спасибо

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

>>4865307

>Таким же образом, как и все остальные надписи -- из контекста.

В языках программирования контекст можно однозначно понять из кода.

>Ты решил покормиться на тупости?

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

>>4865298

>Что такое undefined behavior?

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

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

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

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

>>4865823

>Если кто-то не видит никакой проблемы с недостаточно четким определением математического синтаксиса и семантикой

В математике конечно есть известные проблемы, но это явно не "cos можно прочитать как c o s".

>>4865824

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

А с SMT решателями ты работал? Например есть SMT-решатель Z3 от майкрософта, которым можно доказать, что x != x * x для любых x не считая 0, 1
https://rise4fun.com/Z3/iMVP
Я еще читал, что выводимые там доказательства можно оттранслировать в Coq и проверить еще там. Или просто использовать это как оралкул.
https://yurichev.com/writings/SAT_SMT_by_example.pdf

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

>>4865826

>>4865884
Картинка смешная, а вот ситуация страшная?

Пойду приготовлю еду, а вы пока напишите чего-нибудь, негоже когда тред мёртвый!

>>4865620
А какие в последнее время были случаи что какой-то факт считался очевидным, но труднодоказуемым, а потом бах! и доказывали что верно как раз противоположное?

>>4863704
С чего начать изучение математики? Люблю физику, чтобы понять многие определения из физики нужно знать математику. Я вообще не понимаю где начало у математики, откуда начинать её изучать?

>>4865942
Неплохой вопрос! Вспомнилось несколько примеров, во-первых "комплексная гипотеза якобиана", о том, что если якобиан голоморфного отображение C^n->C^n в каждой точке не вырожден, то существует обратное голоморфное отображение, придумали контрпример, что поламало много доказательств, которые к тому моменту были (эта же гипотеза открыта, если ослабить условие голоморфности до регулярности в смысле Зарисского). Второй известный про гипотезу о групповых кольцах, что если G и H конечные, то ZG = ZH титтк G = H, доказали для многих частных случаев и сильно верили в общий, но потом (аспирант, кстати) нашёл контрпример. Ещё, мне кажется, долго верили в то, что проверка нету детерменированного полиномиального алгоритма проверки на простоту, но потом 3 индуса на какой-то мат.школе AKS-алгоритм придумали. Ещё верили, и, более того, было доказано, что на lim^1 = 0 на системах миттага-леффлера в 60х, и этим даже пользовались, а потому тоже контрпример нашли. Ну и нашли более эффективные примеры (структуры веари-фелмана) к задаче Кеплера о "наиболее эффективной мыльной пене", хотя интуитивно кажется, что конструкция самого Кеплера c биусечёнными кубами оптимальна.
>>4865947
Гельфанд Шень "Алгебра", khan academy, brilliant.org

>>4865952
Спасибо. С меня конечно же ничего.

>>4865954
От тебя ничего и не нужно!

Заснул случайно! Сейчас точно начну готовить!

Вопрос такой. В pdf-ке http://kpfu.ru/docs/F565128140/nasyrov_klein_but.pdf написано

> Поверхность называется неориентируемой, если она содержит в себе какой-то лист Мебиуса. В противном случае поверхность

называется ориентируемой.

> У ориентируемой поверхности есть две стороны, у неориентируемой - одна.

Так вот, если взять ленту из бумаги (это НЕ лист Мёбиуса, у него две поверхности), сделать из этой штуки фигуру вращения то на выходе получится уже поверхность (ну это как тор, в котором при разрезании на две части вместо "oo" будет "∞" т.е. бублик без дырки с самопересечением по центру, как в закрытом торе). Как эту поверхность описать, есть ли у нее название? Это известная штука вообще? Точка, в которой внешняя поверхность этого какбы тора переходит во внутреннюю там будет только одна - это центр закрытого тора. Гомеоморфно ли это бутылке Клейна?

Еще картинка для пояснения

>>4865681

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

https://www.theverge.com/2018/10/24/18019464/4chan-anon-anime-haruhi-math-mystery
A 4chan poster may have solved part of a very tricky math problem that mathematicians have been working on for at least 25 years. The user was just trying to figure out the most efficient way to watch episodes of a nonlinear anime series, but the result has generated considerable interest from mathematicians around the world who have no way to identify the anonymous user.

>>4866034
Это horn torus, это не гладкая поверхность (есть особенность в центре) для таких понятие (не)ориентируемости не рассматривают, ну или рассматривают но я не в курсе. Негомеоморфна бутылке клейна.
>>4866047
Во-первых не факт, что это был любитель, а во-вторых "найти более оптимальную перестановку которая удовлетворяет каким-то там свойствам" подходит под моё видение "примера в виде комбинаторной конфигурации". Неужто ты думаешь, что я не вспомнил эту историю когда писал тот свой пост?

>>4865952
Интересные примеры, спасибо! Некоторые весьма красивые и наглядные даже если в математике не очень разбираться.

>>4866055
Вот этот пример наверное хорошо подходит под "найти более оптимальную перестановку", но всё же: он насколько замечателен? Для непрофессионального математика круто?
https://www.quantamagazine.org/decades-old-graph-problem-yields-to-amateur-mathematician-20180417/

>>4866082
Для непрофессионального математика любое продвижение в любой открытой проблеме - это круто, но всё же мне кажется что конкретные комбинаторные конфигурации и примеры менее ценны, чем какие-то универсальные рассуждения.
>>4866079
Без проблем, если что ещё вспомню - скажу!

>>4866055

>Это horn torus, это не гладкая поверхность (есть особенность в центре) для таких понятие (не)ориентируемости не рассматривают

Я почитал про этот horn torus и не очень понял, что они там имеют ввиду. Если мы идем от наружной поверности такого тора к его центру, то мы так можем попасть наизнанку (на внутреннюю поверхность) такого тора? Может под этим horn torus понимают немного не то, что я имею ввиду?

>>4866105
Вот попробовал проиллюстрировать свой вопрос

>>4866105
Возможно я неправильно тебя понял, посмотри ещё klein eight figure возможно то, что ты ищешь.

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

>>4866171

>Возможно я неправильно тебя понял, посмотри ещё klein eight figure возможно то, что ты ищешь.

Нет, klein eight figure это не то. Я думаю что ты меня понял правильно, просто я не понимаю, почему нельзя четко определить то, куда мы попадем, если пройдем через эту особую точку (выйдем ли опять наружу этого "бублика с нулевой дыркой" или войдем внутрь)? Я не думаю что это прямо так сложно, указать свойства этой точки при прохождении через нее.

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

>>4866186
Кстати говоря, твоя конструкция с тем, чтобы рассмотреть такой путь на хорн торе, тем не менее, довольно остроумная, не могу не похвалить!

>>4866198
Вот тут такую картинку нашел
http://www.meru.org/Advisors/klein.html

>Note the double-cone at the Klein bottle's center:
>Any Klein bottle in 3-dimensional space must pass through itself somewhere. The Klein bottle comes in many topologically equivalent forms.

Вот эта вот прокрученная вокруг центра ∞ которую назвали "frisbee" - это и есть то, что я имел ввиду. И походу это просто еще один способ нарисовать бутылку Клейна.

>>4866226
Хорошо тогда

Бездарный день.

>>4866379
Это посольство Курисача? Что-то слишком прилипла ассоциация персонажа и борды, даже сильнее, чем Хоро<->Доброчан.

>>4866381
Нет, нужна была аниме-девочка связанная с математикой и я ничего лучше, чем Курису, не придумал.

>>4866383
А в каком вообще аниме есть математика?

>>4866461
Вроде бы ни в каком нету, ну или я не в курсе.

>>4866464
Надо было бы Сырну брать.
https://www.youtube.com/watch?v=5wFDWP5JwSM

Надо было, но уже взял кого взял.

>>4866490
Связывать девочек никогда не поздно.

>>4866488
Сырна на ычане это слишком банально.

>>4866504
Быть может в следующем треде, если мне это всё не надоест, тем более уникальные картинки с Курису искать всё сложнее, а писать какие-то скрипты которые бы меняли картинки старые или вручную ставить точку в пэинте - лень.

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

>>4866511
Кое-что знаю. Не, большая часть науки про узлы касается свойств всяких алгебраических и топологических инвариантов узлов (типа гомологий флоера, хованова и фундаментальной группы дополнения), а также гиперболических структур на дополнении к узлу. Вообще узлы - это такая игрушечная моделька в алг. топологии, на которой большая часть алг.топологической машинерии может быть протестирована, прежде чем переходить к каким-то более сложным случаям. Помнится даже кто-то из серьезных людей хотел написать книжку в духе "knots as toy model in alg.topology", но так и не написал. Вычислительная теория узлов связанная со всякими алгоритмами развязывания и завязывания есть, но там, вроде, пока что без сногсшибающих результатов, вроде ничего лучше чем алгоритма из класса co-NP нету. А, ещё Концевич свой интеграл придумал интегрируя какие-то бандлы по каким-то узлам, но про это я точно не в курсе деталей.

А, вот что ещё вспомнил, есть арифметическая топология и cловарь Мазура-Моришиты-Капранова-Резникова, про то что S^3 соответствует Spec(Z), простые числа - узлам, индекс зацепления - символу Лежандра, факт неимения нетривиальный неразветвлённых накрытий у S^3 транслируется в факт неимения нетривиальных алг.расширений у Z, квадраатичный закон взаимности Гаусса транслируется в аналогичный (но тривиальный) закон для зацеплений и тд и тд. Насколько я понимаю пока что какой-то серьезной причины такой сильной аналогии не найдено, но вот это действительно очень неожиданная и будоражащая фантазию штука, за которые я математику и люблю.

>>4866516
Неразветвлённых расширений нету, конечно, разветвлённых сколько угодно. как-будто кто-то проверять будет

Начал читать тред, а там "семантики", "смыслы", "проверяемость"... Философия больше чем математика. Это не яблоко.

>>4866686
Семантика действительно слегка метаматематический концепт, хоть с ним и можно в рамках математики работать, если закрывать глаза на кое-какие неудобства. А что философия больше - так и пускай, математике не нужно быть больше кого-то, чтобы я её любил!

>>4866696
Просто с философской точки зрения, ваш спор о доверии к компиляции очень просто разрешить.

1) Истины не существует, есть только "достаточно точные в контексте задачи" приближения. Тогда исчезает требование к этой самой стопоцентной доказуемости. И ничто тогда не запрещает мне какой-нибудь заковыристый интеграл взять в том же вольфраме, даже зная, что он неправильно считает интегралы.

2) Смысл связан с семантикой, а значит переход от одного языка к другому в корне меняет саму суть поставленной задачи. И когда мы доказываем что "гипотеза Римана верна", то мы можем сделать это только на русском языке. А "Riemann's hypothesis is correct" - это уже другая задача, решающаяся в других категориях. Пример не совсем контрастный, потому что человеческие языки (почти все) обладают эквивалентными категориальными базами, но суть, надеюсь, понятна. А все сопутствующие вычисления на других языках возможны тогда и только тогда, когда мы имеем четкий словарь: "это значит это, а то значит то". Если же мы не понимаем кусок кода, то ничего доказать с помощью него мы не можем.

3) Логическое соответствие в разных логиках разное, невозможно установить логическое соответствие в суждениях машины и человека, обезьяны и человека, а зачастую и человека и человека.

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

>>4866709

>Истины не существует, есть только "достаточно точные в контексте задачи" приближения.

Не согласен с этим утверждением. Типа кто-то скажет, что 1+1=2 а кто-то такой "ну неее, истины не существует, 1+1 это может не точно 2, а допустим 2.00001 или там 1.9999" - но это же бред, 1+1 точно равно 2 если мы таким-то конкретным образом понимаем выражение "1+1", истина у нас будет одна и только одна, без вариантов.

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

С этим тоже не согласен. Если я напишу "1+1=2" римскими цифрами "I+I=II" то никакой сути поставленной задачи не меняется.

>Логическое соответствие в разных логиках разное

Тут я вообще не понял. Что ты имеешь в виду?

>Итого: При переходе из семантики в семантику, мы меняем условия задачи, и от этого никуда не денешься.

Не согласен

>>4866714

>1+1=2

В каком контексте? Один математик плюс один студент равно полтора математика.

>I+I=II

Это не так считается. Возьмем менее тривиальный пример: 81*19 и LXXXI помножить на XIX. Все еще разницы не чувствуешь? Это почти все равно что написать "1" и "0,(9)". С точки зрения математики - одно и то же, а вот с точки зрения гносеологии совершенно разное. Хотя бы потому что получается из разных процессов. А машина вообще писать не умеет, только током биться.

>Логическое соответствие

Галилеева и Лагранджева механики, например. Минимальное отличие в логике приводит к максимальным отличиям в результатах. Причем нарушений логики нет ни там ни там. А на уровне, когда отличаются базовые концепции, все еще интереснее. Объясни от рождения слепому что "У Кафки рыжжие волосы - ложь", а "У Кафки черные волосы - истина". Потом то же самое объясни обезьяне.

>Не согласен

Посчитай сначала 81*19, а потом LXXXI помножить на XIX. Второе я не уверен, что сможешь, но все-таки.

>>4866721
Опять же, более красиво: 1+1=2+dx, где dx - бесконечно малая величина. Интегрируем по x, и внезапно не x+x=2x, а x+x=2x+x^2. И в случае комплексных чисел, совсем не обязательно x=0

>>4866733
где мои C, aaа?!

Ужасный день, но активности в треде рад!

>>4866709
Я прокомментирую, но если что я ни с кем не спорил и ни в чём никого убедить не пытался! Кому нравятся пруверы и у кого они повышают уверенность в чём-то - пусть пишут свои термы дальше, просто мне они не нравятся!

1) Сильное заявление, но его можно придерживаться если разогнать фантазию в достаточной степени (и так всякие \Pi_0^1-формалисты и делают), для меня вот арифметическая истинность уж точно существует, да и в теоретико-множественную истинность, вообще говоря, верю, для меня унивёрсум-фон-неймана объект той же сложности, что и стандартная модель натуральных чисел и оба объекта мне кажутся предельно ясными.
2) Ну примерно о том я и говорил, совсем не обязательно всё редуцировать до какого-то одного метаязыка, так как математики рассказывают историю в пределах одной статьи, значит, грубо, можно считать что в пределах каждой статьи свой маленький синтаксис и своя маленькая семантика. Иногда можно построить интерпретацию результатов из одной статьи в другую - иногда нет.
3) Да, конечно, примерно об этом я и говорил когда говорил, что пруверы не уменьшат количество ошибок, а просто перенесут ошибки на уровень "закодировано было не то, что заявлялось".
>>4866721
Uuggh, ну ты прямо \Delta_0-формалист, как-то недоверие к истине у тебя не из того источника идёт, из какого мне хотелось бы чтобы она шла. Хотелось бы, чтобы дело у тебя не сводилось к всяким штукам вроде приколов с квалиа, когда непонятно то ли человек имеет в виду под "1+1=2", что и ты, сколько бы вы детали контекста между собой не обсуждали (можно сказать, что это семантичесская формулировка теоремы гёделя). И уж точно не хотелось бы чтобы дело сводилось к "природу можно формализовать по разному", всё-таки следует как-то отличать арифметическую и теоретико-множественную истинность от хорошей мат.модели какого-то природного явления.
>>4866733
Идея понятно, но, FGJ, в комплексных верно x^2 = 0 -> x = 0, говори тогда уже "дуальные числа" или, ещё понтовее "неверно в любом кольце с нетривиальными нильпотентами".

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

Помните "Контакт" Карла Сагана? В котором в числе Пи в определённой системе счисления нашли подпись бога? Но ведь даже бог не может изменить число Пи. Если бог может думать, то он уже может вычислить число Пи, значит он не может создать его и оставить там что-то, так как оно уже есть.

Как так-то?

>>4866928

>и оно будет равно всегда одному и тому же

Искривления пространства при околосветовых скоростях и зависимость вообще почти всего от максимальной скорости света вроде говорит об обратном.

>>4866928
Сам диву даюсь что как-то так и выходит! Надеюсь когда-нибудь арифметика расщепится на \Sigma_0^1 уровне, чтобы этот мой невроз унять!
>>4866932
Думаю что он имел в виду то pi, которое через формулы Валли вычисляется, то есть имел в виду некоторую последовательность цифр которую выдаёт вполне конкретная программа, а не про измерения на околосветовых скоростях, в экзотических областях пространства-времени на первых наносекундах после большого взрыва и тд и тд!

>>4866928

>Но ведь даже бог не может изменить число Пи.

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

>>4866932
Кривизна кривизной, но Пи всё равно участвует во всём этом безобразии. И мы можем измерить кривизну с помощью, например, суммы углов треугольника, и потом из кривизны и нарисованной окружности посчитать Пи (если кривизна непостоянная, то будет сложнее, но это не важно). А затем сравнить с тем Пи, что посчитали на компьютере. И они внезапно будут равны. И мы не можем себе представить так, что не равны. Потому сама по себе геометрия абстрактна и применима к любому пространству, которое мы только можем придумать. И внезапно при этом имеет отношения с числами, которые можно взять и вычислить негеометрическим способом.
>>4866944

> \Sigma_0^1

Это вот это вот https://en.wikipedia.org/wiki/Arithmetical_hierarchy ? Можешь пояснить простыми словами? В частности, что именно ты имел в виду.

>>4867095
Круг — это в первую очередь хреновина, у которой точки равноудалены от другой точки. И ты можешь, конечно, манипулировать метрикой сколько угодно, но ты не можешь сделать так, чтобы при эвклидовой метрике (корень из x²+y²) соотношение длины окружности к диаметру не было равно Пи. В определении эвклидовой метрики никакого Пи при этом не было.
То есть даже если ты живёшь в пространстве с абсолютно упоротой метрикой и топологией ты всегда сможешь на компьютере запрограммировать эвклидову плоскость. И там будет Пи. У тебя никак не получится сделать так, чтобы не было.

>>4867097
Ну, да, но отношение длины окружности к радиусу в разных геометриях разное и может быть непостоянным. И в реальной жизни у нас, на секундочку, неЕвклидова геометрия.

>>4866928
Может тебя вообще глючит, а на самом деле дважды два - пять, и противоположное можно только в бреду представить?

>>4867105
Но только одно из них равно Пи. И у нас есть способ определить, какое.
>>4867108
Если глючит одного только меня, то я довольно быстро столкнусь с проблемами.

>>4867108
И даже если всех. То если на самом деле равно 5, то мы сможем понять это.

А вот придумать логически непротиворечивый мир, где и правда 5 (понятное дело, что мы не об именах цифр и не о системах счисления говорим, а об абстрактных понятиях), мы не можем.

>>4867113

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

Это, опять же, исходит из преположения что логика как и арифметика важнее и независимее ощущений. Однако вполне можно представить бред, в котором тебе будет казаться что 2х2=17 и обратное противоречит логике. Значит, может случиться и обратное - в бреду дважды два - четыре, а на самом деле - нечто другое.

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

А всё остальное уже будем из этого набора аксиом выводить. Разницы нет. Просто ты привык к тем базовым понятиям, которые справедливы для нашего мира. И других представить не можешь.

>>4867097
Ну про \Sigma_1 уровень я загнул - низковато всё же. Но чтобы было некоторое недоказуемое и неопровержимое арифметическое утверждение первого порядка (на языке L^1) такого сорта, в которое были бы резонные причины как верить, так и не верить, это бы действительно пошатнуло картинку того, что мы понимаем, что такое "стандартная модель натуральных чисел" (то есть натуральные числа as it is) На языке L^3 такое утверждение есть - континуум-гипотеза называется, но L^3 это слишком абстрактно, а вот если бы было расщепление на L^1 - то это действительно была бы ситуация, которую не стыдно было бы назвать постмодерном (sic!) и посягательством на арифметическую истинность. А пока не вижу причин не пользоваться "арифметической истинностью" как вменяемым концептом.

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

>>4867122
Ты не мог бы понятным для простого обывателя языком объяснить, что означают все эти сигма-уровни и языки L^1 L^2 и так далее?

>>4867166
L1,L2,L3 языки логик первого, второго и третьего порядка, в контексте арифметики позволяют делать утверждения о натуральных числах, множествах натуральных чисел и множествах множеств натуральных чисел соответственно. Завтра напишу про арифметическую иерархию, устал очень сейчас. Если коротко: это некоторая классификация утверждений о натуральных числах по уровню абстрактности, на самом нижнем \Delta_0-уровне находятся утверждения которые требуют конечного (хоть иногда и очень большого) числа синтаксических преобразований для проверки их истинности (вроде 2+2=4, в шахматах всегда будет ничья, и тд итд)

>>4867185

> в шахматах всегда будет ничья

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

>>4867189
Ого, я только что взял и доказал. Видимо, в постели под одеялком думается намного лучше.

>>4867189
>>4867190
Это открытая проблема, но тут это не важно, а важно то, что она сводима к конечному перебору.

Косинус
Синус
Глобус
Анус

Школа - отстой

>>4867185

>L1,L2,L3 языки логик первого, второго и третьего порядка, в контексте арифметики позволяют делать утверждения о натуральных числах, множествах натуральных чисел и множествах множеств натуральных чисел соответственно.

Я кажется понял что тут имеется ввиду, правда это было сделано нестандартным способом (я вообще программист). Есть CS такая доказано нерешаемая проблема - проблема останова. Доказательство можно найти много где, можно почитать про доказательство через Канторов диагональный процесс тут https://web.archive.org/web/20170215130846/https://inf.1september.ru/2000/5/art/turing.htm (мне оно сильнее нравится, чем через рекурсию, но не суть). Взять например Великую Теорему Ферма (которую уже доказали). Если б существовал некий физический принцип, на основе которого можно было б дать заключение, завершается ли некая компьютерная программа на брейнфаке, то прибор, работающий на этом физическом принципе, мог бы легко доказать для теоремы Ферма, что она верна. Т.е. мы б просто закодировали на брейнфаке компьютерную программу, которая просто перебирает все счетное бесконечное множество чисел, удовлетворяющих условию, пытаясь найти решение, и спросили бы у прибора "зависает ли наш перебор теоремы Ферма?" - и на основе ответа мы б сделали соответствующее заключение. Проблему останова для машины Тьюринга можно решать через https://ru.wikipedia.org/wiki/Машина_Зенона если б ее можно было сконструировать. Т.е. будь у нас эта машина Зенона, то она за конечное время перебрала б все счетно-бесконечные варианты теоремы Ферма и загорелась бы лампочка "ЗАВИСАНИЕ".
Теперь давайте рассмотрим https://ru.wikipedia.org/wiki/Теорема_Гудстейна
Тут уже так не выйдет! У нас есть счетное бесконечное множество целых положительных чисел, и нам надо для него доказать, что некоторое преобразование для каждого такого числа всегда завершается чем-то там за конечное число шагов. Это тут просто неформулируемо, я не нашел способа это записать в терминах зависаемости одной конкретной МТ, тут нужен иной подход, тут нужно запустить счетно-бесконечное множество компьютерных программ на брейнфаке и проверить, что все из них всегда завершимы за конечное число шагов. Т.е. если у нас есть волшебный процессор с бесконечным числом волшебных процессорных ядер, каждое из которых за конечное время может решить проблему останова для МТ (как машина Зенона), то вот на такой штуковине эта проблема может быть решена - мы одновременно для каджого из ядер даем по одному из чисел, запускаем там эту проверку теоремы Гудстейна, и потом смотрим на бесконечный ответ от всех ядер - если хоть один из ответов будет "ЗАВИСАЕТ!" то теорема Гудстейна будет опровергнута. Теорема Гудстейна доказывается в арифметике второго порядка - это видимо и есть то, что имеется ввиду под L2. В общем между этими языками логик и способом перебора есть прямое соответствие

А чем арифметика Пеано лучше или хуже арифметики Пресбургера?

>>4867706
Это разрешимая теория, а значит - слабая, а значит почти ничего на ней сформулировать нельзя (например, нельзя выразить предикат "х - простое число").
>>4867654
Понял почти правильно, теорема гудстейна это Pi_2^0 утверждение на L1 языке а именно утверждение уровня "для любого n существует такое k т.ч. "k-ый член последовательности гудстейна начатой с n будет равен 0"

>>4867293
Бака, я не про конкретно шахматы, а про любую игру, где два игрока могут менять текущую позицию по очереди по определенным правилам и рано или поздно можно придти к позиции, считающейся выигрышем (или проигрышем) (а ещё ничьей!) для того, кто ее получил!

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

>>4867875
Да, конечно, неправильно прочитал твоё сообщение, думал ты спрашиваешь о ничейности шахмат.

>>4867875
по определенным правилам, зависящим только от текущей позиции и, быть может, от предыдущих сделанных ходов

Так, наверное, будет точнее.

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

>>4867882
Да лучше сразу определять "комбинаторную игру для двух игроков с полной информацией" как следующую: есть орграф G со стартовой (отмеченной вершиной) s на которую ставится фишка, игроки ходят по очереди и за ход должны двинуть это фишку вдоль ребра, кто не может сделать ход - проиграл, а всякие шахматы-шашки-хексы-нимы-крестикинолики уже сводить к игре такого рода, как это и стандартно делается во всяких штуках типа теории Шпрага-Гранди.

Как продвигается решение задачи о передвижении дивана? Вообще она сложная потому что ей не занимаются или потому что она сводится к каким-то плохо поддающимся исследованию областям математики? Ну и ещё, для каких-нибудь похожих задач нашлись 100% доказанные оптимумы?

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

>>4867888
Не совсем. При таком определении оба игрока в случае попадания в одну и туже вершину имеют доступ к одним и тем же ходам, в то время как в тех же шахматах доступные ходы у каждого игрока -- свои.

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

>>4867917
Значит, что граф шахматных состояний устроен таким образом, что второй игрок никогда не попадёт фишкой в вершины, которые соответствуют ходам белых фигур, а первых не попадёт в вершины которым соответствуют ходы черных фигур. В случае шахмат граф понятно как устроен: вершинам соответствуют состояния доски + очерёдность хода (+ можно пару битов выделить на то, была ли рокировка и какие-то такие тонкости), а стрелкам, соответственно, допустимые ходы.

Есть настроение посидеть ночью, потому - пишите.

>>4867185

>Завтра напишу про арифметическую иерархию, устал очень сейчас.

Напиши. Или подскажи, где это можно почитать?

>>4867908
Ясно, спасибо. Вообще может быть если хитро подобрать форму коридора, то можно будет свести эту задачу к каким-нибудь совсем непохожим.

>>4868171
А, забыл совсем, ну как я и говорил это классификация утверждений по уровню абстрактности. На Delta_0 уровне утверждения в духе "2+2=4", "2^2^37+1 - простое число" и прочие в некотором смысле конечные утверждения, если проводить аналогию с естествознанием, то в соответствие Pi_0 утверждениям можно поставить конкретные события типа "7 марта в 13:00 солнце находилось в точке (13,27) небесной сферы", если с программированием, то Pi_0 уровню соответствуют программы без циклов (или с ограниченными цыклами, но концептуально это не суть).

Pi_1 утверждения - это уже утверждения вида "Для любого x.P(X)" где P(X) - это Pi_0 утверждение, например что не существует нечётных совершенных чисел (для любого x. x нечётное -> x не совершенное) более того RH тоже Pi_1 хотя доказать это и нетривиально, если проводить аналогию с естествознанием, то этому будут соответствовать "однопараметрические универсальные утверждения" в духе "солнце в момент времени t находится в месте f(t)".

Pi_2 уровень это уже "для любого х существует у . P(x,y)" упомянутая тобою теорема гудстейна - хороший пример, ещё один пример - гипотеза коллатца, используя аналогию с естествознанием дальше можно наверное сказать что этому соответствует что-то в духе "у любого тела малой массы в солнечной системе существует эллиптическая орбита".

Ну и тд, Pi_3 это "для любого х существует у для любого z" Pi_n это n раз альтерировать кванторы и начать с "для любого" Sigma_n тоже самое но начать с "существует".

Там есть ещё аналогии с вычислимостью, борелевской/проективной иерархией, множествами натуральных чисел и множествами точек в пространствах Бэра или Кантора, но всё расписывать - это умереть можно. Где об это прочитать (кроме статей на вики) - даже не знаю, это всё используют обычно чтобы называть какие-то вещи и рассказывать какие-то истории, а не как предмет исследования сам по себе. Лично я об этом отдельно никогда не узнавал, узнавал из вступлений ко всяким докладам, но если вспомню какой-то хороший источник для начинающих - то скажу.

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

ОП, а ты умеешь исследовать рекуррентные формулы?
вот есть такая рекуррентная формула
f1(0) = 1
f1(1) = 1
f1(n) = abs(f(n-1)-n)/f(n-2)

Если построить график, получается четыре каких-то синуса, которые вертятся вокруг почти что sqrt(x)
А если определить такую вот рекуррентную формулу
f2(0) = 1
f2(1) = 1
f2(n) = abs(f(n-2)-n)/f(n-1)
То получается как раз этот "почти что sqrt(x)" вокруг которого крутятся эти четыре синуса.

Как можно понять, почему вторая рекуррентная формула f2 так близка к квадратному корню? И почему там именно 4 синуса в первой формуле, а не 8 например? Как быстро меняется период и амплитуда этих синусов? Где прочитать про математический аппарат, который это позволяет делать?

>>4868214

>Где прочитать про математический аппарат, который это позволяет делать?

Про производную почитай.

>>4868215
Я знаю про производные, но что мне эти производные дадут? Я через производную смогу понять, почему там синусов ровно 4 на графике?

>>4868216
Не умею но попробую!

Бампну.

>>4868378
Ну я посмотрел спектрограмму для отдельного "синуса" (можно каждую четвертую точку брать из последовательности) и получается что этот "синус" состоит из трех синусов... В общем сложная какая-то штука

>>4868748
Да рекуррентности с модулем и прочими if/else очень неприятно анализировать, может на досуге погуглю есть ли нечто похожее, но что заметил такую закономерность - молодец конечно!

>>4868955
А можешь привести примеры каких-нибудь решаемых тобою по работе задач, понятных для нематематиков? Ну чтоб сама задача имела относительно простую формулировку, доступную для понимания неспециалистам

>>4869234

>А можешь привести примеры каких-нибудь решаемых тобою по работе задач

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

Я "Кант-кун". Можно тут задать вопрос? Хотя я даже не знаю, какой. Я придумал способ классификации "текстур" объектов. Строго могу сказать только то, что чем-то способ похож на это:
https://en.wikipedia.org/wiki/Viola–Jones_object_detection_framework
И что у этих текстур ещё должны быть какие-то "топологические" свойства

>>4869261
Запили прототип.

>>4863734
дискретная

>>4869234
Нету таких, наверное, чисто в теории многие мои задачи сводимы к решению счётной системы полиномиальных уравнений c коэффициентами в С, но это сведение настолько бесполезное и настолько отдаляет от сути задачи, что наверное его лучше было бы даже не упомянать.
>>4869261
Можно, задавай, как придумаешь! Что придумал - то молодец конечно!

В математике есть просто числа (размерность 1) комплексные числа(когда есть Re и Im т.е. фактически две характеристики), есть кватерионы (1 i j k - 4 параметра), октонионы (8) и сенедионы (16) и думаю можно дальше сделать с 32 64... почему именно степени двойки (1 2 4 8 16), бывают ли какие-нибудь другие гиперкомплексные числа, где число параметров не степень двойки?

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

>>4869287

>Некоммутативны

Фикс. Хотя необщительные числа - тоже идея.

>>4869285

>и думаю можно дальше сделать с 32 64...

Да, это процедура Кэли-Диксона.

>почему именно степени двойки (1 2 4 8 16) бывают ли какие-нибудь другие гиперкомплексные числа, где число параметров не степень двойки?

Вообще "гиперкомплекные числа" это не очень точный термин, и скорее больше для рассказов школьникам используется. Если под этим словом понимать алгебры Клиффорда, то там выходит это примерно по такой причине что если у тебя e_1,...,e_n это некоторые новые символы, которые ты добавляешь к R чтобы получить алгебру (как ты добавляешь i к R чтобы получить комплексные или i,j,k к R чтобы получить кватернионы), то e_i1 e_i2 ... e_ik c i1<...<ik тоже должны быть частью твоей алгебры и мы получаем \sum_{k=0}^n C_n^k = 2^n. Если не понял, то короткий ответ: по построению. Но если тебя вообще любые R-алгебры инересуют (пусть даже слабо похожие на комплексные числа, а потому к ним слово "гиперкомплексные" не очень хорошо применять), то соордуить трёхмерную несложная задача, скажем прямая сумма трёх R такой будет.

>>4869287

>Так-то есть векторы и матрицы, в них вообще сколько угодно элементов, но свои свойства.

Ну а в чем особенность всех этих гиперкомплексных чисел, почему там надо чтоб число элементов было как степень двойки?

>>4869291
Если особых свойств не требовать, то не обязательно степень двойки, можно сколько угодно элементов брать. А если налагать ряд ограничений, то для одного будут только целые и комплексные, для другого кватернионы добавятся, а если ещё ослаблять то и другие системы. Почему? Ну такая структура реальности, можешь посмотреть например
https://ru.wikipedia.org/wiki/Теорема_Фробениуса

>>4869293П

>Почему? Ну такая структура реальности

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

>>4869299
Ну ты можешь вообще принять 2*2=5 за истину. Проблема в том, что из этого потом можно вывести вообще любое равенство, истинное и ложное. Такая структура будет очень богатой на возможности, но малополезной практически.

>>4869299

>Натуральные числа используются для обозначения количества чего-то (у меня 3 ореха, меняю их на одно яблоко).

Вот тут уже проблемы. У тебя нет трёх орехов, у тебя есть орех, орех и орех. То, что их можно свести в три ореха уже абстракция. Конечно попроще и попонятнее октонионов, но идея та же.

>>4869293
Только "вещественные" вместо "целые"! Эта теорема это более-менее про то, что только S^1 S^3 и S^7 параллелизуемы, а что остальные не параллелизуемы - это вычисление полного класса Штиффеля-Уитни + вещественная периодичность Ботта, ну короче да, простыми словами не объяснишь, так как причина глубокая так-то.
>>4869299
Ты мои ответы специально игнорируешь? Я ведь стараюсь! Я ведь сказал, что если брать то (неоправдано широкое) определение гиперкомплексных, что в википедии - то "гиперкомплексные" будут в любых размерностях, а если брать какое-то более-менее вменяемое, то будет просто по построению. Ну типа "гиперкомплексные - это те которые мы получаем такой-то процедурой, а такой-то процедурой мы получаем только 2^n потому что вот так вот устроена процедура", то есть тавтология по сути.

>>4869305

>Только "вещественные" вместо "целые"!

Да, что-то затупил, спасибо за фикс.

>>4869305

>Ну типа "гиперкомплексные - это те которые мы получаем такой-то процедурой, а такой-то процедурой мы получаем только 2^n потому что вот так вот устроена процедура", то есть тавтология по сути.

ОК, понял. Есть процедура построения каких-то там алгебр, и вот поэтому там 2 4 8... А чем хороши числа, которые по такой процедуре были синтезированы? Ну вот есть просто комплексные числа, sqrt(-1)=i, ок, хорошо, допустим. Что полезного в более "расширенных" алгебрах, получаемых по этой процедуре Кели-Диксона? Описать ведь можно еще много всяких разных алгебр и понапридумывать всяких других операторов, например перемножения матриц и проч.

>>4869307
Кватернионы например весьма полезны если ты хочешь писать трехмерный движок. Неплохо упрощают математику.

А есть ли алгебра над бесконечными битовыми векторами?
Ну, грубо говоря, цифр у нас только два: 0, 1, и работает это примерно как двоичная позиционная система счисления, но их может быть бесконечность. Например вот соответствие:
0 это - {0, 0, 0, 0, 0, 0, ...}
1 это - {1, 0, 0, 0, 0, 0, ...}
2 это - {0, 1, 0, 0, 0, 0, ...}
3 это - {1, 1, 0, 0, 0, 0, ...}
-1 это - {1, 1, 1, 1, 1, 1, ...}
-2 это - {0, 1, 1, 1, 1, 1, ...}
-3 это - {1, 0, 1, 1, 1, 1, ...}
И чтоб были какие-то непонятные периодические штуки, вида
{1, 0, 1, 0, 1, 0, 1, 0 (и дак далее повторять 1 0 бесконечное число раз)}
которые вообще никакому числу не соответствуют, но с которыми определены операции
{1, 0, 1, 0, 1, 0, 1, 0 ...} + {0, 1, 0, 1, 0, 1, 0, 1 ...} = {1, 1, 1, 1, 1, 1, ...} = -1
в результате которых получаем обычное число "-1"
Что-то такое математики описывали в своих теориях?

>>4869311
Не совсем то, но можешь p-адичные числа глянуть.

>>4869307
Хороший вопрос, по правде говоря не знаю чем они так выделяются среди всех flexible и степенно-ассоциативных R-алгебр. Но вот, как уже было упомянуто первые четыре члена выделяются тем, что это единственные альтернативные алгебры с делением, по теореме Фробениуса. Спрошу твой вопрос у людей поумнее чуть позже, может они что-то скажут.
>>4869311
Да, это в точности 2-адические.

>>4869313
Целые 2-адические, если быть точнее.

>>4869432
но ведь если записать в этих целых 2-адических такую периодическую последовательность:
{1, 0, 1, 0, 1, 0...}
то никакому целому числу это не соответствует, это вообще непонятно что будет. Арифметика Пеано такое не описывает, можно это представить в виде суммы степеней двойки, 2^0 + 2^2 + 2^4 + 2^6... но это будет просто бесконечность. Да и неясно вообще, положительное это число или нет, если отрицательные числа кодируются бесконечным хвостом из единиц, а тут хвоста никакого и нет!
Но если это интерпретировать как число между от 0 до 1 включительно, то тогда это приобретает какой-то смысл

{1, 1, 1, 1, 1, 1, 1, 1... } это будет:
\sum_{n=1}^{\infty} \frac{1}{2^{n}} = 1

ну а чтоб {1, 0, 1, 0, 1, 0...} надо сделать

\sum_{n=1}^{\infty} \frac{((-1)^{n+1}+1)/2}{2^{n}} = 0.66666...

эта штука ((-1)^{n+1}+1)/2 нужна чтоб то 1 то 0 было в числителе.
А эти 2-адические числа допускают вообще апериодическую запись, типа
101001000100001000001...
когда количество нулей между единицами постоянно увеличивается на 1? Или там по задумке разрешены только периодические записи?

>>4869477
Арифметика Пеано не обязана описывать 2-адические числа, она придумана чтобы описывать натуральные числа (ну или, по крайней мере, нечто, что похоже на натуральные числа). Чтобы последовательность 2^0 + 2^2 + ... сходилась к числу инверсная битовая запись которого выглядит как 101010... нужно переопределить "сходимость" в 2-адическом смысле, и ты даже понял как: сперва определим модуль (норму) 2-адического числа следу если на i-ом месте у числа стоит бит, то нужно считать что это добавляет 1/2^i в модуль, таким образом действительно |1111...| = 1 и |1010...|=2/3 таким образом по этой норме мы будем иметь как раз \sum_n 2^2n = 10101010... как мы того и ожидали. Норма любого 2-адического числа, как ты заметил, действительно лежит на отрезке [0..1], но на 2-адических числах невозможно придумать линейного порядка так, чтобы он был согласован с умножением и сложением, поэтому говорить что "это число между 0 и 1" некорректно. Не обязательно переодические, разрешены любые последовательности. Довольно круто что ты до такой абстрактной конструкции сам додумался, на самом деле, не могу не похвалить!

>>4869280

> Можно, задавай, как придумаешь!

Задам тогда общий вопрос, по теме. Есть ли ещё примеры подобного?:

3Blue1Brown, "The hardest problem on the hardest test"
https://www.youtube.com/watch?v=OkmNXy7er84

Что-то типа "самоулучшения" доказательства по ходу решения, можно сравнить два в чём-то похожих решения

> Что придумал - то молодец конечно!

Тебя точно не интересует классификация, например, лиц? Шахматных поз? Это что-то типа "практической топологии":

Просто вместо "дырок" фокусируешься на любой какой-то паре свойств объекта (свойств в выбранных областях; и области как-то связаны). Например, замечаешь что где-то объект вытянут, а где-то закруглён (как, например, кружка (циллиндр) или Джейк the Dog)(иллюстрации есть в моём треде, и их ещё появится)

Если нет, то не буду больше мешать треду
>>4869269

> Запили прототип.

Так это метод и для людей тоже. (всё, не мешаю, на сторонние сообщения не отвечаю)

>>4869650
Я, если честно, не понял где там "самоулучшение доказательства", там доказательство, по-моему, весьма одноходовое: придумать естественное действие Z_2 х Z_2 на конфигурационном пространстве троек точек так, чтобы в каждой орбите этого действия оказалась ровно одна нужная. Энивей красивых и остроумных доказательств в математике много! На похожей идее (подействовать группой на конфигурационное пространство комбинаторных объектов и выбрать по-умному что-то из орбит), скажем, построен подсчёт всяких штук при помощи леммы Бёрнсайда теоремы Пойя, скажем, задача об Ожерельях, только там действие группы чуть более нетривиальное и требует чуть более тонкого анализа. Если опишешь реквест как-то подробнее - я постараюсь вспомнить задач по больше.

Я же без иронии хвалил! Меня мало что интересует в математике (а в жизни - ещё меньше), но этот тред я создавал не для того, чтобы писать о том, что меня интересует, а чтобы вести изи-толки по-поводу того, что интересует других, так что можешь смело писать - буду только рад! Но то что ты описываешь, честно говоря, звучит как обычный перцептрон (даже не мультилеер), там ведь тоже каждый нейрон отвечает за какой-то "топологический признак". Чем тебе не нравятся перцептроны?

>>4869704

> Если опишешь реквест как-то подробнее - я постараюсь вспомнить задач по больше.

Прости, я из этого всего знаю разве что видео о "Necklace problem" (того же автора). А ты получается согласен со сведением работы человеческого ума к математическому формализму?

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

> так что можешь смело писать - буду только рад! Но то что ты описываешь, честно говоря, звучит как обычный перцептрон (даже не мультилеер), там ведь тоже каждый нейрон отвечает за какой-то "топологический признак". Чем тебе не нравятся перцептроны?

Мне и писать больше нечего. Не знаю, как работают перцептроны и другие сети, просто видел объяснение 3Blue1Brown (и Computerphile) и из-за этих видео и общего знания подумал:
1) Никто не парится, что должна делать сеть на высшем уровне абстракции. В частности, "feature construction" является проблемой судя по статье на вики (https://en.wikipedia.org/wiki/Feature_(machine_learning)#Selection_and_extraction)
2) Идея, которую описал, требовала бы веру в возможность классификации лиц (и прочего)/веру в существование этих "текстур"... Эта идея требовала бы придерживаться определённых идей о том как работает мышление в конце концов
3) Создалось впечатление, что у сетей вообще нет никаких глобальных стратегий работы
4) Другие проблемы (переобучение/проблемы с переносом знания) косвенно указывают на то, что сети так не работают. И в общем люди вроде говорят только о формализме на низшем уровне, не о том что могло бы помочь и другим людям тоже

Если это существует, это должно быть описано как общий метод, причём тут конкретная модель?