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

[arseniiv]

kp9r4d в сообщении #1127101 писал(а):

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

Может быть. В любом случае, как ни назови, согласен с остальным, что вы сказали.