Vlasov, D. Yu. The language of formal mathematics Russell. (Russian. English summary) Zbl 1249.03006 Vestn. Novosib. Gos. Univ., Ser. Mat. Mekh. Inform. 11, No. 2, 27-50 (2011). Summary: Russell is a computer language for formal mathematics which is intended to represent modern mathematics on a formal level and to 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 the 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 a candidate for the QED manifesto realization. MSC: 03B35 Mechanization of proofs and logical operations 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68W30 Symbolic computation and algebraic computation Keywords:formal mathematics; automated reasoning; presentation of mathematical knowledge; automated proof checking; Russell Software:Russell; Smm; Metamath PDF BibTeX XML Cite \textit{D. Yu. Vlasov}, Vestn. Novosib. Gos. Univ., Ser. Mat. Mekh. Inform. 11, No. 2, 27--50 (2011; Zbl 1249.03006) OpenURL