What is the point of computers? A question for pure mathematicians

B. J. Birch and H. P. F. Swinnerton-Dyer, Notes on elliptic curves. II , J. Reine Angew. Math. 218

1965

Earlier work this paper cites.

Thomas Peterfalvi, Character theory for the odd order theorem , London Mathematical Society Lecture Note Series, vol. 272, Cambridge University Press, Cambridge, 2000, Translated from the 1986 French original by Robert Sandling and revised by the author. MR 1747393

1986

Earlier work this paper cites.

Thierry Coquand and Christine Paulin, Inductively defined types , COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings (Per Martin-Löf and Grigori Mints, eds.), Lecture Notes in Computer Science, vol. 417, Springer, 1988, pp. 50–66

1988

Earlier work this paper cites.

Helmut Bender and George Glauberman, Local analysis for the odd order theorem , London Mathematical Society Lecture Note Series, vol. 188, Cambridge University Press, Cambridge, 1994, With the assistance of Walter Carlip. MR 1311244

1994

Earlier work this paper cites.

Benjamin Werner, Sets in types, types in sets , Theoretical aspects of computer software (Sendai, 1997), Lecture Notes in Comput. Sci., vol. 1281, Springer, Berlin, 1997, pp. 530–546. MR 1608927

1997

Earlier work this paper cites.

Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel, Isabelle/hol - A proof assistant for higher-order logic , Lecture Notes in Computer Science, vol. 2283, Springer, 2002

2002

Earlier work this paper cites.

Benjamin Grégoire and Assia Mahboubi, Proving equalities in a commutative ring done right in Coq , Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings (Joe Hurd and Thomas F. Melham, eds.), Lecture Notes in Computer Science, vol. 3603, Springer, 2005, pp. 98–113

2005

Earlier work this paper cites.

Georges Gonthier, The four colour theorem: Engineering of a formal proof , Computer Mathematics, 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007. Revised and Invited Papers (Deepak Kapur, ed.), Lecture Notes in Computer Science, vol. 5081, Springer, 2007, p. 333

2007

Earlier work this paper cites.

Georges Gonthier, Formal proof—the four-color theorem , Notices Amer. Math. Soc. 55

2008

Earlier work this paper cites.

John Harrison, Formalizing an analytic proof of the prime number theorem , J. Automat. Reason. 43

2009

Earlier work this paper cites.

John Harrison, HOL light: An overview , Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings (Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, eds.), Lecture Notes in Computer Science, vol. 5674, Springer, 2009, pp. 60–66

2009

Earlier work this paper cites.

Adam Naumowicz and Artur Korniłowicz, A brief overview of mizar , Theorem Proving in Higher Order Logics (Berlin, Heidelberg) (Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, eds.), Springer Berlin Heidelberg, 2009, pp. 67–72

2009

Earlier work this paper cites.

Lawrence C. Paulson and Jasmin Christian Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers , The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011 (Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, eds.), EPiC Series in Computing, vol. 2, EasyChair, 2010, pp. 1–11

2010

Earlier work this paper cites.

Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry, A machine-checked proof of the odd order theorem , Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings (Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, eds.), Lecture Notes in Computer Science, vol. 7998, Springer, 2013, pp. 163–179

2013

Earlier work this paper cites.

Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, and Enrico Tassi, A computer-algebra-based formal proof of the irrationality of ζ \zeta (3) , International Conference on Interactive Theorem Proving, Springer, 2014, pp. 160–176

2014

Earlier work this paper cites.

Thomas C. Hales, Mathematics in the age of the Turing machine , Turing’s legacy: developments from Turing’s ideas in logic, Lect. Notes Log., vol. 42, Assoc. Symbol. Logic, La Jolla, CA, 2014, pp. 253–298. MR 3497663

2014

Earlier work this paper cites.

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer, The Lean theorem prover (system description) , Automated Deduction - CADE-25 (Cham) (Amy P. Felty and Aart Middeldorp, eds.), Springer International Publishing, 2015, pp. 378–388

2015

Earlier work this paper cites.

Jordan S. Ellenberg and Dion Gijswijt, On large subsets of 𝔽 q n \mathbb{F}^{n}_{q} with no three-term arithmetic progression , Ann. of Math. (2) 185

2017

Earlier work this paper cites.

Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller, A formal proof of the Kepler conjecture , Forum Math. Pi 5

2017

Earlier work this paper cites.

by same author, Etale cohomology of diamonds , https://arxiv.org/abs/1709.07343 , 2017

Original

2017

Earlier work this paper cites.

Yves Bertot, Laurence Rideau, and Laurent Théry, Distant decimals of π \pi : Formal proofs of some algorithms computing them and guarantees of exact computation , J. Autom. Reason. 61

2018

Earlier work this paper cites.

Fabian Immler, A verified ODE solver and the Lorenz attractor , Journal of automated reasoning 61

2018

Earlier work this paper cites.

The Stacks Project Authors, Stacks Project , https://stacks.math.columbia.edu , 2018

2018

Cited alongside, same era.

Zulip, The Lean community Zulip chatroom , https://leanprover.zulipchat.com , Accessed: every day since 2018

2018

Cited alongside, same era.

Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis, Formalizing the solution to the cap set problem , 10th International Conference on Interactive Theorem Proving, LIPIcs. Leibniz Int. Proc. Inform., vol. 141, Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2019, pp. Art. No. 15, 19. MR 4008934

2019

Cited alongside, same era.

by same author, Nine chapters of analytic number theory in Isabelle/HOL , 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA (John Harrison, John O’Leary, and Andrew Tolmach, eds.), LIPIcs, vol. 141, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, pp. 16:1–16:19

2019

Cited alongside, same era.

Mario Carneiro, Metamath Zero , https://github.com/digama0/mm0 , 2021

2021

Closest in time.

Davide Castelvecchi, Mathematicians welcome computer-assisted proof in ‘grand unification’ theory , https://www.nature.com/articles/d41586-021-01627-2 , Accessed: 30-11-2021

2021

Closest in time.

Johan Commelin and Robert Y. Lewis, Formalizing the ring of Witt vectors , CPP ’21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021 (Catalin Hritcu and Andrei Popescu, eds.), ACM, 2021, pp. 264–277

2021

Closest in time.

Johan Commelin and Patrick Massot, Blueprint for the Liquid Tensor Experiment , https://leanprover-community.github.io/liquid/ , Accessed: 30-11-2021

2021

Closest in time.

James Dabbs and Steven Clontz, π \pi -base , https://topology.pi-base.org/ , Accessed: 30-11-2021