Formal mathematics on display : a wiki for Flyspeck

C. Tankink; C. Kaliszyk; J. Urban; J.H. Geuvers

doi:10.1007/978-3-642-39320-4_10

Formal mathematics on display : a wiki for Flyspeck

C. Tankink, C. Kaliszyk, J. Urban, J.H. Geuvers

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

12 Citations (Scopus)

Abstract

The Agora system is a prototype "Wiki for Formal Mathematics", with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The functions implemented in Agora include in-browser editing, strong AI/ATP proof advice, verification, and HTML rendering. The HTML rendering contains hyperlinks and provides on-demand explanation of the proof state for each proof step. In the present paper we show the prototype Flyspeck Wiki as an instance of Agora for HOL Light formalizations. The wiki can be used for formalizations of mathematics and for writing informal wiki pages about mathematics. Such informal pages may contain islands of formal text, which is used here for providing an initial cross-linking between Hales’s informal Flyspeck book, and the formal Flyspeck development. The Agora platform intends to address distributed wiki-style collaboration on large formalization projects, in particular both the aspect of immediate editing, verification and rendering of formal code, and the aspect of gradual and mutual refactoring and correspondence of the initial informal text and its formalization. Here, we highlight these features within the Flyspeck Wiki.

Original language	English
Title of host publication	Intelligent Computer Mathematics (MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings)
Editors	J. Carette, D. Aspinall, C. Lange, P. Sojka, W. Windsteiger
Place of Publication	Berlin
Publisher	Springer
Pages	152-167
ISBN (Print)	978-3-642-39319-8
DOIs	https://doi.org/10.1007/978-3-642-39320-4_10
Publication status	Published - 2013

Publication series

Name	Lecture Notes in Computer Science
Volume	7961
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-642-39320-4_10

Fingerprint Dive into the research topics of 'Formal mathematics on display : a wiki for Flyspeck'. Together they form a unique fingerprint.

Cite this

Tankink, C., Kaliszyk, C., Urban, J., & Geuvers, J. H. (2013). Formal mathematics on display : a wiki for Flyspeck. In J. Carette, D. Aspinall, C. Lange, P. Sojka, & W. Windsteiger (Eds.), Intelligent Computer Mathematics (MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings) (pp. 152-167). (Lecture Notes in Computer Science; Vol. 7961). Springer. https://doi.org/10.1007/978-3-642-39320-4_10

Tankink, C. ; Kaliszyk, C. ; Urban, J. ; Geuvers, J.H. / Formal mathematics on display : a wiki for Flyspeck. Intelligent Computer Mathematics (MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings). editor / J. Carette ; D. Aspinall ; C. Lange ; P. Sojka ; W. Windsteiger. Berlin : Springer, 2013. pp. 152-167 (Lecture Notes in Computer Science).

@inproceedings{417b3e97ca914d14836445a368452777,

title = "Formal mathematics on display : a wiki for Flyspeck",

abstract = "The Agora system is a prototype {"}Wiki for Formal Mathematics{"}, with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The functions implemented in Agora include in-browser editing, strong AI/ATP proof advice, verification, and HTML rendering. The HTML rendering contains hyperlinks and provides on-demand explanation of the proof state for each proof step. In the present paper we show the prototype Flyspeck Wiki as an instance of Agora for HOL Light formalizations. The wiki can be used for formalizations of mathematics and for writing informal wiki pages about mathematics. Such informal pages may contain islands of formal text, which is used here for providing an initial cross-linking between Hales{\textquoteright}s informal Flyspeck book, and the formal Flyspeck development. The Agora platform intends to address distributed wiki-style collaboration on large formalization projects, in particular both the aspect of immediate editing, verification and rendering of formal code, and the aspect of gradual and mutual refactoring and correspondence of the initial informal text and its formalization. Here, we highlight these features within the Flyspeck Wiki.",

author = "C. Tankink and C. Kaliszyk and J. Urban and J.H. Geuvers",

year = "2013",

doi = "10.1007/978-3-642-39320-4_10",

language = "English",

isbn = "978-3-642-39319-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "152--167",

editor = "J. Carette and D. Aspinall and C. Lange and P. Sojka and W. Windsteiger",

booktitle = "Intelligent Computer Mathematics (MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings)",

address = "Germany",

}

Tankink, C, Kaliszyk, C, Urban, J & Geuvers, JH 2013, Formal mathematics on display : a wiki for Flyspeck. in J Carette, D Aspinall, C Lange, P Sojka & W Windsteiger (eds), Intelligent Computer Mathematics (MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings). Lecture Notes in Computer Science, vol. 7961, Springer, Berlin, pp. 152-167. https://doi.org/10.1007/978-3-642-39320-4_10

Formal mathematics on display : a wiki for Flyspeck. / Tankink, C.; Kaliszyk, C.; Urban, J.; Geuvers, J.H.

Intelligent Computer Mathematics (MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings). ed. / J. Carette; D. Aspinall; C. Lange; P. Sojka; W. Windsteiger. Berlin : Springer, 2013. p. 152-167 (Lecture Notes in Computer Science; Vol. 7961).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Formal mathematics on display : a wiki for Flyspeck

AU - Tankink, C.

AU - Kaliszyk, C.

AU - Urban, J.

AU - Geuvers, J.H.

PY - 2013

Y1 - 2013

N2 - The Agora system is a prototype "Wiki for Formal Mathematics", with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The functions implemented in Agora include in-browser editing, strong AI/ATP proof advice, verification, and HTML rendering. The HTML rendering contains hyperlinks and provides on-demand explanation of the proof state for each proof step. In the present paper we show the prototype Flyspeck Wiki as an instance of Agora for HOL Light formalizations. The wiki can be used for formalizations of mathematics and for writing informal wiki pages about mathematics. Such informal pages may contain islands of formal text, which is used here for providing an initial cross-linking between Hales’s informal Flyspeck book, and the formal Flyspeck development. The Agora platform intends to address distributed wiki-style collaboration on large formalization projects, in particular both the aspect of immediate editing, verification and rendering of formal code, and the aspect of gradual and mutual refactoring and correspondence of the initial informal text and its formalization. Here, we highlight these features within the Flyspeck Wiki.

AB - The Agora system is a prototype "Wiki for Formal Mathematics", with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The functions implemented in Agora include in-browser editing, strong AI/ATP proof advice, verification, and HTML rendering. The HTML rendering contains hyperlinks and provides on-demand explanation of the proof state for each proof step. In the present paper we show the prototype Flyspeck Wiki as an instance of Agora for HOL Light formalizations. The wiki can be used for formalizations of mathematics and for writing informal wiki pages about mathematics. Such informal pages may contain islands of formal text, which is used here for providing an initial cross-linking between Hales’s informal Flyspeck book, and the formal Flyspeck development. The Agora platform intends to address distributed wiki-style collaboration on large formalization projects, in particular both the aspect of immediate editing, verification and rendering of formal code, and the aspect of gradual and mutual refactoring and correspondence of the initial informal text and its formalization. Here, we highlight these features within the Flyspeck Wiki.

U2 - 10.1007/978-3-642-39320-4_10

DO - 10.1007/978-3-642-39320-4_10

M3 - Conference contribution

SN - 978-3-642-39319-8

T3 - Lecture Notes in Computer Science

SP - 152

EP - 167

BT - Intelligent Computer Mathematics (MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings)

A2 - Carette, J.

A2 - Aspinall, D.

A2 - Lange, C.

A2 - Sojka, P.

A2 - Windsteiger, W.

PB - Springer

CY - Berlin

ER -

Tankink C, Kaliszyk C, Urban J, Geuvers JH. Formal mathematics on display : a wiki for Flyspeck. In Carette J, Aspinall D, Lange C, Sojka P, Windsteiger W, editors, Intelligent Computer Mathematics (MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings). Berlin: Springer. 2013. p. 152-167. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-39320-4_10