The language of formal mathematics Russell. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 1 article , 1 standard article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Vlasov, D.Yu.: The language of formal mathematics Russell (2011)