{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:25:42Z","timestamp":1748413542780},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642393198"},{"type":"electronic","value":"9783642393204"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39320-4_10","type":"book-chapter","created":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T07:22:52Z","timestamp":1372663372000},"page":"152-167","source":"Crossref","is-referenced-by-count":10,"title":["Formal Mathematics on Display: A Wiki for Flyspeck"],"prefix":"10.1007","author":[{"given":"Carst","family":"Tankink","sequence":"first","affiliation":[]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]},{"given":"Herman","family":"Geuvers","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"10_CR1","first-page":"153","volume":"3","author":"A. Grabowski","year":"2010","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Mizar in a nutshell. Journal of Formalized Reasoning\u00a03(2), 153\u2013245 (2010)","journal-title":"Journal of Formalized Reasoning"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2009","unstructured":"Harrison, J.: HOL Light: An overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 60\u201366. Springer, Heidelberg (2009)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: Engineering mathematics: the odd order theorem proof. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 1\u20132. ACM (2013)","DOI":"10.1145\/2480359.2429071"},{"key":"10_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-87827-8_28","volume-title":"Computer Mathematics","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: The four colour theorem: Engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol.\u00a05081, p. 333. Springer, Heidelberg (2008)"},{"issue":"1","key":"10_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00454-009-9148-4","volume":"44","author":"T.C. Hales","year":"2010","unstructured":"Hales, T.C., Harrison, J., McLaughlin, S., Nipkow, T., Obua, S., Zumkeller, R.: A revision of the proof of the Kepler conjecture. Discrete & Computational Geometry\u00a044(1), 1\u201334 (2010)","journal-title":"Discrete & Computational Geometry"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Tankink, C.: Proof in context \u2014 web editing with rich, modeless contextual feedback. To appear in Proceedings of UITP 2012 (2012)","DOI":"10.4204\/EPTCS.118.3"},{"key":"10_CR9","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. CoRR abs\/1211.7012 (2012)"},{"key":"10_CR10","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]","year":"2006","unstructured":"Kohlhase, M. (ed.): OMDoc. LNCS (LNAI), vol.\u00a04180. Springer, Heidelberg (2006)"},{"issue":"3","key":"10_CR11","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1109\/MCSE.2007.53","volume":"9","author":"F. P\u00e9rez","year":"2007","unstructured":"P\u00e9rez, F., Granger, B.E.: IPython: a System for Interactive Scientific Computing. Comput. Sci. Eng.\u00a09(3), 21\u201329 (2007)","journal-title":"Comput. Sci. Eng."},{"key":"10_CR12","unstructured":"Stein, W.A., et al.: Sage mathematics software (2009)"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-31374-5_12","volume-title":"Intelligent Computer Mathematics","author":"C. Tankink","year":"2012","unstructured":"Tankink, C., Lange, C., Urban, J.: Point-and-write \u2013 documenting formal mathematics by reference. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol.\u00a07362, pp. 169\u2013185. Springer, Heidelberg (2012)"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Hales, T.C.: Dense Sphere Packings - a blueprint for formal proofs. Cambridge University Press (2012)","DOI":"10.1017\/CBO9781139193894"},{"key":"10_CR15","unstructured":"Tankink, C., McKinna, J.: Dynamic proof pages. In: ITP Workshop on Mathematical Wikis (MathWikis). CEUR Workshop Proceedings, vol.\u00a0767 (2011)"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Tankink, C., Geuvers, H., McKinna, J., Wiedijk, F.: Proviola: A tool for proof re-animation. In: [24], pp. 440\u2013454","DOI":"10.1007\/978-3-642-14128-7_37"},{"key":"10_CR17","unstructured":"Adams, M., Aspinall, D.: Recording and refactoring HOL Light tactic proofs. In: Proceedings of the IJCAR Workshop on Automated Theory Exploration (2012)"},{"key":"10_CR18","series-title":"LNAI","first-page":"120","volume-title":"CICM 2013","author":"C. Kaliszyk","year":"2013","unstructured":"Kaliszyk, C., Urban, J.: Automated reasoning service for HOL Light. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol.\u00a07961, pp. 120\u2013135. Springer, Heidelberg (2013)"},{"issue":"2-3","key":"10_CR19","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun.\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"2-3","key":"10_CR20","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E - A Brainiac Theorem Prover. AI Commun.\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: PRocH: Proof reconstruction for HOL Light (2013)","DOI":"10.1007\/978-3-642-38574-2_18"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A wiki for Mizar: Motivation, considerations, and initial prototype. In: [24], pp. 455\u2013469","DOI":"10.1007\/978-3-642-14128-7_38"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"Intelligent Computer Mathematics","year":"2010","unstructured":"Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.): AISC 2010. LNCS, vol.\u00a06167. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39320-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,2]],"date-time":"2023-07-02T15:45:36Z","timestamp":1688312736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39320-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642393198","9783642393204"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39320-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}