Russell, the Language for Formal Mathematics

Russell is a computer language for the formal mathematics, which is intended to represent the modern mathematics on a formal level, provide trustworthy proof verification and automation of routine (technical) proofs. Russell is a high-level superstructure language over the smm language, which, in turn, is a simplified version of metamath language. The main features of Russell are: universality and reliability of metamath, human readable and editable proof texts, which may be managed without external programs. Russell may be concerned a candidate for the QED manifesto realisation.