Проект Metamath в учебных целях

[Dg7780]

Предисловие: существует проект формализации математики под названием Metamath, оффициальный сайт проекта - http://us.metamath.org/index.html. Кратко говоря, авторы формализировали около тридцати тысяч основных теорем (список: http://us.metamath.org/mpegif/mmtheorems.html) из самых различных областей математической науки, как таковой: от самой примитивной логики и определения числа до теории чисел и топологии. Важно отметить, что формализованные теоремы Metamath не являются автоматически созданными, все они прошли путь от непосредственного ручного создания людьми и только конечной компьютерной проверки на правильность.
Вопрос: можно ли человек ипользовать эти формализованные теоремы Metamath в педагогических целях, для самообучения математике, вместо традиционных неформализованных математических учебных материалов? Сможет ли он решать такие же проблемы и разбираться в математике так же, как если бы обучался на традиционных материалах?

Примеры некоторых формализованных теорем. Биномиальная теорема: http://us.metamath.org/mpegif/binomlem.html, описание и основные теоремы векторного пространства: http://us.metamath.org/mpegif/mmtheorems140.html#mm13957b.

[Ruslan_Sharipov]

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

[Dg7780]

Ruslan_Sharipov в сообщении #1122541 писал(а):

В педагогических целях вряд ли.

Хорошо. Но что именно мешает Metamath служить педагогическим целям?

[arseniiv]

Тем, что формальные доказательства не снабжены каким-то «смысловым слоем» (ведь для проверки правильности этого не требуется), так что доказательства длиннее десятка шагов будет довольно трудно распутать. Можно, конечно, написать конвертер такого доказательства к более привычному виду, но эта задача очень объёмная.

[Brukvalub]

Dg7780 в сообщении #1122546 писал(а):

что именно мешает Metamath служить педагогическим целям?

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

[mihailm]

Dg7780 в сообщении #1122546 писал(а):

...Хорошо. Но что именно мешает Metamath служить педагогическим целям?

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

[StaticZero]

Dg7780 в сообщении #1122546 писал(а):

что именно мешает Metamath служить педагогическим целям?

А чему можно научить с помощью Metamath?

[Sonic86]

Dg7780 в сообщении #1122531 писал(а):

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

Насколько я понимаю, в Metamath ограниченное количество терминов. Да?
Если да, то - не может (может с очень низким КПД), поскольку не узнает всех тех терминов, которые есть в математике. Язык математики позволяет развивать язык достаточно сильно.
Если нет, то пардон.

[ewert]

Dg7780 в сообщении #1122531 писал(а):

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

Вы же сами на свой вопрос и ответили:

Dg7780 в сообщении #1122531 писал(а):

Биномиальная теорема: http://us.metamath.org/mpegif/binomlem.html

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

[arseniiv]

Sonic86 в сообщении #1122902 писал(а):

Насколько я понимаю, в Metamath ограниченное количество терминов.

Там интересная вещь в том, что даже то, что считается «базовыми» символами алфавита любого, для примера, языка первого порядка, в Metamath вводится явно. [Можно на основе Metamath построить, например, λ-исчисление (мне кажется, и любую «серьёзную» теорию типов), и он будет работать так же хорошо, а помощники построения доказательства (кажется, там несколько есть, судя по тому, что как-то давно читал) будут работать тоже.] Кстати, потому там скобки нигде не опускаются и есть обозначения довольно разные синтаксически — формулы не делятся на подформулы явно, хотя этим делением можно было бы считать вывод метаутверждения о корректности формулы. Но системе нужен только факт корректности формулы, а не конкретный вид доказательства этого факта.

Это было прелюдией перед словами о том, что свою систему Metamath можно расширять практически чем угодно. Какими угодно символами — точно. Синтаксис какой угодно уже не введёшь, а то могут появиться неоднозначно читаемые формулы. Но тут Metamath не уникален.

[Yuri Gendelman]

Dg7780 в сообщении #1122531 писал(а):

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

Ответ авторов Metamath:

Цитата:

Q: Will Metamath help me learn abstract mathematics?
A: ... this is quite different from understanding the meaning of the math that results. Metamath alone probably will not give you an intuitive feel for abstract math...

[alex_dorin]

На сайтe Metamath касательно ZFC
http://us.metamath.org/mpegif/mmset.html#axioms
приведена аксиома выбора - Axiom of Choice,
Я думаю, что она там написана с ошибками.

[kp9r4d]

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

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

[arseniiv]

В Metamath не просто теория первого порядка, там вместо переменных метапеременные, которые заменяются переменными (отсюда имеющиеся иногда ограничения distinct variable groups и отсюда же meta в названии).

(alex_dorin)

alex_dorin в сообщении #1126926 писал(а):

Я думаю, что она там написана с ошибками.

И давайте мы их тут поугадываем за вас? Напишите, какие ошибки вы там видите. Только сначала прочитайте мотивацию и заметьте, что альтернативные формулировки присутствуют тоже: http://us.metamath.org/mpegif/ax-ac.html.

[kp9r4d]

arseniiv

arseniiv в сообщении #1127097 писал(а):

В Metamath не просто теория первого порядка, там вместо переменных метапеременные, которые заменяются переменными (отсюда имеющиеся иногда ограничения distinct variable groups и отсюда же meta в названии).

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