2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу 1, 2  След.
 
 Проект Metamath в учебных целях
Сообщение10.05.2016, 16:04 


10/05/16
2
Предисловие: существует проект формализации математики под названием 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.

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение10.05.2016, 16:42 


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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение10.05.2016, 16:58 


10/05/16
2
Ruslan_Sharipov в сообщении #1122541 писал(а):
В педагогических целях вряд ли.

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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение10.05.2016, 17:36 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение10.05.2016, 18:40 
Заслуженный участник
Аватара пользователя


01/03/06
13626
Москва
Dg7780 в сообщении #1122546 писал(а):
что именно мешает Metamath служить педагогическим целям?

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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение10.05.2016, 21:25 


19/05/10

3940
Россия
Dg7780 в сообщении #1122546 писал(а):
...Хорошо. Но что именно мешает Metamath служить педагогическим целям?
Педагогика это инструмент, смазка. Что такое педагогическая цель? и какие они бывают цели эти, педагогические?

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение11.05.2016, 09:34 
Заслуженный участник
Аватара пользователя


22/06/12
2129
/dev/zero
Dg7780 в сообщении #1122546 писал(а):
что именно мешает Metamath служить педагогическим целям?

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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение11.05.2016, 21:02 
Заслуженный участник


08/04/08
8556
Dg7780 в сообщении #1122531 писал(а):
Вопрос: можно ли человек ипользовать эти формализованные теоремы Metamath в педагогических целях, для самообучения математике, вместо традиционных неформализованных математических учебных материалов? Сможет ли он решать такие же проблемы и разбираться в математике так же, как если бы обучался на традиционных материалах?

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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение11.05.2016, 22:58 
Заслуженный участник


11/05/08
32166
Dg7780 в сообщении #1122531 писал(а):
Вопрос: можно ли человек ипользовать эти формализованные теоремы Metamath в педагогических целях, для самообучения математике, вместо традиционных неформализованных математических учебных материалов?

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

Dg7780 в сообщении #1122531 писал(а):
Биномиальная теорема: http://us.metamath.org/mpegif/binomlem.html

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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение17.05.2016, 03:17 
Заслуженный участник


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

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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение28.05.2016, 18:34 
Заслуженный участник


15/05/05
3445
USA
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...

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение29.05.2016, 14:07 


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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение29.05.2016, 20:09 
Заслуженный участник
Аватара пользователя


09/02/14

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

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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение30.05.2016, 08:26 
Заслуженный участник


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

(alex_dorin)

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

 Профиль  
                  
 
 Re: Проект Metamath в учебных целях
Сообщение30.05.2016, 08:46 
Заслуженный участник
Аватара пользователя


09/02/14

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

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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 16 ]  На страницу 1, 2  След.

Модераторы: Модераторы, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group