A Perspective on Interactive Theorem Provers in Physics
Source abstract
Abstract
Abstract Interactive theorem provers (ITPs) are a class of computer programming language that guarantee the correctness of mathematical definitions and theorems written in to them. Within mathematics and artificial intelligence the usage of ITPs is growing. In this perspective, the best usage of ITPs are discussed within another area, physics, and motivate the existence of an open‐source community run project for formalized physics results, PhysLean.
Source: crossref · Quality: baseline
Research context
OpenAlex topics: Scientific Computing and Data Management · Mathematics, Computing, and Information Processing · Logic, programming, and type systems
SciVX discovery tags are terminology-based. OpenAlex topics are source-provided classifications.
Affiliations
Department of Computer Science University of Bath Bath BA2 7AU UK
References (21)
Show source-provided references
1. Google DeepMind AI achieves silver‐medal standard solving international mathematical olympiad problems 2024 https://deepmind.google/discover/blog/ai‐solves‐imo‐problems‐at‐silver‐medal‐level/.
2. The PhysLean Community PhysLean: Digitalising physics into lean 4 https://github.com/HEPLean/PhysLean.
3. L.De Moura S.Kong J.Avigad F.Van Doorn J.vonRaumer inAutomated Deduction‐CADE‐25: 25th International Conference on Automated Deduction Berlin Germany August 1‐7 2015.Springer 2015 pp.378–388.10.1007/978-3-319-21401-6_26 ↗
4. D.Silkenat Mechanizing Lagrangian mechanics in Isabelle/HOL 2022.
5. Khan‐Afshar S. · Math. Comput. Sci. · 2014 · 8 · 3910.1007/s11786-014-0175-z ↗
6. L.Vermeulen PhD Thesis Concordia University 2024.
7. E. H.Lu A formalization of elements of special relativity in Coq 2017 http://nrs.harvard.edu/urn‐3:HUL.InstRepos:38811518.
8. F.Marić J.Markovic Archive of Formal Proofs2025 https://isa‐afp.org/entries/GyrovectorSpaces.html Formal proof development.
9. M.Stannett E.Higgins H.Andreka J.Madarasz I.Németi G.Szekely Archive of Formal Proofs2023 https://isa‐afp.org/entries/No_FTL_observers_Gen_Rel.html Formal proof development.
10. R.Schmoetten J.Palmer J. D.Fleuriot Archive of Formal Proofs2021 https://isa‐afp.org/entries/Schutz_Spacetime.html Formal proof development.
11. Bobbin M. P. · Digital Discovery · 2024 · 3 · 26410.1039/D3DD00077J ↗
12. E. D.Ugwuanyi C. T.Jones J.Velkey T. R.Josephson arXiv preprint arXiv:2505.090952025.
13. J.Tooby‐Smith arXiv2025 https://arxiv.org/abs/2505.07939.
14. J.Tooby‐Smith arXiv2024 https://arxiv.org/abs/2411.07667.
15. Tooby‐Smith J. · Comput. Phys. Commun. · 2025 · 30810.1016/j.cpc.2024.109457 ↗
16. J.Breitner loogle https://github.com/nomeata/loogle.
17. P.Massot Lean blueprints https://github.com/PatrickMassot/leanblueprint.
18. K.Buzzard R.Taylor Towards a Lean proof of Fermat’s Last Theorem 2025 https://github.com/ImperialCollegeLondon/FLT.
19. V. K.Chaudhri C.Baru B.Bennett M.Bhatt D.Cassel A. G.Cohn R.Dechter E.Erdem D.Ferrucci K.Forbus G.Gelfond M.Genesereth A. S.Gordon B.Grosof G.Gupta J.Hendler S.Israni T. R.Josephson P.Kyllonen Y.Lierler V.Lifschitz C.McFate H. K.McGinty L.Morgenstern A.Oltramari P.Paritosh D.Roth B.Shepard C.Shimzu D.Vrandečić arXiv preprint arXiv:2506.165962025.
20. J.Asher arXiv2025 https://arxiv.org/abs/2506.11085.
21. Yang K. · Adv. Neural Inf. Process. Syst. · 2023 · 36