Skip to main content
SpringerLink
Log in
Book cover

Algorithms and Complexity in Mathematics, Epistemology, and Science pp 81–132Cite as

Proof Verification Technology and Elementary Physics

  • Conference paper
  • First Online:

  • 493 Accesses

Part of the book series: Fields Institute Communications ((FIC,volume 82))

Abstract

Software technology that can be used to validate the logical correctness of mathematical proofs has attained a high degree of power and sophistication; extremely difficult and complex mathematical theorems have been verified. This paper discusses the prospects of doing something comparable for elementary physics: what it would mean, the challenges that would have to be overcome; and the potential impact, both practical and theoretical.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD   109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    I do not know to what extent the experts agree on which, if any, kinds of theorems lie outside generalizations (1) and (2). As far as I know, there is essentially universal agreement that (1) and (2) are valid across most subfields in mathematics. Whether set theory is the best foundation for mathematics, or whether it is important for mathematics to have foundations at all, are separate questions.

  2. 2.

    This does not, of course, imply that it required ninety man-years of work.

  3. 3.

    Technically speaking, the operator Until here can be viewed as “syntactic sugar”, or as a temporal modal operator, or, if one performs some “representational tinkering” on the arguments, as a first-order predicate.

  4. 4.

    The “Monty Hall” problem is even trickier, and has tripped up professional mathematicians.

  5. 5.

    You may argue that because of noise, the theory does not correspond to a lower-dimensional manifold, it corresponds to a probability distribution centered on the manifold. That hardly helps, because now the probability distribution of the projection onto the manifold depends strongly on largely arbitrary assumptions about the noise.

  6. 6.

    The Lagrangian for the Standard Model, given in full in [33], is 36 lines long and has something like 170 terms and 1000 symbols. However, Gutierrez does claim that he has printed tee shirts with the whole thing.

  7. 7.

    Large levels of trust are needed in any such enterprise. That is why conspiracy theorists, who are willing to distrust any evidence that runs against their theory, are so crazy and so unanswerable; and why any violation of trust—by scientists, by technologists, by the media—is so damaging, not just to the specific instance, but to the entire scientific/technological enterprise.

  8. 8.

    Hendry [41] similarly argues that molecular structures cannot be calculated from Schrödinger’s equation. Rather, given the structure, it is possible to use quantum mechanics to calculate various physical values.

  9. 9.

    Incidentally, the fact that Hilbert included this problem and spent a great deal of time working on it tells strongly against the common idea that Hilbert was a pure formalist, who viewed the meaning of mathematical symbols as unimportant [12].

  10. 10.

    It has been suggested to me that it will be easier to find a logical formulation of the “many-worlds” interpretation of quantum mechanics or, alternatively, the theory of quantum decoherence than the Copenhagen interpretation. That may be so; but I can’t find that anyone has produced a logical formulation of either of these interpretations either.

  11. 11.

    Slemrod [77] writes, “Historically a canonical interpretation of this ‘6th problem of Hilbert’ has been taken to mean passage from the kinetic Boltzmann equation for a rarefied gas to the continuum Euler equations of compressible gas dynamics as the Knudsen number 𝜖 approaches zero.” I do not know what is the basis for this rather narrow interpretation.

  12. 12.

    I am necessarily relying here on the fact that I have failed to find much later work of this flavor, which is obviously an unreliable argument. However, I do have the following concrete evidence. The International Congress of Logic, Methodology, and Philosophy of Science was in some respects the successor to the Symposium on the Axiomatic Method; it has met 15 times since its inception in 1960. Between 1960 and 1999 there was only one paper [66] that presented an axiomatization of any physical theory (relativistic space-time), though there was a second paper [60] that argued in favor of axiomatizations.

  13. 13.

    In fact, despite its popularity as an philosophical example since Frege, there is little evidence that anyone who was aware of the existence of the planets has ever thought that Phosphorus and Hesperus were two different planets.

  14. 14.

    Hossenfelder [45] argues that the fetishizing of mathematical elegance is responsible for the stagnation of fundamental physics over the last few decades.

References

  1. Appel K, Haken W (1977) The solution of the four-color-map problem. Sci Am 237(4):108–121

    Article  MathSciNet  Google Scholar 

  2. Avigad J, Donnelly K, Gray D, Raff P (2007) A formally verified proof of the prime number theorem. ACM Trans Comput Log 9(1):1–23

    Article  MathSciNet  Google Scholar 

  3. Bailey DH, Borwein J (2015) Experimental computation as an ontological game changer: the impact of modern mathematical computation tools on the ontology of mathematics. In: Davis E, Davis P (eds) Mathematics, substance and surmise: views on the meaning and ontology of mathematics. Springer, Cham

    Google Scholar 

  4. Beech M (2014) the pendulum paradigm: Variations on a theme and the measure of heaven and earth. Brown Walker Press, Boca Raton

    Google Scholar 

  5. Berger M (2010) Geometry revealed: a Jacob’s ladder to modern higher geometry. Springer, Berlin

    Book  Google Scholar 

  6. Bhaskar R (1979) Realism in the natural sciences. In: Proceedings of the sixth international congress of logic, methodology and philosophy of science

    Google Scholar 

  7. Bobrow D (ed) (1985) Qualitative reasoning about physical systems. MIT Press, Cambridge

    Google Scholar 

  8. Boender J, Kammüller F, Nagarajan R (2015) Formalization of quantum protocols using Coq. In: Huenen C, Selinger P, Vicary J (eds) 12th international workshop on quantum physics and logic, pp 71–83.

    Article  MathSciNet  Google Scholar 

  9. Bridewell W, Langley P (2010) Two kinds of knowledge in scientific discovery. Top Cogn Sci 2:36–52

    Article  Google Scholar 

  10. Bundy A, Byrd L, Luger G, Mellish C, Palmer M (1979) Solving mechanics problems using meta-level inference. In: IJCAI-79, pp 1017–1027

    Google Scholar 

  11. Cappellaro P (2012) Quantum theory of radiation interaction. MIT OpenCourseware. https://ocw.mit.edu/courses/nuclear-engineering/22-51-quantum-theory-of-radiation-interactions-fall-2012/lecture-notes/

    Google Scholar 

  12. Corry L (2004) David Hilbert and the axiomatization of physics (1898–1918): from Grundlagen der Geometrie to Grundlagen der Physik. Kluwer, Dordrecht

    Book  Google Scholar 

  13. Davis E (1988) A logical framework for commonsense predictions of solid object behavior. AI Eng 3(3):125–140

    Google Scholar 

  14. Davis E (1993) The kinematics of cutting solid objects. Ann Math Artif Intell 9(3–4):253–305

    Article  Google Scholar 

  15. Davis PJ (1993) Visual theorems. Educ Stud Math 24(4):333–344

    Article  Google Scholar 

  16. Davis E (2008) Physical reasoning. In: van Harmelen F, Lifschitz V, Porter B (eds) The handbook of knowledge engineering. Elsevier, Amsterdam, pp 597–620

    Google Scholar 

  17. Davis E (2008) Pouring liquids: a study in commonsense physical reasoning. Artif Intell 172:1540–1578

    Article  MathSciNet  Google Scholar 

  18. Davis E (2011) How does a box work? a study in the qualitative dynamics of solid objects. Artif Intell 175:299–345

    Article  MathSciNet  Google Scholar 

  19. Davis E (2017) Logical formalizations of commonsense reasoning: a survey. J Artif Intell Res 59:651–723

    Article  MathSciNet  Google Scholar 

  20. Davis E (in preparation) The logic of coal, iron, air, and water: representing common sense and elementary science

    Google Scholar 

  21. Davis E, Marcus G (2014) The scope and limits of simulation in cognition. https://arxiv.org/abs/1506.04956

  22. Davis E, Marcus G (2016) The scope and limits of simulation in automated reasoning. Artif Intell 233:60–72

    Article  MathSciNet  Google Scholar 

  23. Davis E, Marcus G, Frazier-Logue N (2017) Commonsense reasoning about containers using radically incomplete information. Artif Intell 248:46–84

    Article  MathSciNet  Google Scholar 

  24. Dehaene S (1997) The number sense: how the mind creates mathematics. Oxford University Press, Oxford

    MATH  Google Scholar 

  25. de Kleer J, Brown JS (1985) A qualitative physics based on confluences. In: Bobrow D (ed) Qualitative reasoning about physical systems. MIT Press, Cambridge

    Google Scholar 

  26. Domingos P (2015) The master algorithm: how the quest for the ultimate learning machine will remake our world. Basic Books, New York

    Google Scholar 

  27. Dwyer J, Uman MA (2013) The physics of lightning. Phys Rep 534:147–241. https://doi.org/10.1016/j.physrep.2013.09.004

    Article  MathSciNet  Google Scholar 

  28. Feynman R, Leighton RB, Sands M (1964) The Feynman lectures on physics. Addison-Wesley, Boston

    Book  Google Scholar 

  29. Friedman S, Forbus K, Sherin B (2017) Representing, running, and revising mental models: a computational model. Cogn Sci 42(2):1–36

    Google Scholar 

  30. Gonthier G et al (2013) A machine-checked proof of the odd order theorem. In: International conference on interactive theorem proving (Lecture notes in computer science), vol 7998. Springer, Berlin, pp 163–179.

    Chapter  Google Scholar 

  31. Gopnik A (2012) Scientific thinking in young children: theoretical advances, empirical research, and policy implications. Science 337(6102):1623–1627

    Article  Google Scholar 

  32. Gunning D et al (2010) Project Halo update—progress toward Digital Aristotle. AI Mag 31(3):33–58

    Article  Google Scholar 

  33. Gutierrez TD (1999) Standard model lagrangian. http://nuclear.ucdavis.edu/~tgutierr/files/stmL1.html

  34. Hales T et al (2015) A formal proof of the Kepler conjecture. http://arxiv.org/abs/1501.02155

  35. Hamel GKW (1912) Elementare Mechanik. Teubner, Leipzig

    MATH  Google Scholar 

  36. Hamel GKW (1921) Grundbegriffe der Mechanik. Teubner, Leipzig

    MATH  Google Scholar 

  37. Harrison J (2006) Formal verification of floating point trigonometric functions. In: International conference on formal methods in computer-aided design, pp 254–270

    Google Scholar 

  38. Harrison J (2009) Formalizing an analytic proof of the prime number theorem. J Autom Reason 43(3):243–261

    Article  MathSciNet  Google Scholar 

  39. Hayes P (1979) The naïve physics manifesto. In: Michie D (ed) Expert systems in the micro-electronic age. Edinburgh University Press, Edinburgh

    Google Scholar 

  40. Hayes P (1985) Ontology for liquids. In: Hobbs J, Moore R (eds) Formal theories of the commonsense world. Ablex Publishing, New York

    Google Scholar 

  41. Hendry RF (1999) Chemistry and the completeness of physics. In: Symons J, van Dalen D, Davidson D (eds) Philosophical dimensions of logic and science: selected contributed papers from the 11th international congress of logic, methodology, and philosophy of science, Kraków, pp 165–178

    Google Scholar 

  42. Henkin L, Suppes P, Tarski A (1958) The axiomatic method with special reference to geometry and physics. North-Holland, Amsterdam

    MATH  Google Scholar 

  43. Hertz H (1894) Die Prinzipien der Mechanik. Johann Ambrosius Barth, Leipzig

    MATH  Google Scholar 

  44. Hornby GS, Globus A, Linden DS, Lohn JD (2006) Automated antenna design with evolutionary algorithms. In: AIAA space, pp 19–21

    Google Scholar 

  45. Hossenfelder S (2018) Lost in math: how beauty leads physics astray. Basic Books, New York

    MATH  Google Scholar 

  46. Howson C, Urbach P (2006) Scientific reasoning: the Bayesian approach. Open Court Publishing, Chicago

    Google Scholar 

  47. Jaynes ET (2003) Probability theory: the logic of science. Cambridge University Press, Cambridge

    Book  Google Scholar 

  48. Jeannin JB et al (2015) A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. Int J Softw Tools Technol Transfer 19(6):717–741

    Article  Google Scholar 

  49. Kemp C, Tenenbaum J (2009) The discovery of structural form. Proc Natl Acad Sci 105(31):10687–10692

    Article  Google Scholar 

  50. Khashabi D, Khot T, Sabharwal A, Roth D (2018) Question answering as global reasoning over semantic abstractions. In: AAAI-18

    Google Scholar 

  51. Khot T, Sabharwal A, Clark P (2018) SciTail: a textual entailment dataset from science question answering. In: AAAI-18

    Google Scholar 

  52. Krenn M et al (2016) Automated search for new quantum experiments. Phys Rev Lett 116(9):090405

    Article  Google Scholar 

  53. Kushman N, Artzi Y, Zettlemoyer L, Barzilay R (2014) Learning to automatically solve algebra word problems. In: ACL-2014

    Google Scholar 

  54. Langley P, Bradshaw GL, Simon HA (1981) BACON.5: The discovery of conservation laws. IJCAI-81, pp 121–126

    Google Scholar 

  55. Langley P, Bradshaw GL, Simon HA (1983) Rediscovering chemistry with the BACON system. In: Michalski RA et al (eds) Machine learning. Springer, Berlin

    Google Scholar 

  56. Laughlin R, Pines D (2000) The theory of everything. Proc Natl Acad Sci 97(1):28–31

    Article  MathSciNet  Google Scholar 

  57. Lehmann J, Chan M, Bundy A (2013) A higher-order approach to ontology evolution in physics. J Data Semant 2:163–187

    Article  Google Scholar 

  58. Ludwig G (1985) An axiomatic basis for quantum mechanics: volume 1, derivation of Hilbert space structure. Springer, Berlin

    Book  Google Scholar 

  59. Ludwig G (1987) An axiomatic basis for quantum mechanics: volume 2, quantum mechanics and Macrosystems. Springer, Berlin

    Book  Google Scholar 

  60. Ludwig G (1989) An axiomatic basis as a desired form of a physical theory. In: Proceedings of the 1987 international congress for logic, methodology, and the philosophy of science. North Holland, Amsterdam

    Google Scholar 

  61. Martin U, Pease A (2015) Hardy, Littlewood, and polymath. In: Davis E, Davis P (eds) Mathematics, substance and surmise: views on the meaning and ontology of mathematics. Springer, Berlin

    Google Scholar 

  62. MathOverflow (2016) Is it possible to have a research career while checking the proof of every theorem you cite? https://mathoverflow.net/questions/237987/is-it-possible-to-have-a-research-career-while-checking-the-proof-of-every-theor

  63. McCarthy J (1968) Programs with common sense. In: Minsky M (ed) Semantic information processing. MIT Press, Cambridge

    Google Scholar 

  64. McCune W (1997) Solution of the Robbins problem. J Autom Reason 193, 264–276

    MathSciNet  MATH  Google Scholar 

  65. McKinsey JCC, Sugar AC, Suppes P (1953) Axiomatic foundations of classical particle mechanics. J Ration Mech Anal 2:253–272

    MathSciNet  MATH  Google Scholar 

  66. Mehlberg H (1965) Space, time, relativity. In: Proceedings of the 1964 international congress for logic, methodology, and the philosophy of science. North Holland, Amsterdam

    Google Scholar 

  67. Melnikov A et al (2018) Active learning machine learns to create new quantum experiments. PNAS 115(6):1221–1226

    Article  Google Scholar 

  68. Montague R (1974) Deterministic theories. In: Thomason R (ed) Formal philosophy: selected papers of Richard Montague. Yale University Press, New Haven

    Google Scholar 

  69. Newell A (1982) The knowledge level. Artif Intell 18(1):87–127

    Article  MathSciNet  Google Scholar 

  70. Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL: a proof assistant for higher-order logic. Lecture notes in computer science, vol 2283. Springer, Berlin

    MATH  Google Scholar 

  71. Paleo BW (2012) Physics and proof theory. Appl Math Comput 219:45–53

    MathSciNet  MATH  Google Scholar 

  72. Rosenkrantz R (1977) Inference, method, and decision: towards a bayesian philosophy of science. Springer, Berlin

    Book  Google Scholar 

  73. Russell B (1903) The principles of mathematics. Cambridge University Press, Cambridge

    MATH  Google Scholar 

  74. Sant’Anna A (1999) An axiomatic framework for classical particle mechanics without space-time. Philos Nat 36:307–319

    MathSciNet  Google Scholar 

  75. Schwartz J (1960) The pernicious influence of mathematics on science. In: Proceedings of the 1960 international congress for logic, methodology, and the philosophy of science. North Holland, Amsterdam

    Google Scholar 

  76. Sigmund K (2017) Exact thinking in demented times: the Vienna circle and the epic quest for the foundations of science. Basic Books, New York

    MATH  Google Scholar 

  77. Slemrod M (2013) From Boltzmann to Euler: Hilbert’s 6th problem revisited. Comput Math Appl 65(10):1497–1501

    Article  MathSciNet  Google Scholar 

  78. Smith KA, Battaglia P, Vul E (2013) Consistent physics underlying ballistic motion prediction. In: Cognitive science

    Google Scholar 

  79. Sober E (2002): Bayesianism—its scope and limits. Proc British Acad 113:21–38

    MathSciNet  Google Scholar 

  80. Souyris J, Wiels V, Delmas D, Delseny H (2009) Formal verification of avionics software products. In: International symposium on formal methods, pp 532–546

    Google Scholar 

  81. Strevens M (2005) The Bayesian approach in the philosophy of science. In: Borchet DM (ed) Encyclopedia of philosophy, 2nd ed. Macmillan, Detroit

    MATH  Google Scholar 

  82. Strevens M (2013) Tychomancy: inferring probability from causal structure. Harvard University Press, Cambridge

    Book  Google Scholar 

  83. Suppes P, Luce RD, Krantz D, Tversky A (1974) Foundations of measurement. Dover Publications, Mineola

    MATH  Google Scholar 

  84. Tegmark M (2009) The multiverse hierarchy. ArXiv preprint arXiv:0905.1283

    Google Scholar 

  85. Tenenbaum JB, Kemp C, Griffiths TL, Goodman ND (2011). How to grow a mind: Statistics, structure, and abstraction. Science 331(6022):1279–1285

    Article  MathSciNet  Google Scholar 

  86. van Harmelen F, Lifschitz V, Porter B (eds) (2008) Handbook of knowledge representation. Elsevier, Amsterdam

    MATH  Google Scholar 

  87. Vogt A (1997) Review of an axiomatic basis for quantum mechanics: vol 1, derivation of hilbert space structure by Günther Ludwig, SIAM Rev 29(3):499–501

    Article  Google Scholar 

  88. Wallace D (to appear) The logic of the past hypothesis. In: Loewer B, Weslake B, Winsberg E (eds) Time’s arrows and the probability structure of the world Harvard University Press, Cambridge

    Google Scholar 

  89. Weidenbach C, Dimova D, Fietzke A, Kumar R, Suda M, Wischnewski C (2009) Spass Version 3.5. In: International conference on automated deduction (CADE) (Lecture Notes in Computer Science), vol 5563. pp 140–145

    Chapter  Google Scholar 

  90. Whitehead AN, Russell B (1910) Principia Mathematica. Cambridge University Press, Cambridge

    MATH  Google Scholar 

  91. Wittgenstein L (1922) Tractatus Logico-Philosophicus. Harcourt, Brace, and Company, San Diego

    Google Scholar 

  92. Yandell BH (2002) The honors class: Hilbert’s problems and their solvers. A.K. Peters. Taylor & Francis, Milton Park

    MATH  Google Scholar 

Download references

Acknowledgements

Thanks for useful information and helpful feedback to Scott Aaronson, Alan Bundy, Ken Forbus, Tom LaGatta, Michael Strevens, David Tena Cucala, Peter Winkler, and the anonymous reviewer.

Author information

Authors and Affiliations

  1. Department of Computer Science, New York University, New York, NY, USA

    Ernest Davis

Authors
  1. Ernest Davis
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ernest Davis .

Editor information

Editors and Affiliations

  1. Department of Philosophy, Simon Fraser University Philosophy, Burnaby, BC, Canada

    Nicolas Fillion

  2. The Rotman Institute of Philosophy, The Ontario Research Center for Computer Algebra and The School of Mathematical and Statistical Sciences, The University of Western Ontario, London, ON, Canada

    Robert M. Corless

  3. Department of Physics & Computer Science, Wilfrid Laurier University, Waterloo, ON, Canada

    Ilias S. Kotsireas

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Science+Business Media, LLC, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Davis, E. (2019). Proof Verification Technology and Elementary Physics. In: Fillion, N., Corless, R., Kotsireas, I. (eds) Algorithms and Complexity in Mathematics, Epistemology, and Science. Fields Institute Communications, vol 82. Springer, New York, NY. https://doi.org/10.1007/978-1-4939-9051-1_4

Download citation

Publish with us

Policies and ethics

Search

Navigation