Leopoldo Sarra - autoformalization in physics / engineering

Stream: Lean Together 2026

[Jireh Loreaux]

Discussion thread for the talk.

[Jireh Loreaux]

(copied from the Zoom chat):
Dominic Steinitz said:

The problem is at what level do you present your theory. Electromagnetism can be either Maxwell’s equations or a gauge theory for example

Leo said:

Probably we need to accept different formalizations, and show that they are equivalent, one choice may be useful for some application and some other choice is better for proving other properties? I mean it is probably valuable to have both the general theory and the specific implementation that derives maxwells equations, because you don’t want to start from scratch each time you want to use them.

[Joseph Tooby-Smith]

Thanks for the nice talk here. I want to ask a question related to something I've asked in private before, but would be nice to get a public answer to:

In your talk you mentioned the need to have a library for physics - I would naturally argue that such a library exists in the shape of #PhysLean the aim of which is to be a community run - open source project. What can we take from what you have learned to:

1. Make PhysLean better and easier to use for the community?
2. Expand its results in the direction of Quantum Mechanics?
3. Make it easier for companies like Axiomatic AI to use?

[Leopoldo Sarra]

Joseph Tooby-Smith said:

Thanks for the nice talk here. I want to ask a question related to something I've asked in private before, but would be nice to get a public answer to:

In your talk you mentioned the need to have a library for physics - I would naturally argue that such a library exists in the shape of #PhysLean the aim of which is to be a community run - open source project. What can we take from what you have learned to:

1. Make PhysLean better and easier to use for the community?
2. Expand its results in the direction of Quantum Mechanics?
3. Make it easier for companies like Axiomatic AI to use?

Yes we are definitely happy to integrate with existing effort, and as you know we are exploring the best ways of doing it : ) I think it goes that direction, we are looking for a library that can be used for practical applications (e.g. solving exercises) and we are interested in lowering the entry barrier, especially for physicists that don't have enough experience in Lean! We are currently iterating on the quantum library as a proof of concept to try more practical applications, it's more about understanding how hard is it to build the supporting tactics and interfaces rather than the specific field I would say!

[Joseph Tooby-Smith]

library that can be used for practical applications (e.g. solving exercises)

It's hard for me to see how this is different from what PhysLean is doing (i.e. building APIs around key areas to make them easier to use etc.). Do you have any specific examples in mind which would help illustrate the idea, or have something specific that would stop you from making a pull-request to PhysLean or QuantumInfo (depending on the problem) and building up or improving those libraries?

[Dominic Steinitz]

@_Leo|921547 said:

Probably we need to accept different formalizations, and show that they are equivalent, one choice may be useful for some application and some other choice is better for proving other properties? I mean it is probably valuable to have both the general theory and the specific implementation that derives maxwells equations, because you don’t want to start from scratch each time you want to use them.

That seems eminently sensible. I do recall someone working on affine connections which I hope will one day meet with my attempts on top down Ehresmann connections (specialised to principal fiber bundles).

The first two of Maxwell's equations (no magnetic monopoles and Faraday's law) are a consequence of the first Bianchi identity. But I feel we are still some way from being to write that down (and certainly without the "Débauche d'indices" as Cartan puts it). But it would be fun to do this Mathlib or PhysLean.

[Joseph Tooby-Smith]

@Dominic Steinitz In PhysLean we have the derivation of Maxwell's equations from the Lagrangian of the EM potential, and the definition of the Electric field and Magnetic field in terms of the field strength tensor (will be in a paper at some point). This is done in terms of Lorentz tensors, not connections yet. E.g. (from here)

lemma isExtrema_iff_tensors {𝓕 : FreeSpace}
    (A : ElectromagneticPotential d)
    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ ∞ J) :
    IsExtrema 𝓕 A J ↔ ∀ x,
    {((1/ 𝓕.μ₀ : ℝ) • tensorDeriv A.toFieldStrength x | κ κ ν') + - (J x | ν')}ᵀ = 0 := by

says (in index notation) that $A$ is an extrema of the action with external current $J$ if and only if $\frac{1}{\mu_0} \partial_\kappa F^{\kappa \nu'} - J^{\nu'}= 0$.

[Leopoldo Sarra]

Joseph Tooby-Smith said:

library that can be used for practical applications (e.g. solving exercises)

It's hard for me to see how this is different from what PhysLean is doing (i.e. building APIs around key areas to make them easier to use etc.). Do you have any specific examples in mind which would help illustrate the idea, or have something specific that would stop you from making a pull-request to PhysLean or QuantumInfo (depending on the problem) and building up or improving those libraries?

Until now it was just faster for us to iterate in a smaller repo, but we are also happy to push to PhysLean the parts that can go there. I think as we work more together we will figure out what code should go where, and the differences will be more clear!

The idea of development driven by exercises also means that all definitions are used in practice, avoiding the possibility that a definition can be changed without breaking anything like here https://github.com/HEPLean/PhysLean/pull/894/files

[Joseph Tooby-Smith]

Makes sense and sounds good to me. As I said above - let me know if there is anything I can do to help here.
I think the exercise driven approach is nice, and like you say a good test of definitions.

[Joseph Tooby-Smith]

More generally, I really think it is a good idea that we have a single (open-source, community-run) project that is collectively worked on, and that we try and prevent competing fiefdoms - which will lead to conflicting definitions, theorems etc. and in general make things harder for new users. I'm fully aware that it probably feels that PhysLean is my fiefdom, and I am willing to take suggestions of how we can prevent/mitigate this. Here is my suggestion: We expand/create the 'maintainer team' for the project, and then if you have someone on your team who 1) is somewhat use to Mathlib's review process, 2) has direct experience writing Lean code for physics, 3) willing to volunteer to be on the 'maintainer team' and act impartially and independently, then I think it makes sense to have them on the 'maintainer team'.

Is this an approach you think you would be interested in?

[Leopoldo Sarra]

I think it makes sense and we should really explore this direction! Let's discuss it more in a few weeks or so ?(while we still work on some internal project)