Формализация математических текстов

[Sycamore]

Alexandr Gavrichenko в сообщении #1482539 писал(а):

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

... угу, тем паче правильно их толковать/интерпретировать интуитивно

[Alexandr Gavrichenko]

Sycamore в сообщении #1482570 писал(а):

формализация нужна компу

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

Sycamore в сообщении #1482570 писал(а):

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

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

[Sycamore]

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

Alexandr Gavrichenko в сообщении #1482672 писал(а):

Запись на естественном языке может быть неправильно понята

(не)пониманию ничем не помочь

[Cuprum2020]

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

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

[Sycamore]

приходится напомнить:

Sycamore в сообщении #1482717 писал(а):

(не)пониманию ничем не помочь

[Alexandr Gavrichenko]

Alexandr Gavrichenko в сообщении #1476790 писал(а):

Класс колец можно обозначить $RNG$, класс групп - $GRP$, класс коммутативных объектов - $COM$.
Тогда класс абелевых (коммутативных) групп можно обозначить $COM.GRP$, а запись $g \in G \in COM.GRP$ будет расшифровываться как "$g$ является элементом абелевой группы $G$".

В основной идее (перед аббревиатурой множества приписывать аббревиатуру свойства (коммутативность, максимальность), сужающего множество) принципиально нет ничего нового.
Аналогичный подход к обозначениям я встретил в книге С. И. Адяна "Проблема Бернсайда и тождества в группах" (1975 г.):

Прав $(\alpha, X)$ - множество всех правильных вхождений ранга $\alpha$ в слово $X$

ВпПрав $(\alpha - 1, X)$ - множество всех вполне правильных вхождений ранга $\alpha - 1$ в слово $X$

Норм $(\alpha, Z, r)$ - множество всех нормированных вхождений элементарных $r$-степеней ранга $\alpha$ в слово $Z$

МаксНорм $(\alpha, Z, r)$ - множество всех максимальных нормированных вхождений элементарных $r$-степеней ранга $\alpha$ в слово $Z$

Таким образом, предлагающийся мной метод применялся ещё до моего рождения.

[Alexandr Gavrichenko]

Исправленная версия заметки в виде pdf-файла:
https://drive.google.com/file/d/1TuzXeX ... sp=sharing

[sugarySalt7]

Тема старая, но раз уж она хорошо находится, то любителям математики, более формальной, чем TeX, но менее формальной, чем Coq, может иметь смысл обратить внимание на sTeX.

https://github.com/slatex/sTeX

[Alexandr Gavrichenko]

Исправления для первого сообщения темы.

Математическое понятие можно записать так же, как химическую формулу.

Исправленная версия заметки:

https://drive.google.com/file/d/1389gaq ... drive_link

[Alexandr Gavrichenko]

Ещё одно исправление версии заметки:
https://drive.google.com/file/d/17LHfKw ... drive_link

[Alexandr Gavrichenko]

В работе Пеано "Formulario mathematico" обозначение

$Num'Cls$

применялось для описания класса натуральных чисел.


Исправленная версия заметки с учётом обозначений Пеано:
https://drive.google.com/file/d/18uWa88 ... drive_link

[Alexandr Gavrichenko]

Alexandr Gavrichenko в сообщении #1602550 писал(а):

В работе Пеано "Formulario mathematico" обозначение

$Num'Cls$

применялось для описания класса натуральных чисел.

Здесь опечатка. Правильно:

применялось для описания класса кардинальных чисел.

[Alexandr Gavrichenko]

Оператор "точка" можно выносить за скобки.

Введём обозначения:

$DPEQ = DPEQ(x, y, z)$ — множество дифференциальных уравнений в частных производных

$DEG(2)$ — второй порядок

$ELP$ — эллиптический
$ HPB$ — гиперболический
$ PRB$ — параболический

Тогда классификация дифференциальных уравнений в частных производных второго порядка записывается так:

$ DEG(2).DPEQ = ELP.DEG(2).DPEQ + HPB.DEG(2).DPEQ + PRB.DEG(2).DPEQ$

Или так:

$DEG(2).DPEQ = (ELP + HPB + PRB).DEG(2).DPEQ$

[Alexandr Gavrichenko]

Alexandr Gavrichenko в сообщении #1602924 писал(а):

$DPEQ = DPEQ(x, y, z)$ — множество дифференциальных уравнений в частных производных

Исправление (по подсказке старших товарищей):


$DPLEQ = DPLEQ(x, y, z)$ — множество линейных дифференциальных уравнений в частных производных

$DEG(2).DPLEQ$ — множество линейных дифференциальных уравнений в частных производных второго порядка

Утверждение о классификации:

$DEG(2).DPLEQ = (ELP + HPB + PRB).DEG(2).DPLEQ$

[Red_Herring]

Alexandr Gavrichenko в сообщении #1602924 писал(а):

Оператор "точка" можно выносить за скобки.

Введём обозначения:

$DPEQ = DPEQ(x, y, z)$ — множество дифференциальных уравнений в частных производных

$DEG(2)$ — второй порядок

$ELP$ — эллиптический
$ HPB$ — гиперболический
$ PRB$ — параболический

Тогда классификация дифференциальных уравнений в частных производных второго порядка записывается так:

$ DEG(2).DPEQ = ELP.DEG(2).DPEQ + HPB.DEG(2).DPEQ + PRB.DEG(2).DPEQ$

Или так:

$DEG(2).DPEQ = (ELP + HPB + PRB).DEG(2).DPEQ$

В самом деле? Тогда прошу объяснить, куда отнести уравнение Шредингера или $u_{xx}+u_{yy}-u_{tt}-u_{zz}=0$ или $u_t=u_{xx}-u_{yy}$.