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

[Alexandr Gavrichenko]

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

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

1. Логическая структура

К стандартным логическим символам добавляются $\rfloor$ (пусть) и $\vdash$ (тогда).


Запись ($\mathrm{Th}. 2 \mid x\mapsto a$) означает ссылку на формулировку теоремы 2, в которой параметр $x$ заменяется параметром $a$.

Часть доказательства, заключённая в скобки $(_{asd} \,\,\, _{asd}) $, проводится методом "от противного".


2. Буквы и аббревиатуры

Предположим, что в тексте часто упоминаются математические объекты одного типа (например, кольца). В этом случае зарезервируем для обозначения таких объектов букву (например, $R$). На протяжении всего текста эта буква будет обозначать объект данного типа. При необходимости ввести несколько объектов данного типа можно воспользоваться той же буквой с индексами. Запись $r \in R$ автоматически будет расшифровываться как "$r$ - элемент кольца", а запись $R_1 \sqsubset R_2$ - как "$R_1$ - подкольцо кольца $R_2$".

Для того чтобы обозначить класс объектов, применяются аббревиатуры. Класс колец можно обозначить $RNG$, класс групп - $GRP$, класс коммутативных объектов - $COM$.
Тогда класс абелевых (коммутативных) групп можно обозначить $COM.GRP$, а запись $g \in G \in COM.GRP$ будет расшифровываться как "$g$ является элементом абелевой группы $G$".
Если класс объектов образует категорию, то аббревиатуру класса следует подчеркнуть. Например, $\underline{COM.RNG}$ - категория коммутативных колец.
Зарезервировав для понятия "простой", аббревиатуру $PRM$, получим обозначения для множества простых чисел - $PRM.\mathbb{Z}$ и для множества простых идеалов данного кольца - $PRM.IDL(R)$. Если буква $I$ обозначает идеал, то запись $I \in PRM$ означает, что $I$ - простой идеал.

Запись $f : A {\rightarrow}_{hme} B$ означает, что $f$ - гомеоморфизм ($hme$).

Списки букв и аббревиатур размещаются в указателе обозначений.

Соединение аббревиатур точкой аналогично обращению к члену класса в языке программирования C++.

Изложение с дополнениями в виде pdf-файла в хранилище Google Диск.
https://drive.google.com/file/d/1wp3-Fb ... 6ur8-/view

Исправленная версия заметки (добавлена ссылка на монографию С.И. Адяна, где используются схожие обозначения):
https://drive.google.com/file/d/1TuzXeX ... pFpzY/view

Практическая реализация предлагаемого способа в виде конспектов конкретных математических текстов в виде pdf-файлов доступна по следующим ссылкам:

Конспект книги В.Г. Каца и П. Чена "Квантовый анализ".
https://drive.google.com/file/d/13qJvqZ ... PDV0C/view

Конспект §§1-11 главы 1 книги Ю.И. Манина "Введение в теорию схем и квантовые группы".
https://drive.google.com/file/d/1eD98R2 ... mQRvN/view

[Lia]

Тема перемещена из форума «Дискуссионные темы (М)» в форум «Карантин»
по следующим причинам:

- просьба предельно четко сформулировать предмет темы,
- касательно внешних ссылок см п. 5 правил форума topic3476.html
- (краткие инструкции по набору формул: «Краткий FAQ по тегу [math]» и видеоролик Как записывать формулы);


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

[Lia]

Тема перемещена из форума «Карантин» в форум «Дискуссионные темы (М)»
Причина переноса: пока сюда.

[bot]

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

Практическая реализация предлагаемого способа в виде конспектов конкретных математических текстов в виде pdf-файлов доступна по следующим ссылкам:

Для шпаргалок годится - проверено на себе.

[mustitz]

А чем это лучше чем Coq?

[Alexandr Gavrichenko]

bot в сообщении #1479968 писал(а):

Для шпаргалок годится - проверено на себе.

Объём текста уменьшается ориентировочно на 30%.

mustitz в сообщении #1479986 писал(а):

А чем это лучше чем Coq?

Здесь предлагается однотипный способ записи разнообразных терминов на основе обозначения математического понятия, такого же как обращение к элементу записи в языках программирования (например, Паскаль).
Судя по статье в Википедии https://ru.wikipedia.org/wiki/Coq (с Coq я не знаком) элементы этого способа есть в Coq, поскольку Peano.plus и Peano.mult означают пеановские сложение и умножение.
Я рассмотрел возможность сделать такую запись повсеместно применяемой в обычном тексте (книге, статье), а не только в языке программирования. Тогда открывается возможность сделать математический текст машинно распознаваемым.
В моей работе собственно автоматическое доказательство теорем не рассматривается.

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

[demolishka]

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

Известно, что математический текст представляет собой формулу

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

Для людей это не подходит. Для компьютеров - есть более основательные подходы.

[Alexandr Gavrichenko]

demolishka в сообщении #1480609 писал(а):

Тут тоже новые закорючки придумывать будем?

Почему бы и нет. В настоящем же виде

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

список обозначений, исторические и идейные замечания

записываются на естественном языке. Формализации подлежат формулировки определений и теорем и доказательства.
Вводя аббревиатуру для неизвестного понятия $XYZ$, можно формализованно записывать и некоторые наводящие соображения в виде вопросов.

Запись

$$SPC(R) \in IRD.TOP.SPACE \Leftrightarrow NPT(R) \in XYZ$$

эквивалентна вопросу: как охарактеризовать нильрадикал кольца с неприводимым спектром?

Ответ:

$$XYZ = PRM.IDL(R)$$

(нильрадикал прост).

demolishka в сообщении #1480609 писал(а):

Для людей это не подходит.

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

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

$$\forall I \in PRM \quad \exists I' \in MAX \quad (I \subset I' \subset R)$$

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

demolishka в сообщении #1480609 писал(а):

Для компьютеров - есть более основательные подходы.

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

[demolishka]

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

Это с непривычки.

Дело не в привычке, а в неэффективности. Вы просто сокращаете английские слова и требуете некоторой однозначной записи высказываний.

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

её плюс в том, что уменьшается число разночтений.

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

[Alexandr Gavrichenko]

demolishka в сообщении #1480680 писал(а):

плюс только для "левополушарных математиков"

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

demolishka в сообщении #1480680 писал(а):

распознавать формулы подобно компьютеру

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

demolishka в сообщении #1480680 писал(а):

неэффективности

Ещё раз: запись "неизвестная величина, умноженная на себя" неэффективна в том смысле, что никто ей не пользуется. Так что есть уровень, на котором формализация общепринята.

demolishka в сообщении #1480680 писал(а):

Вы просто сокращаете английские слова

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

[demolishka]

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

Так что есть уровень, на котором формализация общепринята.

Уровень есть, только Вы его доводите до абсурда.

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

правополушарнику

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

Из Вашей посылки, что

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

математический текст представляет собой формулу

путь только в компьютерную проверку доказательств теорем. Либо это так и останется как Ваше личное развлечение.

[Alexandr Gavrichenko]

demolishka в сообщении #1480694 писал(а):

Вы его доводите до абсурда.

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

demolishka в сообщении #1480694 писал(а):

путь только в компьютерную проверку доказательств теорем.

Скорей обучение компьютера математике.

[mustitz]

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

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

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

[Sycamore]

Формализация вроде Coq-а реално нужна для проверки доказательств только в очень редких и исключительных случаях, когда эти доказательства оказываются слишком громоздкими, хаотическими и с трудом обозримыми для экспертов: задача 4-ых красок, решение Т.Хейлсом гипотезы Кеплера и подобные плохо структурированные проблемы с большущим пространством перебора. Полная формализация чревата большими накладными расходами и серьёзными ошибками при интуитивной/содержательной интерпретации чужих мышлению формальных текстов. На мой взгляд, для подавляющего большинства работающих математиков и проблем такая формализация не стоит свеч и ненужно затормозила бы продуктивность.

[Alexandr Gavrichenko]

mustitz в сообщении #1480701 писал(а):

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

Этот вопрос так же уместен по отношению к Coq, как и к предложенной "нотации".
Можно ли научить компьютер (тот же Coq) воспринимать уже написанный текст?
То есть, Coq "читает" статью или книгу и автоматически добавляет содержащиеся в тексте теоремы в свой список лемм. Здесь формализация текста может оказаться полезной.

mustitz в сообщении #1480701 писал(а):

И в результате получить то же представление в мозгу, что и раньше.

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

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

серьёзными ошибками при интуитивной/содержательной интерпретации чужих мышлению формальных текстов.

Остаётся возможность, что эта интерпретация будет не ошибочной, а альтернативной.


О передаче идей в формализованном тексте

Идеи передаются обычным (естественным) языком и никак не формализуются.

Конспект книги В. Г. Каца и П. Чена "Квантовый анализ", §7, Th.4
https://drive.google.com/file/d/13qJvqZ ... PDV0C/view
Доказательство содержит обращение к интуитивному представлению о выборе шаров и записывается естественным языком.