Формализация математики упирается уже в выбор определений. В проекте Annals Challenge К...
Формализация математики упирается уже в выбор определений. В проекте Annals Challenge Кевин Баззард ставит задачу записать на формальном языке формулировки всех теорем из недавних выпусков Annals of Mathematics, пока без доказательств. Главным препятствием здесь оказываются недостающие определения. Проект должен стимулировать создание формальных определений, которыми действительно пользуются исследователи. Это помогает понять требования к большой математической библиотеке. Её понятия должны иметь ожидаемый математиком смысл, а связь с литературой должна позволять это проверить. Теоремы стоит формулировать достаточно общо для повторного использования, избегать дублирования, документировать и систематически организовывать материал. Именно такие принципы предлагают авторы эссе «How to Formalize All of Mathematics». У машинной проверки есть конкретная задача. Lean позволяет проверять корректность формального доказательства. Но для дальнейшей работы с библиотекой важно также понимать, что именно доказано. Поэтому реестр проектов Palomar требует и метаданные с описанием формализованного результата и его происхождения, и настройку Comparator, облегчающую аудит точного утверждения. Авторы эссе предлагают оценивать формализацию по тому, что она позволяет делать дальше. Можно ли с её помощью искать обобщения, исследовать связи между разделами, находить приложения, улучшать сами определения? В этой перспективе понятность, организация и возможность повторного использования входят в цель формализации с самого начала. https://github.com/ImperialCollegeLondon/AnnalsChallenge Наши каналы MAX · Telegram · Дзен #математика #формализация #доказательства #математическаялогика