Book contents
- Frontmatter
- Contents
- Turing's legacy: developments from Turing's ideas in logic
- Computability and analysis: the legacy of Alan Turing
- Alan Turing and the other theory of computation (expanded)
- Turing in Quantumland
- Computability theory, algorithmic randomness and Turing's anticipation
- Computable model theory
- Towards common-sense reasoning via conditional simulation: legacies of Turing in Artificial Intelligence
- Mathematics in the age of the Turing machine
- Turing and the development of computational complexity
- Turing machines to word problems
- Musings on Turing's Thesis
- Higher generalizations of the Turing Model
- Step by recursive step: Church's analysis of effective calculability
- Turing and the discovery of computability
- Transfinite machine models
- References
Mathematics in the age of the Turing machine
Published online by Cambridge University Press: 05 June 2014
Edited by
Book contents
- Frontmatter
- Contents
- Turing's legacy: developments from Turing's ideas in logic
- Computability and analysis: the legacy of Alan Turing
- Alan Turing and the other theory of computation (expanded)
- Turing in Quantumland
- Computability theory, algorithmic randomness and Turing's anticipation
- Computable model theory
- Towards common-sense reasoning via conditional simulation: legacies of Turing in Artificial Intelligence
- Mathematics in the age of the Turing machine
- Turing and the development of computational complexity
- Turing machines to word problems
- Musings on Turing's Thesis
- Higher generalizations of the Turing Model
- Step by recursive step: Church's analysis of effective calculability
- Turing and the discovery of computability
- Transfinite machine models
- References
Summary
“And when it comes to mathematics, you must realize that this is the human mind at the extreme limit of its capacity.”
(H. Robbins)“ … so reduce the use of the brain and calculate!”
(E. W. Dijkstra)“The fact that a brain can do it seems to suggest that the difficulties [of trying with a machine] may not really be so bad as they now seem.”
(A. Turing)§1. Computer calculation.
1.1. A panorama of the status quo. Where stands the mathematical endeavor?
In 2012, many mathematical utilities are reaching consolidation. It is an age of large aggregates and large repositories of mathematics: the arXiv, Math Reviews, and euDML, which promises to aggregate the many European archives such as Zentralblatt Math and Numdam. Sage aggregates dozens of mathematically oriented computer programs under a single Python-scripted front-end.
Book sales in the U.S. have been dropping for the past several years. Instead, online sources such as Wikipedia and Math Overflow are rapidly becoming students' preferred math references. The Polymath blog organizes massive mathematical collaborations. Other blogs organize previously isolated researchers into new fields of research. The slow, methodical deliberations of referees in the old school are giving way; now in a single stroke, Tao blogs, gets feedback, and publishes.
Machine Learning is in its ascendancy. Log Answer and Wolfram Alpha answer our elementary questions about the quantitative world; Watson our Jeopardy questions.
- Type
- Chapter
- Information
- Turing's LegacyDevelopments from Turing's Ideas in Logic, pp. 253 - 298Publisher: Cambridge University PressPrint publication year: 2014
References
[Aga13] http://en.wikipedia.org/wiki/Lorenz-attractor, accessed 2013.
[Ada07] , Atlas of Lie groups and representations, MIT colloquium slides, http://atlas.math.umd.edu/talks/boston.pdf, 2007.
[Ada11] , Computing global characters, http://www.liegroups.org/papers/characters.pdf, 2011.
[Ada09] , Importing proofs into HOL Zero, private communication, 2009.
[AHK77] , , and , Every planar map is four colorable, Illinois Journal of Mathematics, vol. 21 (1977), pp. 439-567.Google Scholar
[AriBC] Aristotle, On the heavens, http://classics.mit.edu/Aristotle/heavens.html, 350BC, translated by .
[AS92] and , The uniqueness of groups of Lyons type, Journal of the American Mathematical Society, vol. 5 (1992), no. 1, pp. 75-98.Google Scholar
[At1] Atlas of Lie groups and representations, http://www.liegroups.org/.
[Aus08] , On the roles of proof in mathematics, Proof and other dilemmas ( and , editors), Mathematical Association of America, 2008.
[AW09] and , Homotopy theoretic models of identity types, Mathematical Proceedings of the Cambridge Philosophical Society, vol. 146 (2009), no. 1, pp. 45-55.Google Scholar
[BV08] and , New upper bounds for kissing numbers from semidefinite programming, Journal of the American Mathematical Society, vol. 21 (2008), pp. 909-924.Google Scholar
[Bar07] , Foundations of mathematics from the perspective of computer verification, Mathematics, computer science, logic—a never ending story, Springer-Verlag, 2007.
[Bar98] , Verification of the interface of a small proof system in Coq, Types for proofs andprograms, Lecture Notes in Computer Science, vol. 1512, 1998, pp. 28-45.Google Scholar
[Bee85] , Foundations of constructive mathematics: metamathematical studies, Springer-Verlag, 1985.
[BG94] and , Local analysis for the odd order theorem, LMS, vol. 188, Cambridge University Press, 1994.
[Ber05] , Nationale Onderzoeksagenda Informatie en Communicatietechnologie (NOAG-ict) 2005–2010, Albani drukkers, Den Haag, 2005.
[BC04] and , Interactive theorem proving and program development Coq'Art: The calculus of inductive constructions, Springer-Verlag, 2004.
[BGBP08] , , , and , Canonical big operators, Theorem provingin higher order logics, Lecture Notes in Computer Science, vol. 5170, Springer-Verlag, 2008, pp. 86-101.
[Bet91] , The approximation problem for Sobolev maps between two manifolds, Acta Mathematica, vol. 167 (1991), no. 3–4, pp. 153-206.Google Scholar
[BH00] and , Densest lattice packings of 3-polytopes, Computational Geometry, vol. 16 (2000), pp. 157-186.Google Scholar
[BS10] and , Ternary cubic forms having bounded invariants, and the existence of a positive proportion of elliptic curves having rank 0, http://arxiv.org/abs/1007. 0052v1 [math.NT], 2010.
[Bir02] , In lieu of birthday greetings, Number theory and algebraic geometry, Cambridge Univ. Press, 2002, pp. 1-30.
[BSD65] and , Notes on elliptic curves, II, Journal für die Reine und Angewandte Mathematik, vol. 218 (1965), pp. 79-108.Google Scholar
[BN10] and , Sledgehammer: Judgement day, Automated reasoning (iJCAR 2010) ( and , editors), Lecture Notes in Computer Science, vol. 6173, Springer-Verlag, 2010, pp. 107-121.
[Bor09] , A geometric approach to the two-dimensional Jacobian conjecture, http://arxiv.org/abs/0912.4803, 2009.
[BG11] and , Did a 1-dimensional magnet detect a 248-dimensional Lie algebra?, Notices of the American Mathematical Society, vol. 58 (2011), no. 8, pp. 1055-1066.Google Scholar
[Boy90] , Soap bubbles, (Dover reprint), 1890.
[Car07] , La conjecture de Sato-Tate [d'après Clozel, Harris, Shepherd-Barron, Taylor], Séminaire Bourbaki, vol. 59 (2006–2007), pp. 345-391.Google Scholar
[CES11] , , and , A generative geometric kernel, Proceedings of the 20th ACM SIGPLAN workshop on partial evaluation and program manipulation, PEPM '11, 2011, pp. 53-62.
[CC11] 10 best jobs 2011, http://www.careercast.com/jobs-rated/10-best-jobs-2011
[CEG10] , , and , Dense crystalline dimer packings of regular tetrahedra, Discrete & Computational Geometry, vol. 44 (2010), pp. 253-280, http://arxiv.org/abs/1001.0586.Google Scholar
[CT06] and , Packing, tiling, and covering with tetrahedra, Proceedings of the National Academy of Sciences, vol. 103 (July 11, 2006), no. 28, pp. 10612-10617.Google Scholar
[Cor10] , On the history of Fermat's last theorem: fresh views on an old tale, Mathematische Semesterberichte, vol. 57 (2010), no. 1, pp. 123-138.Google Scholar
[Dav09] , A self-verifying theorem prover, Ph.D. thesis, University of Texas at Austin, 2009.
[Dij82] , On the role of scientific thought, Edsger W. Dijkstra: Selected writings on computing: A personal perspective, Springer-Verlag, 1982, http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD447.PDF.
[DCF+62] , , , , and , Manual for authors of mathematical papers, vol. 68, 1962.
[Doy11] and , http://arxiv.org/abs/cond-mat/9709201, accessed 2011.
[Elk88] , On A4 + B4 + C4 = D4, Mathematics of Computation, vol. 51 (1988), no. 184, pp. 825-835.Google Scholar
[Fey85] , QED: the strange theory of light and matter, Princeton University Press, 1985.
[Fey00] , Selected papers of Richard Feynman, World Scientific, 2000.
[For09] , The status of the P versus NP problem, Communications of the ACM, vol. 52 (2009), no. 9, pp. 78-86.Google Scholar
[Fox03] , Formal specification and verification of ARM6, Theorem proving in higher order logics, Lecture Notes in Computer Science, vol. 2758, Springer-Verlag, 2003, pp. 25-40.
[Gab10] , Hyperbolic 3-manifolds in the 2000's, Proceedings of the International Congress of Mathematicians, 2010.
[GMT03] , , and , Homotopy hyperbolic 3-manifolds are hyperbolic, Annals of Mathematics, vol. 157 (2003), pp. 335-431.Google Scholar
[Gan09] , The language of mathematics, Ph.D. thesis, Cambridge University, 2009, http://people.pwf.cam.ac.uk/mg262/GanesalingamMdis.pdf.
[Gan10] , The language of mathematics, slides, http://www.srcf.ucam.org/principia/files/ganesalingam.pdf, 2010.
[GGMR09] , , , and , Packaging mathematical structures, Theorem proving in higher order logics, Lecture Notes in Computer Science, vol. 5674, Springer-Verlag, 2009, pp. 327-342.
[Gon08] , Formal proof—the four colour theorem, Notices of the American Mathematical Society, vol. 55 (December 2008), no. 11, pp. 1382-1393.Google Scholar
[Gon11] , Point-free, set-free concrete linear algebra, Interactive theorem proving, Lecture Notes in Computer Science, vol. 6898, Springer-Verlag, 2011, pp. 103-118.
[Gon12] , http://www.msr-inria.inria.fr/events-news/feit-thompson-proved-in-coq, 2012.
[GM11] and , An introduction to small scale reflection in Coq, http://hal.inria.fr/inria-00515548/, 2011.
[GMR07] , , and , A modular formalisation of finite group theory, Theorem proving in higher order logics, Lecture Notes in Computer Science, vol. 4732, Springer-Verlag, 2007, pp. 86-101.
[GMT11] , , and , A small scale reflection extension for the Coq system, http://hal.archives-ouvertes.fr/inria-00258384/, 2011.
[Gor00] , From LCF to HOL: a short history, Proof, language, and interaction: essays in honour of Robin Milner, MIT, 2000, pp. 169-185.
[Gru11] , An enduring error, The best writing on mathematics 2010 (, editor), Princeton University Press, 2011.
[Ha105a] , The Flyspeck project, Dagstuhl seminar proceedings ( and , editors), vol. 25, IBFI, 2005, pp. 489-507.
[Hal05b] , A proof of the Kepler conjecture, Annals of Mathematics, vol. 162 (2005), pp. 1065-1185.Google Scholar
[Hal08] , Formal proof, Notices of the American Mathematical Society, vol. 55 (December 2008), no. 11, pp. 1370-1380.Google Scholar
[Hal11] , On the Reinhardt conjecture, http://arxiv.org/abs/1103.4518, 2011.
[Ham08] , KNOPPIX/math: A live system for enjoying mathematics with computer, ACM Communications in Computer Algebra, vol. 42 (2008), no. 3, pp. 175-176, http://www. knoppix-math.org/.Google Scholar
[HL03] and , Topology of Sobolev mappings. II, Acta Mathematica, vol. 191 (2003), no. 1, pp. 55-107.Google Scholar
[Har96] , Optimizing proof search in model elimination, Proceedings of the 13th international Conference on Automated Deduction (CADE-13), Lecture Notes in Computer Science, vol. 1104, Springer-Verlag, 1996, pp. 313-327.
[Har06] , Towards self-verification of HOL light, Proceedings of IJCAR 2006, Lecture Notes in Computer Science, vol. 4130, Springer-Verlag, 2006, pp. 177-191.
[Har08] , Formal proof—theory and practice, Notices of the American Mathematical Society, vol. 55 (December 2008), no. 11, pp. 1395-1406.Google Scholar
[Har09] , Handbook of practical logic and automated reasoning, Cambridge University Press, 2009.
[Har10] , On the cruelty of really doing formal proofs, www.srcf.ucam.org/principia/files/jrhslides.pdf, 2010, Principia Mathematica anniversary symposium.
[HHS95] , , and , The double bubble conjecture, Electronic Research Announcements of the American Mathematical Society, vol. 1 (1995), no. 3.Google Scholar
[HS99] and , A presentation for the Lyons simple group, http://dimacs.rutgers.edu/~havas/TR0416.pdf, 1999.
[Hoe11] , Towards semantic mathematical editing, http://hal.archives-ouvertes.fr/hal-00569351/fr/, 2011.Google Scholar
[Hof87] , The computer-aided discovery of new embedded minimal surfaces, The Mathematical Intelligencer, vol. 9 (1987), no. 3, pp. 8-81.Google Scholar
[Hor10] , Projective plane of order 12, http://mathoverflow.net/questions/38632/projective-plane-of-order-12, 2010, Math Overflow.
[HTT11] Homotopy type theory, http://homotopytypetheory.org/, 2011.
[HT00] and , The pragmatic programmer, Addison Wesley, 2000.
[HMRR00] , , , and , Proof of the double bubble conjecture, Electronic Research Announcements of the American Mathematical Society, vol. 6 (2000), pp. 45-49.Google Scholar
[IR11] and , Formalizing foundations of mathematics, Mathematical Structures in Computer Science, vol. 21 (2011), no. 4, pp. 883-911.Google Scholar
[Ima13] Wellcome Images, http://images.wellcome.ac.uk, London, accessed 2013.
[KW07] and , Certified computer algebra on top of an interactive theorem prover, Proceedings of the 14th symposium on the integration of symbolic computation andmech-anised reasoning (Calculemus'07) (, , , and , editors), Lecture Notesin Computer Science, vol. 4573, Springer-Verlag, 2007, http://sco1re.cs.tsukuba.ac.jp/~kaliszyk/docs/kaliszyk-p04-calc.pdf, pp. 94-105.
[KLV12a] , , and , The simplicial model of univalent foundations, http://arxiv.org/abs/1211.2851, 2012.
[KLV12b] , Univalence in simplicial sets, http://arxiv.org/abs/1203.2553, 2012.
[KLS08] , , and , Functoriality and the inverse Galois problem, Compositio Mathematica, vol. 144(2008), pp. 541-564.Google Scholar
[KAE+10] , , , , , , , , , , , , and , seL4: Formal verification of an operating-system kernel, Communications of the ACM, vol. 53 (2010), no. 6, pp. 107-115.Google Scholar
[Kur99] , The age of spiritual machines, Penguin, 1999.
[Lam91] , The search for a finite projective plane of order 10, American Mathematical Monthly, vol. 98 (1991), no. 4, pp. 305-318.Google Scholar
[LTS89] , , and , The non-existence of finite projective planes of order 10, Canadian Journal of Mathematics, vol. 41 (1989), no. 6, pp. 1117-1123.Google Scholar
[LP66] and , Counterexample to Euler's conjecture on sums of like powers, American Mathematical Society. Bulletin, (1966), p. 1079.
[LSW01] , , and , The dimension of the planar Brownian frontier is 4/3, Mathematical Research Letters, vol. 8 (2001), pp. 401-411, http://www. mrlonline.org/mrl/2001-008-004/2001-008-004-001.pdf.Google Scholar
[Lax82] , Report of the panel on large scale computing in science and engineering, www.pnl.gov/scales/docs/lax_report1982.pdf, 1982.
[Ler06] , Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, 33rd acm symposium on Principles of Programming Languages, ACM Press, 2006, http://compcert.inria.fr/, pp. 42-54.
[Lev95] , Making waves: A guide to the ideas behind “outside in”, AK Peters, 1995, extract at http://www.math.sunysb.edu/CDproject/OvUM/cool-links/www.geom.umn.edu/docs/outreach/oi/history.html.
[LMM94] , , and , Outside in, AK Peters, 1994, video, The Geometry Center (also on You Tube).
[LH11] and , Canonicity for 2-dimensional type theory, preprint 2011, http://www.cs.cmu.edu/~drl/pubs/1h112tt/1h112tt.pdf.
[Lor63] , Deterministic nonperiodic flow, Journal of the Atmospheric Sciences, vol. 20 (1963), no. 2, pp. 130-141.Google Scholar
[Mac01] , Mechanizing proof, MIT Press, Cambridge, MA, 2001.
[MST73] , , and , On the existence of a projective plane of order 10, Journal of Combinatorial Theory. Series A, vol. 14 (1973), pp. 66-78.Google Scholar
[MM99] and Matzat, Inverse Galois theory, Springer-Verlag, 1999.
[Man82] , The fractal geometry of nature, Freeman and Co., 1982.
[Man04] , A theory of roughness, http://www.edge.org/3rd_culture/mandelbrot04/mandelbrot04-index.html, 2004.
[MW04] and , Soft errors' impact on system reliability, EDN, (Sept. 30, 2004).
[MC02] and , A computer-free construction of the Lyons group, to appear, http://www.math.msu.edu/~meier/Preprints/Ly/ly.pdf, 2002.
[Met] Metis, http://www.gilith.com/software/metis/index.html.
[Met03] , Catalan's conjecture: another old Diophantine problem solved, American Mathematical Society. Bulletin, vol. 41 (2003), no. 1, pp. 43-57.Google Scholar
[Mih04] , Primary cyclotomic units and a proof of Catalan's conjecture, Journal für die Reine und Angewandte Mathematik, vol. 572 (2004), pp. 167-195.Google Scholar
[Mul11] , On P vs. NP, and geometric complexity theory, Journal of the ACM, vol. 58 (April 2011), no. 2.Google Scholar
[MT10] and , The strong thirteen spheres problem, preprint http://arxiv.org/abs/1002.1439, February 2010.
[NYT10] Lone $4.1 billion sale led to [flash crash] in May, New York Timeshttp://www. nytimes.com/2010/10/02/business/02flash.html, October 10 2010.
[Op111] http://new.math.uiuc.edu/optiverse/images.html, accessed 2011.
[Ove09] Most interesting mathematics mistake?, http://mathoverflow.net/questions/879, 2009.
[Ove10] Widely accepted mathematical results that were later shown wrong?, http://mathover flow.net/questions/35468, 2010.
[Pas07] , The syntax andsemantics of the For The language, http://nevidal.org/download/forthel.pdf, 2007.
[Pau94] , Short and easy computer proofs of the Rogers–Ramanujan identities and of identities of similar type, Electronic Journal of Combinatorics, vol. 1 (1994), pp. 1-9.Google Scholar
[Pau10] , Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers, 2010, PAAR-2010, Practical Aspects of Automated Reasoning.
[PSST08] , , , and , The annual SUMO reasoning prizesat CASC, First international workshop on Practical Aspects of Automated Reasoning, CEUR Workshop Proceedings, vol. 373, 2008.Google Scholar
[PW12] and , Homotopy type theory and Voevodsky's univalent foundations, http://arxiv.org/abs/1210.5658, 2012.
[Pet00] , Character theory for the odd order theorem, LMS, vol. 272, Cambridge University Press, 2000.
[PWZ96] , , and , A = B, A. K. Peters, 1996.
[PZ04] and , Kissing numbers, sphere packings, and some unexpected proofs, Notices of the American Mathematical Society, (2004), pp. 873-883.
[Phi66] , Turning a surface inside out, Scientific American, (1966), pp. 112-120.
[PS08] and , Using automated theorem provers in nonassociative algebra, http://www.karlin.mff.cuni.cz/stanovsk/math/lpar08.pdf, 2008.
[Pit11] (editor), The best writing on mathematics 2010, Princeton Univ. Press, 2011, forward by .
[Poi92] , Les méthodes nouvelles de la mécanique céleste, Dover reprint, 1892.
[Poi52] , Science and hypothesis, Dover reprint, 1952.
[PW11] http://it.wikipedia.org/wiki/File:Foam_-_Weaire-Phelan-structure.png, accessed 2011.
[RhD11] http://upload.wikimedia.org/wikipedia/commons/8/86/Rhombic-dodeca hedra.jpg, accessed 2011.
[RSST97] , , , and , The four-colour theorem, Journal of Combinatorial Theory, Series B, vol. 70 (1997), pp. 2-44.Google Scholar
[San12] , http://www.flickr.com/photos/arenamontanus/8059864268/, accessed 2012.
[SN63] and , unpublished data, April 3, 1963.
[Sch] , The Sato–Tate conjecture, www.math.ou.edu/~rschmidt/satotate/page5.html.
[Sci11] The $23 million textbook, Science, vol. 332 (2011), pp. 647-648.
[SEC10] Findings regarding the market events of May 6, 2010, http://sec.gov/news/studies/2010/marketevents-report.pdf, September 10, 2010, Report of the Staffs of the Cftc and Sec to the Joint Advisory Committee on Emerging Regulatory Issues.
[Ser68] , Abelian l-adic representations and elliptic curves, WA Benjamin, 1968.
[Sma98] , Mathematical problems for the next century, The Mathematical Intelligencer, vol. 20 (1998), no. 2, pp. 7-15.Google Scholar
[SvdW11] and , Type classes for mathematics in type theory, http://arxiv.org/abs/1102.1323, 2011.
[Sta07] , Sequence A129935 in the on-line encyclopedia of integer sequences, published electronically at http://oeis.org/A129935, 2007.
[Ste41] , Über Maximum und Minimum bei den Figuren in der Ebene, auf der Kugelfläche und in Raume überhaupt, Comptes Rendu de l'Académie des Sciences. Paris, vol. 12 (1841), pp. 177-308.Google Scholar
[SFL] , , and , The Optiverse, video http://new.math.uiuc.edu/optiverse/ or YouTube.
[Tez04] Tezzaron semiconductor, http://www.tezzaron.com/about/papers/soft-errors-1-1-secure.pdf, 2004.
[Tsi13] , http://en.wikipedia.org/wiki/File:Double-bubble.png, accessed 2013.
[Tuc02] , A rigorous ODE solver and Smale's 14th problem, Foundations of Computational Mathematics, vol. 2 (2002), pp. 53-117.Google Scholar
[Urb07] , MaLARea: A metasystem for automated reasoning in large theories, Proceedings of the CADE-21 workshop on empirically successful automated reasoning in large theories (, , and , editors), 2007, pp. 45-58.
[Voe11] , Univalent foundations, http://hottheory.files.wordpress.com/2011/06/report-11_2011.pdf, 2011, Mathematisches Forschungsinstitut Oberwolfach, pp. 7-9.
[Vog07] , The character table for E8, Notices of the American Mathematical Society, vol. 54 (2007), no. 9, pp. 1022-1034.Google Scholar
[WW11] and , About the cover: early images of minimal surfaces, American Mathematical Society. Bulletin, vol. 48 (2011), no. 3, pp. 457-460.Google Scholar
[Wie06] (editor), The seventeen provers of the world, Lecture Notes in Artificial Intelligence, Springer-Verlag, 2006.
[Wie08] , Formal proof—getting started, Notices of the American Mathematical Society, vol. 55 (December 2008), no. 11, pp. 1408-1414.Google Scholar
[Wie10a] , Pollack inconsistency, 9th international workshop on user interfaces for theorem provers ( and , editors), ENTCS, 2010.
[Wie10b] , The next generation of proof assistants, http://www.cs.ru.nl/F.Wiedijk/talks/lsfa.ps.gz, slides, 2010.
[Wik11] List of published incomplete proofs, http://en.wikipedia.org/wiki/List_of-published-incomplete-proofs, accessed 9/2011.
[Wi102] , Four colors suffice: How the map problem was solved, Princeton University Press, 2002.
[Wo102] , A new kind of science, Wolfram Media, 2002, http://www.wolfram science.com/reference/notes/971c.
- 4
- Cited by