{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T19:07:57Z","timestamp":1774984077936,"version":"3.50.1"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,4,1]],"date-time":"2014-04-01T00:00:00Z","timestamp":1396310400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2014,4]]},"abstract":"<jats:p>With the help of computational proof assistants, formal verification could become the new standard for rigor in mathematics.<\/jats:p>","DOI":"10.1145\/2591012","type":"journal-article","created":{"date-parts":[[2014,3,24]],"date-time":"2014-03-24T13:45:50Z","timestamp":1395668750000},"page":"66-75","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":55,"title":["Formally verified mathematics"],"prefix":"10.1145","volume":"57","author":[{"given":"Jeremy","family":"Avigad","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA"}]},{"given":"John","family":"Harrison","sequence":"additional","affiliation":[{"name":"Intel Corporation, Hillsboro, OR"}]}],"member":"320","published-online":{"date-parts":[[2014,4]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Clarendon Press","author":"Aubrey J.","year":"1898","unstructured":"Aubrey , J. Brief Lives . A. Clark , Ed. Clarendon Press , Oxford, U.K. , 1898 . Aubrey, J. Brief Lives. A. Clark, Ed. Clarendon Press, Oxford, U.K., 1898."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 20th International Colloquium on Automata, Languages and Programming (Lund, Sweden, July 5--9)","author":"Blum M.","year":"1993","unstructured":"Blum , M. Program result checking: A new approach to making programs more reliable . In Proceedings of the 20th International Colloquium on Automata, Languages and Programming (Lund, Sweden, July 5--9) , A. Lingas, R. Karlsson, and S. Carlsson, Eds. Springer , Berlin , 1993 , 1--14. Blum, M. Program result checking: A new approach to making programs more reliable. In Proceedings of the 20th International Colloquium on Automata, Languages and Programming (Lund, Sweden, July 5--9), A. Lingas, R. Karlsson, and S. Carlsson, Eds. Springer, Berlin, 1993, 1--14."},{"key":"e_1_2_1_3_1","volume-title":"Elements of Mathematics: Theory of Sets","author":"Bourbaki N.","year":"1968","unstructured":"Bourbaki , N. Elements of Mathematics: Theory of Sets . Addison-Wesley , Reading, MA , 1968 ; translated from the French Th\u00e9orie des ensembles in the series El\u00e9ments de math\u00e9matique, revised version, Hermann, Paris, 1970. Bourbaki, N. Elements of Mathematics: Theory of Sets. Addison-Wesley, Reading, MA, 1968; translated from the French Th\u00e9orie des ensembles in the series El\u00e9ments de math\u00e9matique, revised version, Hermann, Paris, 1970."},{"key":"e_1_2_1_4_1","volume-title":"\u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik 38, 1","author":"G\u00f6del K.","year":"1931","unstructured":"G\u00f6del , K. \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik 38, 1 ( 1931 ), 173--198; reprinted with English translation in Kurt G\u00f6del : Collected Works, Volume 1 , S. Feferman et al., Eds. Oxford University Press , Oxford, U.K., 1986, 144--195. G\u00f6del, K. \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik 38, 1 (1931), 173--198; reprinted with English translation in Kurt G\u00f6del: Collected Works, Volume 1, S. Feferman et al., Eds. Oxford University Press, Oxford, U.K., 1986, 144--195."},{"key":"e_1_2_1_5_1","first-page":"11","volume":"55","author":"Gonthier G.","year":"2008","unstructured":"Gonthier , G. Formal proof---The four-color theorem. Notices of the American Mathematical Society 55 , 11 ( Dec. 2008 ), 1382--1393. Gonthier, G. Formal proof---The four-color theorem. Notices of the American Mathematical Society 55, 11 (Dec. 2008), 1382--1393.","journal-title":"Notices of the American Mathematical Society"},{"key":"e_1_2_1_6_1","first-page":"213","volume":"201","author":"Grabiner J.V.","year":"1986","unstructured":"Grabiner , J.V. Is mathematical truth time-dependent? In New Directions in the Philosophy of Mathematics: An Anthology, T. Tymoczko , Ed. , Birkh\u00e4user , Boston , 1986 , 201 -- 213 . Grabiner, J.V. Is mathematical truth time-dependent? In New Directions in the Philosophy of Mathematics: An Anthology, T. Tymoczko, Ed., Birkh\u00e4user, Boston, 1986, 201--213.","journal-title":"Boston"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1090\/noti988"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139193894","volume-title":"Dense Sphere Packings: A Blueprint for Formal Proofs","author":"Hales T.","year":"2012","unstructured":"Hales , T. Dense Sphere Packings: A Blueprint for Formal Proofs . Cambridge University Press , Cambridge, U.K. , 2012 . Hales, T. Dense Sphere Packings: A Blueprint for Formal Proofs. Cambridge University Press, Cambridge, U.K., 2012."},{"key":"e_1_2_1_9_1","volume-title":"The Kepler Conjecture (unpublished manuscript)","author":"Hales T.","year":"1998","unstructured":"Hales , T. The Kepler Conjecture (unpublished manuscript) , 1998 ; http:\/\/arxiv.org\/pdf\/math\/9811078.pdf Hales, T. The Kepler Conjecture (unpublished manuscript), 1998; http:\/\/arxiv.org\/pdf\/math\/9811078.pdf"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_17"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006023127567"},{"key":"e_1_2_1_12_1","unstructured":"Hobbes T. Leviathan. Andrew Crooke London 1651. Hobbes T. Leviathan . Andrew Crooke London 1651."},{"key":"e_1_2_1_13_1","volume-title":"Theoretical mathematics': Toward a cultural synthesis of mathematics and theoretical physics. Bulletin of the American Mathematics Society (New Series) 29, 1","author":"Jaffe A.","year":"1993","unstructured":"Jaffe , A. and Quinn , F . ' Theoretical mathematics': Toward a cultural synthesis of mathematics and theoretical physics. Bulletin of the American Mathematics Society (New Series) 29, 1 ( 1993 ), 1--13. Jaffe, A. and Quinn, F. 'Theoretical mathematics': Toward a cultural synthesis of mathematics and theoretical physics. Bulletin of the American Mathematics Society (New Series) 29, 1 (1993), 1--13."},{"key":"e_1_2_1_14_1","volume-title":"Cambridge University Press","author":"Littlewood J.E.","year":"1986","unstructured":"Littlewood , J.E. Littlewood's Miscellany . Cambridge University Press , Cambridge, U.K. , 1986 . Littlewood, J.E. Littlewood's Miscellany. Cambridge University Press, Cambridge, U.K., 1986."},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4872-9","volume-title":"Mathematics: Form and Function","author":"Mac Lane S.","year":"1986","unstructured":"Mac Lane , S. Mathematics: Form and Function . Springer , New York , 1986 . Mac Lane, S. Mathematics: Form and Function. Springer, New York, 1986."},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/4529.001.0001","volume-title":"Mechanizing Proof: Computing, Risk and Trust","author":"MacKenzie D.","year":"2001","unstructured":"MacKenzie , D. Mechanizing Proof: Computing, Risk and Trust . MIT Press , Cambridge, MA , 2001 . MacKenzie, D. Mechanizing Proof: Computing, Risk and Trust. MIT Press, Cambridge, MA, 2001."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005843212881"},{"key":"e_1_2_1_18_1","first-page":"7","volume":"55","author":"Nathanson M.","year":"2008","unstructured":"Nathanson , M. Desperately seeking mathematical truth. Notices of the American Mathematical Society 55 , 7 ( Aug. 2008 ), 773. Nathanson, M. Desperately seeking mathematical truth. Notices of the American Mathematical Society 55, 7 (Aug. 2008), 773.","journal-title":"Notices of the American Mathematical Society"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_4"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-003-0387-5"},{"key":"e_1_2_1_21_1","volume-title":"Zur Modernisierung des Studiums der Mathematik in Berlin","author":"Schubring G.","year":"1820","unstructured":"Schubring , G. Zur Modernisierung des Studiums der Mathematik in Berlin , 1820 --1840. In Amphora : Festschrift f\u00fcr Hans Wussing Zu Seinem 65. Geburtstag, S.S.Demidov et al., Eds. Birkh\u00e4user , Basel, 1992, 649--675. Schubring, G. Zur Modernisierung des Studiums der Mathematik in Berlin, 1820--1840. In Amphora: Festschrift f\u00fcr Hans Wussing Zu Seinem 65. Geburtstag, S.S.Demidov et al., Eds. Birkh\u00e4user, Basel, 1992, 649--675."},{"key":"e_1_2_1_23_1","volume-title":"On proof and progress in mathematics. Bulletin of the American Mathematical Society (New Series) 30, 2","author":"Thurston W.P.","year":"1994","unstructured":"Thurston , W.P. On proof and progress in mathematics. Bulletin of the American Mathematical Society (New Series) 30, 2 ( 1994 ), 161--177. Thurston, W.P. On proof and progress in mathematics. Bulletin of the American Mathematical Society (New Series) 30, 2 (1994), 161--177."},{"key":"e_1_2_1_24_1","volume-title":"Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Univalent Foundations Program","year":"2013","unstructured":"Univalent Foundations Program , Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations of Mathematics . Princeton, NJ , 2013 ; https:\/\/github.com\/HoTT\/book Univalent Foundations Program, Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton, NJ, 2013; https:\/\/github.com\/HoTT\/book"},{"key":"e_1_2_1_25_1","volume-title":"The de Bruijn Factor (unpublished manuscript)","author":"Wiedijk F.","year":"2000","unstructured":"Wiedijk , F. The de Bruijn Factor (unpublished manuscript) , 2000 ; http:\/\/www.cs.ru.nl\/~freek\/factor\/ Wiedijk, F. The de Bruijn Factor (unpublished manuscript), 2000; http:\/\/www.cs.ru.nl\/~freek\/factor\/"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/2168152"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2591012","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2591012","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:01:13Z","timestamp":1750276873000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2591012"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["10.1145\/2591012"],"URL":"https:\/\/doi.org\/10.1145\/2591012","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4]]},"assertion":[{"value":"2014-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}