Анимация формул

Аватар пользователя
Ian
Сообщений: 960
Зарегистрирован: 18 янв 2016, 19:42

Анимация формул

Сообщение Ian » 18 окт 2017, 12:42

Почему бы на вставить в матпакеты такие функции как преобразование формул с контролем за правильностью этих преобразований. Вот например набрал я уравнение [math]Единичку зацепляю мышкой и тащу правее знака равенства, комп догадывается что я хочу перенести в правую часть с противоположным знаком, и пишет мне на этом месте [math], но запоминает, что я сделал. Потом я зацепляю двойку и тащу правее и ниже формулы, комп догадывается что я хочу поделить уравнение на 2 и пишет на этом же месте [math]. Но запоминает он не просто результат, а анимированную формуду [math] и потом при открытии файла когда на нее курсор навожу она из первой превращается во вторую и дальше в третью. Мне бы лично такое было удобно читать вместо скучной цепочки преобразований одно под другим, а заодно помогает не ошибаться. Но это не только с целью младших школьников учить, а пусть будут и анимированные статьи в ВАКовских журналах, там экономят место, и поэтому догадаться как автор перевел одну большую формулу в другую- как правило надо бумажку брать, а будет и видно как, и знак качества- компом проверено. А когда подрастут младшеклассники, которых так учили, для них уже это будет так естественно как гаджет в кармане. Ну короче это так просто что наверное уже где-то есть, на учебных сайтах , гифки всякие. В поверпойнт я сам пару раз анимацию делал но трудоемко, чтобы приложить надо искать на старом компе. У многих лекторов кстати есть манера сокращение и уничтожение членов в формуле производить не мелом а тряпкой, что ставит в тупик студентов которые тупо списывают с доски, списал левую часть до стирания, а правую после, ну так тебе и надо, думай или на видео снимай) Ну и наконец если шахматы анимируют и почти всем это нравится, то что мы глупее шахматистов? А нам нужнее, разнообразие действий больше)

zykov
Сообщений: 1393
Зарегистрирован: 06 янв 2016, 17:41

Анимация формул

Сообщение zykov » 19 окт 2017, 01:04

Ian, мне кажется, Вы тут смешиваете две разные вещи.

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

Вторая - это машинная помощь при доказательстве теорем. В том числе и автоматизированная проверка.
Сам никогда не пользовалься такими системами, но читал, что такие есть. Вот на wiki есть статья про proof assistant (interactive theorem prover). Там есть список существующих компьютерных систем, которые можно использовать в интерактивном режиме в процессе поиска доказательства. Ещё есть системы автоматического поиска доказательства, но это уже из другой области (из области ИИ). Тоже интересно, но там успехи весьма ограниченные.
Другое полезное направление - это автоматизированная проверка доказательств (Automated proof checking).
Тут идея такая, что доказательство - это просто строка записанная в соответствии с определенными правилами синтаксиса. Если какая-то строка синтаксически коректна, то она представляет коректное доказательство. Ну а проверку коректности синтаксиса легко сделать на компьютере. Правда сначала нужно закодировать доказательство в соответствии с правилами выбранного языка представления.
Идея довольно интересная. В самом деле, на сегодняшний день в математике есть огромная база доказательств в разных областях. Некоторые из них довольно сложны для проверки человеком и возможно где-то есть какие-то ошибки. Было бы замечательно всё это забить в компьютер и прверить формально. Даже возник такой прект QED manifesto. Правда в wiki написано, что они провели только две конференции (1994 и 1995), а потом в 1996 проект как бы умер. Тем ни менее есть компьютерные системы (например Mizar, HOL) с функциональностью автоматической проверки доказательств и при этом довольно солидной базой оцифрованных доказательств.

Если есть интерес, то можете глубже копнуть в этом направлении или попробовать самостоятельно одну из таких систем (например Mizar).

zykov
Сообщений: 1393
Зарегистрирован: 06 янв 2016, 17:41

Анимация формул

Сообщение zykov » 19 окт 2017, 01:17

Да, на равне с Mizar и HOL следует упоминуть Metamath.

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

При этом конечный результат не обещает каких то новых прорывов. Ну может где найдём пропущеные ошибки. Но новых результатов оно не обещает. А усилия при этом весьма значительные.

Аватар пользователя
Ian
Сообщений: 960
Зарегистрирован: 18 янв 2016, 19:42

Анимация формул

Сообщение Ian » 19 окт 2017, 08:31

zykov, спасибо, такого рода обзора я и ждал от человека на порядок более эрудированного.
Я больше всего жду прорыва не столько от разработчиков матпакетов, сколько от разработчиков математических редакторов (из которых знаю латех и ликс), в смысле приближения их функционала к имеюшемуся в матпакетах, в части редактировании больших формул.
У меня есть простая статистика. Опытные люди, тоже бывшие преподаватели, должны были как можно быстрее написать решение задачки про коэффициенты Фурье кусочно-непрерывной функции на отрезке, как Вы догадываетесь, решение с трудом уместится на тетрадный лист. Они пишут ручкой на листе а я пишу в редакторе Lyx2.0. И у меня выходит быстее чем у них, и к тому же подробнее примерно 3,5 минуты у меня, 4,5 минуты ручкой. Как такое возможно. Беру строчку из интегралов и копирую в следующую. Вношу изменения там где они малы например какой-то интеграл заменяю на результат интегрирования по частям, у другого множитель вынесу.... А мои конкуренты в это время переписывают ручкой всю формулу с теми же малыми изменениями, и хорошо если без ошибки перепишут, спешка ведь.А я в это время свой результат копирую в следующую строчку, и снова редактирую. Вот Вам и 2 страницы набранные за 3,5 минут.Уж не думал что буду в этом компоненте выигрывать у людей в 2-5 раз моложе, причем регулярно.
А вот еще одно явление. Девушки затачивают ноготок специальным образом и так быстро и точно стучат им по виртуальной маленькой клавиатуре на гаджете (ну как колибри клюет) что регулярно обгоняют устную речь, даже быстро протараторить точно те же слова выйдет медленнее) Засекали несколько раз. Чисто эргономика, рот при речи раскрывается до 3 см на каждый звук, а ее пальчик перемещается на 1 -3 см для этого же, но он легче)
Это я пишу не с целью экономить секунды при болтовне девушек о нарядах, а в принципе избавлять человека от действий хотя и привычных, но объективно необязательных, чтобы оставалось больше времени на суть

zykov
Сообщений: 1393
Зарегистрирован: 06 янв 2016, 17:41

Анимация формул

Сообщение zykov » 21 окт 2017, 00:24

Ian писал(а):Source of the post сколько от разработчиков математических редакторов

При отсутствии спроса разработчики добавлять не будут. Им это просто не нужно.

Если нужна такая анимация, то скорее придется делать самому (как говорится, спасение утопающего - дело рук самого утопающего).
Делать через всякие всякие редакторы WYSIWYG довольно трудоёмко. Например можно делать презентацию в powerpoint и там же делать анимацию. Но автоматизировать там не так просто.
Мне кажется, что проще автоматизировать в контексте какого-то языка, такого как TeX (можно написать скрипт генерирующий нужный текстовый код).
Кстати, сами презентации тоже можно делать в TeX. Есть там такой пакет - Beamer. Позволяет верстать презентации. Потом просаматриватся/показывать в PDF просмоторщике.
Вот ещё про него статья: https://habrahabr.ru/post/145523/


Если же нужно это делать на Web, то тут можно обратить внимание на формат векторной графики SVG. Там графика тоже задается в текстовом виде (через XML), что тоже можно генерировать скриптом. Есть и возможности по анимации через SMIL (вот конкретно про анимацию SVG - там внизу есть примеры).
Это всё уже доступно в рамках стандарта HTML5. Там же кстати есть и язык для математических формул MathML (тоже на базе XML).

Аватар пользователя
Ian
Сообщений: 960
Зарегистрирован: 18 янв 2016, 19:42

Анимация формул

Сообщение Ian » 29 окт 2017, 12:15

zykov писал(а):При отсутствии спроса разработчики добавлять не будут. Им это просто не нужно.
Когда есть спрос, то конечно все зашевелятся. Но винды например возникли без спроса, просто нескольким людям показалось, что это удобно. Был явный спрос на мультизадачность, но не обязательно на оконный интерфейс.Я помню, как в начале 90х все это обсуждалось в прессе, ни один эксперт не промолчал)


Вернуться в «Computer Science»

Кто сейчас на форуме

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