Новости из-за переднего края науки.
http://concolor.livejournal.com/26144.html?style=mine
concolor дошел до Берлина первого релиза своей системы формальной математики. Привожу авторский анонс as-is:эм....
Какбы релиз у меня. Альфа-версия транслятора с mdl в mm. Слабенькая, конечно.
НО! уже полная трансляция. То есть трансляция проводится в два конца - туда и обратно, и проверяется чекером. Для этого есть скрипт test.
Есди чо, лежит здесь:
https://sourceforge.net/projects/mathdevlanguage/
Версия 0.7.3
WiKi:
ЧТО ЭТО:
ядро системы формальной математики. Транслятор с языка mdl в язык metamath (www.metamath.org) и обратно.
ЗАЧЕМ ЭТО:
разделение системы формальной математики на 2 уровня:
1) mdl - язык высокого уровня. Удобен для написания и доказательства теорем. доказательства на языке mdl (в отличие от metamath) - читабельные.
2) язык metamath - язык низкого уровня. Очень прост и удобен для реализации, позволяет писать очень простые (а значит и надежные) верификаторы. Но плохо читабелен человеком. Доказательства в metamath вообще человеком абсолютно не читабельны.
ТЕКУЩЕЕ СОСТОЯНИЕ:
Базовый транслятор с упрощенного mdl в metamath. Тест сьют включает 10 теорем. Многие фичи полной математики ещё не реализованны.
ПЛАНЫ:
Реализация полного языка mdl. Но это все фигня, цветочки. Главная цель - прувер, система автоматического доказательства теорем. Но пока ещё это только в планах.....
P.S. Ко мне с вопросами по -- лезть бесполезно.