Undergraduate Physics

Stream: Natural sciences

[Joseph Tooby-Smith]

I am interested in making a foray into formalizing the undergraduate physics curriculum using Lean. (My background: I'm a physics postdoc at Cornell, but my work is fairly mathematical.)

A previous thread in this stream seems to indicate that Hamiltonian Mechanics may be difficult to do due to the lack of formalism for ODEs and PDEs.

I think it would be nice to have a list of areas in undergraduate physics (and other areas), an indication of whether they can be formalised in lean or not - and what the obstacles are for formalisation. An obvious question is, what are the areas which can be formalised using the current state of mathlib? Maybe special relativity?

[Tomas Skrivan]

I'm also interested in formalizing physics, mainly from computational perspective. Writing down a set of ODEs/PDEs and then transforming/approximating them until I obtain executable program computing approximate solution.

If you want to formalize physics textbooks I would argue that you do not really need too much of ODE and PDE theory. In physics, you usually assume that the solution exists and only derive that the solution has such and such properties. This usually boils down to some involved calculation and approximation.

I would not shy away from trying to do Hamiltonian mechanics, you can just assume the missing parts of mathlib. I think having such formalization of Hamiltonian mechanics would be great and it could motivate people to further develop the missing parts of mathlib.
One crucial point, if you want to do Hamiltonian mechanics from geometrical perspective then I would wait as (I think) mathlib does not have differential forms yet.

I think there are two main challenges. First, figuring out what exactly are the starting assumptions and what are the statements you want to formalize ... well this effectively Hilbert's 6th problem. The second challenge will be doing calculations, it can be quite tiresome in lean and there is not yet too much good automation for it. (I'm working on symbolic differentiation but it is not ready yet)

[Tyler Josephson ⚛️]

Welcome to the Lean community! We're really interested in this, too. Take a look at our preprint here - we formalize the derivation of the kinematic equations from the 1D equations of motion for constant acceleration.

@Tomas Skrivan did a great job of laying out your options. I see this on two orthogonal axes - formalizing the physics and formalizing the mathematics.

Along the "formalizing mathematics" axis: If you don't care about connecting either to foundational axioms, you can just assume high-level mathematics as axioms and you can just state the physics assumptions as hypotheses, then build out the proof from there. Alternatively, you can import your mathematics from Mathlib, then state the physics assumptions as hypotheses, and build out the proof from these. If Mathlib doesn't have the math you need, then you'll have to wait for someone else to do it, or take that initiative yourself. As Tomas said, if you do the first approach, you can refactor your code later on once the requisite math has been added to Mathlib.

Along the "formalizing physics" axis - where you land on this corresponds to how you approach Hilbert's 6th problem. In our paper, we very much start at high-level concepts and prove what other high-level concepts follow. At the moment, I'm not too interested in unifying all the things, and I suspect you're not too interested in that either, given your curiosity about formalizing undergrad physics. Nonetheless, figuring out techniques for formally interrelating different scientific theories is something we're exploring.

[Tyler Josephson ⚛️]

Since you specifically asked about special relativity, I'll point you to this senior thesis:
https://dash.harvard.edu/handle/1/38811518?show=full

[Adomas Baliuka]

How about quantum theory (esp. quantum information)? It's mostly basic linear algebra and maybe a tiny bit of representation theory. L2 spaces seem to at least have a skeleton, too.

[Tyler Josephson ⚛️]

Tomas Skrivan said:

In physics, you usually assume that the solution exists and only derive that the solution has such and such properties. This usually boils down to some involved calculation and approximation.

Approximation is something we haven't tackled yet, but this shows up a lot in science/engineering proofs, so it's on my radar. E.g. Wikipedia's derivation of Kepler's Third Law uses an "approximately equal" logical step, to reduce m1+m2 to m1, because m1 (mass of sun) >> m2 (mass of planet). What would be the Lean way to do this?

theorem kepler_reduce {a T G m1 m2 : ℝ} (h1: a^3 / T^2 = G*(m1 + m2)/(4* π^2)) (h2: m1 > m2)
: (a^3 / T^2 = G*(m1)/(4* π^2)) := by sorry

[Adomas Baliuka]

One way would be to include statements like "x much greater than y" as input assumptions and replace equality by some notion of "equal to first order in all the small things"? (Maybe reuse Landau notation?)

Of course, it doesn't match the normal practice of not mentioning assumptions and writing "equals" for "equal enough". However, I don't see how you can prove a statement that is only approximate using Lean's = in a framework that doesn't immediately allow to prove False. The way physics works in my experience (no snark intended) is that you work in a framework that does allow to prove False and just don't do that.

[Tyler Josephson ⚛️]

Landau notation could be great here! I suspect we can restate such arguments using limits, too. A more difficult approach would be to build an alternative to equality, like ≈ a la this paper.

[Tyler Josephson ⚛️]

Overall, I think what Lean can offer Physics is to provide an alternative framework that rewards the author for staying within the guardrails of mathematics, and pushes them away from the hand-wavy derivations toward more rigorous ones.

[Kevin Buzzard]

And time will tell us whether this kind of approach can remain feasible -- or rather whether the community can use Lean to make it feasible.