Аннотация:
Описывается синтаксис и семантика языка smm – компьютерного языка формальной математики, предназначенного для представления современной математики на формальном уровне и надежной проверки, который является упрощенной версией языка формальной математики metamath.
Ключевые слова:формальная математика, представление математического знания, автоматическая проверка доказательств.