Towards autoformalization for physics and engineering with Lean

Abstract: We strive to bring formal methods and interactive theorem provers like Lean 4 to the broader scientific community beyond mathematics. To ease its adoption, we are building reusable Lean libraries that formalize areas of science using the main concepts that scientists and engineers actually apply in practice, such as dimensional analysis, tolerances, and approximations.

We begin with physics domains that have a strong mathematical grounding, like quantum mechanics, where we validate the correctness of the libraries on real use cases and problem sets (e. g. 700 problems from Galitski et. al. 2013) to ensure their practical relevance and adoptability.

Finally, we are developing autoformalization AI agents to further boost the adoption of formal methods in science and engineering. These agents will have access to the libraries we build, as well as Mathlib, enabling them to help formalize real-world problems together with their proposed solutions in the form of theorems. This allows us to certify the validity of a given solution by converting it into a formal theorem and proving it through our prover AI agents.

logic in computer sciencemathematical softwaremathematical physicsquantum physics

Audience: researchers in the topic

( video )

Lean Together 2026