The language of formal mathematics Russell. (Russian. English summary) Zbl 1249.03006

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.


03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation


Metamath; Smm; Russell