Formal treatment for physics

Stream: general

[Abhishek Chugh]

Can someone point me to any formalization work done in physics.
For example, proving "when a force of 1N is applied to an object of mass 1kg, it travels 2m in 2 seconds" using Newton's laws (and required math) as axioms.

Not hoping to find an actual working system, but any theoretical work, i.e. book chapters, papers dealing with rigorous proof will also be quite helpful.

[Jalex Stark]

I haven't studied this, but I think it might be asking the lines of what you're looking for
https://groups.csail.mit.edu/mac/users/gjs/6946/sicm-html/

[Abhishek Chugh]

Thanks Jalex. The formal treatment is very helpful.

[Abhishek Chugh]

For future reference, here is another paper that discusses formalization of physics in detail

[Abhishek Chugh]

https://nyuscholars.nyu.edu/en/publications/proof-verification-technology-and-elementary-physics

[Ben]

I'm interested in figuring out how Lean can be applied to mathematical derivations in Physics.

[Jireh Loreaux]

Can you give an example of the kinds of things you're interested in? For example, one simple example, and one thing you hope can be done eventually.

[Bulhwi Cha]

On formalization of Hamiltonian mechancs: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Bulhwi.20Cha.20.26.20Seongwoo.20Shim.3A.20Introductions/near/293911504

[Ben]

Jireh Loreaux said:

Can you give an example of the kinds of things you're interested in? For example, one simple example, and one thing you hope can be done eventually.

Hello Jireh,

I've been working on a project to write down mathematical Physics -- https://derivationmap.net/
That project is primarily focused on documenting the relations between the equations used in Physics.
I've been using a Computer Algebra System called SymPy to validate steps in derivations.
It may be possible to use Lean to validate derivations.

As very simple example, start with the equation

$$T =\frac{1}{f}$$

where $T$ is period of oscillation and $f$ is frequency of oscillation.
A transformation would be to multiply both sides by $f$ to get

$$f T = 1$$

and then divide both sides by $T$ to get

$$f = \frac{1}{T}$$

That's not too exciting, but has 2 steps and is easier to understand than a 12 step derivation like
https://derivationmap.net/review_derivation/000004/?referrer=zulip_2023-06-17

I'm not clear yet how to map steps in a derivation to aspects of a proof in Lean.

My current understanding is that the initial expression (here $T=1/f$) is a predicate, and the output (here $f=1/T$) is a goal? The transformations between expressions might be tactics in Lean. Alternatively, each step in a derivation might constitute a theorem.
At this point I don't know enough about the mapping to be sure about how to proceed.

I'm relatively confident that the above derivation (involving simple algebra) can be done in Lean now. I'm not clear where the boundaries are for what cannot be done in Lean. For example, Dirac notion for quantum, or Einstein notation for electrodynamics.

I found https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Maxwell.20relation and that's aligned with what I'm interested in.

[Tomas Skrivan]

I'm interested in physics related stuff too, more on the computational side rather than formally proving everything but there is a big overlap.

Looking at the derivation of the wave equation from Maxwell's equations, it looks totally doable in Lean, you could even write a widget that would extract info from the proof and display the graph.

Figuring out how much information to display and how to do it in a human readable way will be the tricky part. Some tactics can do too much and some do too obvious steps.

Regarding notation, by "Dirac notion" do you mean bra-ket notation? That should be straightforward, it might clash a bit with notation for nameless constructors, but that has to be tested.
I'm not so sure if Einstein's summation convention is a good idea, it would have to go through syntax to find repeated indentifiers and plug in a binder somewhere. Having this globally is definitely a bad idea, maybe you could define a special syntax category for physics expressions. Alternatively you just write the binders yourself i.e. instead of writing T i i you would write \Sigma i, T i i

[Eric Wieser]

I assume you mean \sum not \Sigma

[Eric Wieser]

One problem you'll have with something like https://derivationmap.net/review_derivation/000004/?referrer=zulip_2023-06-17 is that, as far as I know, mathlib doesn't have any of div/grad/curl (they can be built without too much work from docs#fderiv; but we don't have any proofs about them)

[Ben]

Tomas Skrivan said:

Looking at the derivation of the wave equation from Maxwell's equations, it looks totally doable in Lean, you could even write a widget that would extract info from the proof and display the graph.

Yes, after thinking about the mapping between the Physics Derivation Graph and Lean I've come up with the following.

Deriving $f = 1/T$ from $T=1/f$ is expressed in Lean as

(T = 1/f) -> (f = 1/T)

Breaking a derivation into steps is simply a sequence of related proofs:

(T = 1/f) -> (T f = 1)
and then
(T f = 1) -> (f = 1/T)

I think this generalizes to more complicated derivation graphs. My sketch of that observation is here: https://physicsderivationgraph.blogspot.com/2023/06/relation-between-inference-rules-in.html

Figuring out how much information to display and how to do it in a human readable way will be the tricky part. Some tactics can do too much and some do too obvious steps.

Agreed. My hacky approach is to make the granularity of derivation (i.e., how many steps in the derivation, aka how big are the leaps in logic) tunable. A somewhat related web demo of tunable granularity: https://derivationmap.net/clickable_layers?referrer=zulip_2023-06-18

Regarding notation, by "Dirac notion" do you mean bra-ket notation? That should be straightforward, it might clash a bit with notation for nameless constructors, but that has to be tested.
I'm not so sure if Einstein's summation convention is a good idea, it would have to go through syntax to find repeated indentifiers and plug in a binder somewhere. Having this globally is definitely a bad idea, maybe you could define a special syntax category for physics expressions. Alternatively you just write the binders yourself i.e. instead of writing T i i you would write \Sigma i, T i i

I'll start with derivations that just rely on algebra before getting to more advanced notation, but my intent in mentioning Dirac/bra-ket notation and Einstein notation was to point to the more complicated notations that I'm hoping to include. Thank you for explaining potential paths forward.

[Tyler Josephson ⚛️]

@Tomas Skrivan’s SciLean project is worth checking out!

https://github.com/lecopivo/SciLean