A Perspective on Interactive Theorem Provers in Physics

Joseph Tooby-Smith

doi:10.1002/advs.202517294

A Perspective on Interactive Theorem Provers in Physics

Joseph Tooby-Smith

Department of Computer Science

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Article number	e17294
Journal	Advanced Science
DOIs	https://doi.org/10.1002/advs.202517294
Publication status	Published - 22 Oct 2025

Keywords

interactive theorem provers
physics
proof assistants

ASJC Scopus subject areas

Medicine (miscellaneous)
General Chemical Engineering
Biochemistry, Genetics and Molecular Biology (miscellaneous)
General Materials Science
General Engineering
General Physics and Astronomy

Access to Document

10.1002/advs.202517294Licence: CC BY

Cite this

@article{623987e581a341029e04eaf71db8112b,

title = "A Perspective on Interactive Theorem Provers in Physics",

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.",

keywords = "interactive theorem provers, physics, proof assistants",

author = "Joseph Tooby-Smith",

year = "2025",

month = oct,

day = "22",

doi = "10.1002/advs.202517294",

language = "English",

journal = "Advanced Science",

issn = "2198-3844",

publisher = "John Wiley and Sons Inc.",

}

TY - JOUR

T1 - A Perspective on Interactive Theorem Provers in Physics

AU - Tooby-Smith, Joseph

PY - 2025/10/22

Y1 - 2025/10/22

N2 - 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.

AB - 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.

KW - interactive theorem provers

KW - physics

KW - proof assistants

UR - https://www.scopus.com/pages/publications/105019556693

U2 - 10.1002/advs.202517294

DO - 10.1002/advs.202517294

M3 - Article

SN - 2198-3844

JO - Advanced Science

JF - Advanced Science

M1 - e17294

ER -

A Perspective on Interactive Theorem Provers in Physics

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this