Язык формальной математики Russell

Russell — это компьютерный язык формальной математики, предназначенный для представления современной математики на формальном уровне, надежной проверки доказательств и автоматизации рутинных (технических) доказательств при доказательстве теорем. Russell является языком высокого уровня над языком smm, который, в свою очередь, является упрощенной версией языка формальной математики metamath. Ключевыми особенностями Russell являются: сохранение уровня универсальности и надежности языка metamath, возможность читать и реадктировать тексты формальных доказательств без привлечения специальных программ, чего лишен язык metamath. Язык Russell может считаться кандидатом на полную реализацию QED манифеста.