Geodesic
Russell, the Language for Formal Mathematics
Sibirskij žurnal čistoj i prikladnoj matematiki, Tome 11 (2011) no. 2, pp. 27-50 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

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.
Keywords: formal mathematics, automated reasoning, presentation of mathematical knowledge, automated proof checking. 
@article{VNGU_2011_11_2_a3,
     author = {D. Yu. Vlasov},
     title = {Russell, the {Language} for {Formal} {Mathematics}},
     journal = {Sibirskij \v{z}urnal \v{c}istoj i prikladnoj matematiki},
     pages = {27--50},
     year = {2011},
     volume = {11},
     number = {2},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VNGU_2011_11_2_a3/}
}
TY  - JOUR
AU  - D. Yu. Vlasov
TI  - Russell, the Language for Formal Mathematics
JO  - Sibirskij žurnal čistoj i prikladnoj matematiki
PY  - 2011
SP  - 27
EP  - 50
VL  - 11
IS  - 2
UR  - http://geodesic.mathdoc.fr/item/VNGU_2011_11_2_a3/
LA  - ru
ID  - VNGU_2011_11_2_a3
ER  - 
%0 Journal Article
%A D. Yu. Vlasov
%T Russell, the Language for Formal Mathematics
%J Sibirskij žurnal čistoj i prikladnoj matematiki
%D 2011
%P 27-50
%V 11
%N 2
%U http://geodesic.mathdoc.fr/item/VNGU_2011_11_2_a3/
%G ru
%F VNGU_2011_11_2_a3
D. Yu. Vlasov. Russell, the Language for Formal Mathematics. Sibirskij žurnal čistoj i prikladnoj matematiki, Tome 11 (2011) no. 2, pp. 27-50. http://geodesic.mathdoc.fr/item/VNGU_2011_11_2_a3/

[1] Appel K., Haken W., “Every Planar Map Is Four Colorable. Part I: Discharging”, Illinois J. Math., 21 (1977), 429–490 | MR | Zbl

[2] Appel K., Haken W., “Every Planar Map Is Four Colorable. Part II: Reducibility”, Illinois J. Math., 21 (1977), 491–567 | MR | Zbl

[3] Hales Th. C., “A Proof of the Kepler Conjecture”, Annals of Mathematics. Second Series, 162:3 (2005), 1065–1185 | DOI | MR | Zbl

[4] Aschbacher M., “The Status of the Classification of the Finite Simple Groups”, Mathematical Monthly, 51:7 (2004), 736–740 | MR | Zbl

[5] Sudoplatov S. V., Problema Lakhlana, Ser. Monografii NGTU, Izd-vo NGTU, Novosibirsk, 2009

[6] Barendregt H., Wiedijk F., “The Challenge of Computer Mathematics”, Transactions A of the Royal Society, 363:1835 (2005), 2351–2375 http://www.cs.ru.nl/f̃reek/notes/RSpaper.pdf | DOI | MR | Zbl

[7] Boyer R. et al., “The QED Manifesto”, Automated Deduction, CADE 12, LNAI, 814, ed. A. Bundy, Springer-Verlag, 1994, 238–251 http://www.cs.ru.nl/\allowbreakf̃reek/qed/qed.ps.gz | MR

[8] Wiedijk F., The Seventeen Provers of the World, Foreword by Dana S. Scott, LNAI, 3600, Springer, 2006 http://www.cs.ru.nl/f̃reek/comparison/comparison.pdf | MR

[9] Wiedijk F., “The QED Manifesto Revisited”, Studies in Logic, Grammar and Rhethoric, 10(23) (2007), 121–133 http://mizar.org/trybulec65/8.pdf

[10] Megill N. D., Metamath: A Computer Language for Pure Mathematics, Lulu Press, Morrisville, North Carolina, USA, 1997 http://us.metamath.org/downloads/metamath.pdf