Physics in Lean

Stream: Natural sciences

[Mr Proof]

Have many physics theorems been done in Lean? (Should there be a PhysicsLib?)

I suppose some proofs might be (off the top of my head:)

• Prove a projectile follows a parabolic path
• Prove orbits are conic sections under an inverse square law
• Prove Maxwell's equations are Lorentz invariant
• Prove Einstein's equations are diffeomorphism invariant
• Proof of renormalizability of QED
• Proof of Noether's theorem
• Prove non-quantum black holes never decrease their surface area
• Prove Penrose singularity theorems
• Prove quantum mechanics satisfies causality
• Prove space-time can't smoothly change the signature of the metric
• Prove centre of mass of a closed system doesn't change

Any others? Well you might say of course these are just mathematical proofs in disguise.

[Utensil Song]

You might want to check out HepLean: https://github.com/HEPLean/HepLean

[Utensil Song]

and #Natural sciences

[Mr Proof]

Seems like people are starting at the most difficult physics and working their way down from there!

[Joseph Tooby-Smith]

Hey @Mr Proof , it would be great to have some of the things you mention in HepLean. It would also be great to have more people involved in this project.

There is some motivation for starting with something like high-energy physics, rather than say more 'basic physics results'. Parts of high energy physics are very close to mathematics (some are indistinguishable from mathematics), thus it lends itself very nicely to formalisation into Lean. I also believe that the way to get the physics community involved in Lean is to show them how it can be useful in their research. (I note that high energy physics is quite broad, and includes all but 4 of the points you mention).

It is my opinion that we are not ready for something like PhysicsLib, for the whole of physics. Physics communities are quite separated from one another, and have their own cultures and expectations. It's hard to imagine fitting all of that into one project, and keeping everyone happy/been able to motivate people that its a good idea.

[Mr Proof]

I wonder how much of a physicslib would just be making alternative names for mathematical concepts. e.g.

• acceleration --> second derivative
• gravity --> Riemannian geometry
  I could see value in maybe more of a database of physics proofs which would basically be mathematics proofs inspired by physics.

Indeed, my personal view is that the universe and it's symmetries are really just some expression of some exceptional mathematical object anyway.

BTW, do you have a roadmap for the HEPlean? From the paper I see it is starting with CKM matrix and Higgs potentials. That maybe would be a good start to do a sort of blue-print for physics. (Sort of like the FLT project). And then it would allow different people to work on different aspects and fit it all together at the end.

[Joseph Tooby-Smith]

I agree with your personal view of the universe. I could even make a guess of what that mathematical object is. But we are a long way from going from there to what the average physicist is working on - the theory just isn't there yet.

I don't have a roadmap per-se for HepLean. HepLean is more like Mathlib than the FLT project, there is not a single target. When I was writing the paper I had the targets of the CKM matrix, the Higgs potential and anomaly cancellation conditions, but these are pretty much done. I have my own personal targets within HepLean. I am working on the properties of the Lorentz group so that we can define properties of fermions etc. I also have ideas for other targets (which anyone should feel welcome to take), some of which are discussed at the end of my paper, some of which are given here: https://github.com/users/jstoobysmith/projects/4.

[Jason Rute]

Also check out https://atomslab.github.io/LeanChemicalTheories/ by @Tyler Josephson ⚛️ and his lab. I think his goal is to make a sort of SciLib to complement Mathlib.

[Tyler Josephson ⚛️]

Yes! We're focused on bringing Lean into science and engineering applications. My group has a half dozen grad and undergrad students working on this. Check out our paper here (note this is Lean 3; we're only doing Lean 4 now) - we have more on the way.

[Tyler Josephson ⚛️]

We're interested in two directions with this: 1) describing derivations in science and engineering as math proofs, and 2) writing formally-verified software for scientific computing.

These can go hand-in-hand: one major long-term project is to define molecular dynamics simulations in Lean as executable software (capable of integrating the equations of motion for interacting particles in a simulation box) and pair that with proofs about the functions involved in the software. @Tomas Skrivan is a major player in this, with his development of SciLean. I've found, in the grant funding space, that connecting this to "bug-free software" is strong motivation for funding agencies that value practical applications of the work we do.

I'd love to build an interconnected web of derivations in statistical thermodynamics, connecting the axioms of statistical mechanics to definitions of things like "canonical ensemble" and proving that an implemented molecular dynamics simulation (or a Monte Carlo simulation) generates samples in that distribution. Functions that analyze MD simulation outputs to calculate things like "pressure" and "temperature" could be formally connected to their thermodynamic concepts.

[Tyler Josephson ⚛️]

We don't have an official "wishlist" of math missing from Mathlib essential for our project, but partial derivatives is a major one.

[Mr Proof]

No partial derivatives? :open_mouth: We got to fix that.
Is it yet possible to do calculus of variations e.g. L=(1/2) (dx/dt)^2 + V(x) and prove that the Euler-Lagrange equations give d^2/dx^2-V'(x) ?
Just wondering what the state of play is at the moment.
It would be nice to be able to just write down things like Maxwell's equations even if we can't prove anything about them yet.

[Kim Morrison]

In what sense are partial derivatives missing?

[Mr Proof]

BTW is this up to date: https://leanprover-community.github.io/undergrad_todo.html because it says partial derivatives are are missing.

[Kim Morrison]

That page is horribly out of date. :-)

[Dean Young]

@Kim Morrison what is there for something like ∂ᵢ : [ℝⁿ, ℝ]_(Smooth) ⭢ [ℝⁿ, ℝ]_(Smooth) ?

[Joseph Tooby-Smith]

@Mr Proof (As a side not, the proper way to write down the Maxwell equations is using the theory of principal bundles and connections thereon. I am pretty sure this isn't yet in Mathlib.)

[Mr Proof]

Hopefully we can write it in physics-sy way and a math-y type way and then have proofs linking the two. Reminds me of books with titles like "physics for mathematicians" which writes everything in a language no physicist would understand. I must admit things like "fibre bundles" go right over my head :laughing:.

[Joseph Tooby-Smith]

This isn't really a math-y vs physics-y way. If you want to quantise electromagnetism (or do it on space-times which are not R^4) you need principal bundles, fibre bundles and connections - this is certainly part of physics. Part of physics is writing things in the correct mathematical language; it makes life easier in the long run. This is especially important for something like Lean, where you (hope) that you only have to formalise things once, and then people can use it in perpetuity.

[Mr Proof]

Perhaps you may need principle bundles but you can certainly get quite far without knowing what they are. It's just that physicists use different terminology. I'd be impressed if you found any mention of fibre bundles in any papers by Einstein, Dirac or Feynman to name but a few.
I would disagree that there is a "correct" language, as mathematicians and physicists often use different terms, conventions and names.
But having said that if Lean is geared towards mathematicians then I suppose it is best to use the language of mathematicians.

[Tyler Josephson ⚛️]

@Kim Morrison It has been a while since I dug into this; Moogle tells me multivariable polynomials have partial derivatives.

For example, can we state the Maxwell relations (to be disambiguated from Maxwell's equations; I'm personally more into thermodynamics than electromagnetism)? Fick's Law of diffusion? What about Navier-Stokes?

[Kim Morrison]

Dean Young said:

Kim Morrison what is there for something like ∂ᵢ : [ℝⁿ, ℝ]_(Smooth) ⭢ [ℝⁿ, ℝ]_(Smooth) ?

variable (n : Nat) (f : (Fin (n + 1) → ℝ) → ℝ)
#check fderiv ℝ f 0 (Pi.single 0 1)

[Kim Morrison]

Oh, I guess this is not actually what you are asking for, but there is plenty of material on derivatives.

[Utensil Song]

Tyler Josephson ⚛️ said:

Kim Morrison It has been a while since I dug into this; Moogle tells me multivariable polynomials have partial derivatives.

For example, can we state the Maxwell relations (to be disambiguated from Maxwell's equations; I'm personally more into thermodynamics than electromagnetism)? Fick's Law of diffusion? What about Navier-Stokes?

They might also be stated with what's available in SciLean.

[Kevin Buzzard]

Whilst it's good to have discussions about physics in the open, there is an entire stream #Natural sciences where one can discuss physics. I personally would be interested to see lists of desiderata from people wishing to do physics but who feel like they are missing fundamental constructions. We have a huge and general theory of differentiation on manifolds including infinite dimensional manifolds, p-adic manifolds and more, of course we have partial derivatives, in a completely coordinate-free manner. We don't have partial d/dx per se because that involves picking a basis which we avoid if possible. But we can make it if you want, it will just be one line of gobbledegook given what we have.

[Patrick Massot]

Kim Morrison said:

That page is horribly out of date. :-)

I don’t think this is true. If you know things that are outdated on this page then it would be great to say it. I am sure there are a couple of outdated items. But there are many more items that are stuck because a style mismatch. The case of partial derivatives is a canonical example. This is a notion that is emphasized in a certain style of elementary courses, although it is mathematically “useless”. So it is not developed in Mathlib, but it is a question that arises on Zulip from time to time. One way to try to fix that is to create a Lean file with explanations about how to get partial derivatives from Fréchet derivatives, so that we can point to it from that undergrad list and when people ask. But it should probably come with big warnings telling people to not build on this. Nobody took the trouble to do it, that’s all.

[Patrick Massot]

Mr Proof said:

Perhaps you may need principle bundles but you can certainly get quite far without knowing what they are. It's just that physicists use different terminology. I'd be impressed if you found any mention of fibre bundles in any papers by Einstein, Dirac or Feynman to name but a few.

It seems your definition of physics stops right before fiber bundles become useful.

But having said that if Lean is geared towards mathematicians then I suppose it is best to use the language of mathematicians.

Formalization is definitely easier in a more abstract setting. But this goes beyond the usual language of mathematicians. I think every mathematician here learned more abstract mathematics when learning about Lean. It is just more efficient.

[Ruben Van de Velde]

Partial derivatives might be interesting for Archive, maybe

[Patrick Massot]

We could do that, or we could even have a folder dedicated to specializations of Mathlib things to more elementary setups.

[Yaël Dillies]

It could also fit in the framework of textbook formalisations

[Dean Young]

The recognition theorem, the fundamental theorem of G-principal bundles and two variations each
Screenshot-2024-06-17-at-12.36.24AM.png

Note that Id₁ is the identity law for "tree shapes", Ass the "associativity for tree-composition", etc.

[Dean Young]

InternalGroupAction₀ ⊆ InternalGroupAction ⊆ OperadicGroupAction

[Mr Proof]

Is there any documentation how to express the Klein Gordon equation in Lean notation? That would be a nice start I think. (Talking as a beginner).

[Winston Yin (尹維晨)]

We can have lofty goals, but it’s probably best to reproduce the success of the Xena project by first restricting ourselves to the typical undergraduate physics curriculum.

As an example, it’s probably a reasonable short term goal to formalise common special functions, eg spherical harmonics. And the equivalence between Hamiltonian and Lagrangian formulations.

Some of these can go into mathlib, I reckon, but others are just special instantiations of general mathematical statements, which are probably better suited for a specialised physics library.

[Mr Proof]

Well if you're trying to implement the theoretical minimum, perhaps this book would be a good guide? (just as inspiration)

Spherical harmonics would be nice. In terms of showing they satisfy a wave equation for a hydrogen atom maybe? Although that's probably not difficult to prove. More a case of just substituting them in and simplifying a few times :thinking: Perhaps the more difficult proof is that these solutions form a complete basis.

[Winston Yin (尹維晨)]

Isn’t this a pop sci -ish book? I’m more inclined to provide a library in which people formalise standard problems of popular textbooks, eg Griffiths E&M and quantum mechanics.

[Tomas Skrivan]

Here is an example how to state Klein-Gordon, Navier-Stokes, Maxwell and Euler-Lagrange equations in flat space:

import Mathlib

variable {n : ℕ}  {U} [NormedAddCommGroup U] [NormedSpace ℝ U]

open BigOperators EuclideanSpace

/-- partial derivative -/
noncomputable
abbrev pderiv (i : Fin n) (u : EuclideanSpace ℝ (Fin n) → U) (x : EuclideanSpace ℝ (Fin n)) :=
  deriv (fun (h' : ℝ) => u (x + h' • basisFun (Fin n) ℝ i)) 0

/-- iterated partial derivative -/
noncomputable
abbrev iteratedPDeriv (k : ℕ) (i : Fin n) (u : EuclideanSpace ℝ (Fin n) → U) (x : EuclideanSpace ℝ (Fin n)) :=
  iteratedDeriv k (fun (h' : ℝ) => u (x + h' • basisFun (Fin n) ℝ i)) 0

noncomputable
def laplace
    {U} [NormedAddCommGroup U] [NormedSpace ℝ U]
    (u : EuclideanSpace ℝ (Fin n) → U) (x : EuclideanSpace ℝ (Fin n)) :=
  ∑ i, iteratedPDeriv 2 i (fun x' => u x') x

noncomputable
def div
    (u : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (x : EuclideanSpace ℝ (Fin n)) :=
  ∑ i, pderiv i (fun x' => u x' i) x

noncomputable
def curl
    (u : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (x : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3) :=
  ![pderiv 1 (fun x' => u x' 2) x - pderiv 2 (fun x' => u x' 1) x,
    pderiv 2 (fun x' => u x' 0) x - pderiv 0 (fun x' => u x' 2) x,
    pderiv 0 (fun x' => u x' 1) x - pderiv 1 (fun x' => u x' 0) x]


def KleinGordonEquation (m : ℝ) (ψ : ℝ → EuclideanSpace ℝ (Fin n) → ℝ) :=
  ∀ (t : ℝ) (x : EuclideanSpace ℝ (Fin n)),
    iteratedDeriv 2 (fun t' => ψ t' x) t + laplace (ψ t) x + m^2 • ψ t x = 0


def NavierStokesEquation
    (ρ ν : ℝ)
    (u : ℝ → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (p : ℝ → EuclideanSpace ℝ (Fin n) → ℝ) :=
  ∀ t x,
    deriv (fun t' => u t' x) t + fderiv ℝ (fun x' => u t x') x (u t x) = - ρ⁻¹ • gradient (fun x' => p t x') x + ν • laplace (fun x' => u t x') x
    ∧
    div (fun x' => u t x') x = 0


def MaxwellEquations
    (ε₀ μ₀ : ℝ)
    (E : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))
    (B : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))
    (ρ : ℝ → EuclideanSpace ℝ (Fin 3) → ℝ)
    (J : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) :=
  ∀ t x,
    div (fun x' => E t x') x = ρ t x / ε₀
    ∧
    div (fun x' => B t x') x = 0
    ∧
    curl (fun x' => E t x') x = - deriv (fun t' => B t' x) t
    ∧
    curl (fun x' => B t x') x = μ₀ • (J t x + ε₀ • deriv (fun t' => E t' x) t)


def EulerLagrangeEquation
    (L : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3) → ℝ)
    (q : ℝ → EuclideanSpace ℝ (Fin 3)) :=
  ∀ t,
    -- ∇ₓ L(t,x(t),ẋ(t))                        - d/dt (∇_ẋ L(t,x(t),ẋ(t)))
    gradient (fun x => L t x (deriv q t)) (q t) - deriv (fun t' => gradient (fun v => L t' (q t') v) (deriv q t')) t = 0

[Tomas Skrivan]

In SciLean I define custom notation for derivatives so the equations would look like this:

code

def KleinGordonEquation (m : ℝ) (ψ : ℝ → EuclideanSpace ℝ (Fin n) → ℝ) :=
  ∀ (t : ℝ) (x : EuclideanSpace ℝ (Fin n)),
    ∂[2] (t':=t) ψ t' x + Δ (x':=x), ψ t x' + m^2 • ψ t x = 0


def NavierStokesEquation
    (ρ ν : ℝ)
    (u : ℝ → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (p : ℝ → EuclideanSpace ℝ (Fin n) → ℝ) :=
  ∀ t x,
    ∂ (t':=t), u t' x + ∂ (x':=x;(u t x)), u t x' = - ρ⁻¹ • ∇ (x':=x), p t x' + ν • Δ (x':=x), u t x'
    ∧
    ∇⬝ (x':=x), u t x' = 0


def MaxwellEquations
    (ε₀ μ₀ : ℝ)
    (E : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))
    (B : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))
    (ρ : ℝ → EuclideanSpace ℝ (Fin 3) → ℝ)
    (J : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) :=
  ∀ t x,
    ∇⬝ (x':=x), E t x' = ρ t x / ε₀
    ∧
    ∇⬝ (x':=x), B t x' = 0
    ∧
    ∇× (x':=x), E t x' = - ∂ (t':=t), B t' t
    ∧
    ∇× (x':=x), B t x' = μ₀ • (J t x + ε₀ • ∂ (t':=t), E t' x)


def EulerLagrangeEquation
    (L : ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3) → ℝ)
    (q : ℝ → EuclideanSpace ℝ (Fin 3)) :=
  ∀ t,
     ∇ (x:=q t), L t x (deriv q t) - ∂ (t':=t), ∇ (v:=∂ q t'), L t' (q t') v = 0

For example, ∂ (x':=x;v), f x' says: take derivative of f x' w.r.t. x' at point x in direction v. If direction is missing, e.g. ∂ (x':=x), f x', then it is assumed that x is real number and it is equivalent to ∂ (x':=x;1), f x'.

[Joseph Tooby-Smith]

I would be keen on having the Klein-Gordon equation in HepLean, and its derivation from the Klein-Gordon action via variational methods. (And properties of solutions thereof).

[Joseph Tooby-Smith]

(And also the same for the Dirac equation and the Dirac lagrangian)

[Tomas Skrivan]

Yeah, variational calculus is one thing I'm trying to automate in SciLean. One issue I have encoutered is that physicist usually work with $C^\infty(\mathbb{R}^n)$ which is not Hilbert space and they write for example $\int \|\nabla u(x) \|^2 \, dx$ without specifying the domain of integration and during the derivation ignore the question of boundary conditions.

As the first step I would just derive that $\delta_u \int \|\nabla u(x) \|^2 \, dx = 0$ implies $\Delta u(x) = 0$. Klein-Gordon and Dirac equation is fairly simple extension of that.

[Joseph Tooby-Smith]

I think it usually assumed that the domain of integration is the whole of $\mathbb{R}^n$, and that everything vanishes as it tends to $\infty$.

[Mr Proof]

That's pretty nice. What kind of things can you prove with these equations? Is it fairly straight forward to check solutions by substituting them in the equations?
A lot of the proofs like verifying the equations have certain symmetries seem like fairly trivial cases of substitution followed by simplification. Even checking gauge symmetries... unless I'm missing something. Can you think of any more interesting proofs?
As more of a challenge I would like to see non-abelian Yang-Mills. (Then we're heading towards being able two state two of the Millenium Problems: Yang-Mills . and Navier-Stokes Although the definitions of these problems a a bit open to interpretation.

[Siddharth Bhat]

@Joseph Tooby-Smith I am curious how one formalizes "vanishes at the boundary". It was years after taking gauge theory that I realized that assuming $L^2$ is insufficient: one can have functions in $L^2$ that are comprised of spikes that get "thinner and taller", but don't every decay! I realized this when studying sobolev space theory, which allows one to actually rigorously setup boundary conditions, but is more sophisticated to setup :( So I'm curious if there's an easy way to setup the theory.

[Tomas Skrivan]

I think checking solutions should be quite easy and I'm working on tactic that does differentiation so really the proof should be one line. Difficulty might arise when you are working on some domain or you have to do some non trivial algebraic simplification afterwards

Proofs that should not be too difficult

• check solution
• invariance w.r.t. a coordinate transformation
• conserved quantities
• expressing equations in different coordinate systems

At least these proofs should not be difficult in principle and might be a good test case for CAS(computer algebra system) capabilities of Lean.

[Tomas Skrivan]

Siddharth Bhat said:

Joseph Tooby-Smith I am curious how one formalizes "vanishes at the boundary". It was years after taking gauge theory that I realized that assuming $L^2$ is insufficient: one can have functions in $L^2$ that are comprised of spikes that get "thinner and taller", but don't every decay! I realized this when studying sobolev space theory, which allows one to actually rigorously setup boundary conditions, but is more sophisticated to setup :( So I'm curious if there's an easy way to setup the theory.

I think that all these derivations should just be done in $C^\infty_0(Ω)$. In case of fluid flow, you might have to work with $C^\infty_0(Ω,\mathbb{R}^n)$ for viscid flow or with $\{u : C^∞(Ω, ℝ^n) | ∀ (x : ∂ Ω), N(x)⬝u(x) = 0 \}$ for inviscid flow.

Sobolev spaces is too heavy machinery that is useful if you want to prove existence but it gets in the way when you do just calculations.

[Tomas Skrivan]

Also here I sketched how to state and prove Bernoulli principle if you assume potential and stationary flow.

[Tomas Skrivan]

Tyler Josephson ⚛️ said:

Kim Morrison It has been a while since I dug into this; Moogle tells me multivariable polynomials have partial derivatives.

For example, can we state the Maxwell relations (to be disambiguated from Maxwell's equations; I'm personally more into thermodynamics than electromagnetism)? Fick's Law of diffusion? What about Navier-Stokes?

Some time ago I also sketched how to state/prove Maxwell's relations here

Here is updated code to be more aligned with mathlib:

code

import Mathlib

macro (priority:=high) " ∂ " "(" x:ident ":=" xval:term ")" "," fval:term : term => `((deriv λ $x => $fval) $xval )

-- internal energy -------------------------------------------------------------
variable (U : (S : ℝ) → (V : ℝ) → ℝ)

-- definition of temperature and pressure as functions of entropy and volume
noncomputable
def T_sv (s v) := ∂ (s':=s), U s' v
noncomputable
def P_sv (s v) := - ∂ (v':=v), U s v'


theorem MaxwellRelation1 (s v)
  : (∂ (v':=v), T_sv U s v') = - (∂ (s':=s), P_sv U s' v) :=
by
  unfold T_sv P_sv
  -- swap derivatives and we are done
  admit

-- Enthalpy --------------------------------------------------------------------

-- volume and temperature as functions of entropy and pressure
-- change of variables comming from Legandre transform
noncomputable
def V_sp (s p : ℝ) := (λ v => P_sv U s v).invFun p
noncomputable
def T_sp (s p : ℝ) := T_sv U s (V_sp U s p)


-- Enthalpy
-- H is leganre transform of U w.r.t. to V variable
noncomputable
def H (s p : ℝ) : ℝ := U s (T_sp U s p) - p * T_sp U s p

theorem enthalpy_temperature (s p) : T_sp U s p = (∂ (s':=s), H U s' p) := sorry
theorem enthalpy_volume      (s p) : V_sp U s p = (∂ (p':=p), H U s p') := sorry

theorem MaxwellRelation2 (s p)
  : (∂ (p':=p), T_sp U s p') = (∂ (s':=s), V_sp U s' p) :=
by
  simp only [enthalpy_temperature, enthalpy_volume]
  -- swap derivatives and we are done
  admit


-- Helmholtz -------------------------------------------------------------------

-- entropy and pressure as functions of temperature and volume
noncomputable
def S_tv (t v : ℝ) := (λ s => T_sv U s v).invFun t
noncomputable
def P_tv (t v : ℝ) := P_sv U (S_tv U t v) v


-- Helmholtz free energy
-- F is leganre transform of U w.r.t. to S variable
noncomputable
def F (t v : ℝ) : ℝ := U (S_tv U t v) v - t * S_tv U t v

theorem helmholtz_pressure (t v : ℝ) : P_tv U t v = - (∂ (v':=v), F U t v') := sorry
theorem helmholtz_entropy  (t v : ℝ) : S_tv U t v = - (∂ (t':=t), F U t' v) := sorry

theorem MaxwellRelation3 (t v)
  : (∂ (v':=v), S_tv U t v') = (∂ (t':=t), P_tv U t' v) :=
by
  simp only [helmholtz_pressure,helmholtz_entropy]
  -- swap derivatives and we are done
  admit

One issue is that you can't simply talk about temperature T as function of entropy and volume and after few lines as a function of entropy and pressure. Therefore there is T_sv and T_sp for temperature in terms of entropy/volume and entropy/pressure. Also all of these quantities are function of internal energy U : (S : ℝ) → (V : ℝ) → ℝ that actually defines the system.

[Tomas Skrivan]

Joseph Tooby-Smith said:

I think it usually assumed that the domain of integration is the whole of $\mathbb{R}^n$, and that everything vanishes as it tends to $\infty$.

Yeah this is not nice for formalization because you would need some integrability conditions on all those functions you are working with. Dealing with all those integrability conditions will be really painful especially for non-linear problems. Without these conditions all those integrals might be meaningless. The calculation should be done on some bounded set, then all those integrability conditions go away.

[Mr Proof]

I guess dealing with singularities will also be a challenge. E.g the inverse square law may include a delta function at zero.
So we would need the theory of distributions unless that region was left undefined

[Joseph Tooby-Smith]

@Tomas Skrivan It wouldn't surprise me if that all the integrals are indeed meaningless.
The place these actions appear in physics is in the path integral, and the path integral is certainly ill defined. We never actually compute actions or path-integrals (because we can't). We work with approximations.

One approximation is to use Feynman diagrams, which gives you perturbative quantum field theory. The other is to use the variational principle, which gives you classical field theory.

When a physicist does the variational principle, they literally just stick their Lagrangian into the Euler-Lagrange equations and see what happens.

Thus to the physicist, there little point worrying about what functions these integrals are defined on, because we never calculate these integrals. We have a definition of a field theory (a Lagrangian and some fields), and different ways to approximate that field theory. We give half-hearted attempts to justify these approximations, but until we work out the correct definition of the path integral (e.g. through functorial field theory), this is the best we can do.

[Mr Proof]

I think it's mostly well defined over Euclidean space and you solve things there then make the substitution t->I t at the end (if you're talking about path integrals.)

On QED it is a less known fact that the perturbation series expansion is asymptotic only meaning it converges until about the 137th term then begins to diverge again. So defining QED in terms of Feynmn diagrams can't work. Probably lattice QED is the rigorous definition. (An easier example is expanding out exp(-x^2 - a x^4) in terms of a. It is also an asymptotic expansion only. ) Can we formalise asymptotic expansions? :thinking:

Whether QCD is well defined at all I think is the point of the Yang-Mills Millenium prize problem.

[Tomas Skrivan]

I know nothing about path integrals or Feynman diagrams and I have heard that there are indeed problems with properly formulating them.

What I'm talking about is the derivation that $\delta_u \int \|\nabla u(x) \|^2 \, dx = 0$ implies $\Delta u(x) = 0$. This can be done fully formal but still is a bit challenging as I pointed out. My interest is manly continuum mechanics and thermodynamics where there are none of the path integral issues.

[Notification Bot]

This topic was moved here from #lean4 > Physics in Lean by Patrick Massot.

[Patrick Massot]

@Mr Proof @Joseph Tooby-Smith I moved this discussion because it was still going on and had nothing to do in the lean4 channel whose description is “Questions & discussion around the programming language Lean.” while your discussion has nothing to do with programming in Lean. Please don’t see it as push back. It’s perfectly fine to discuss physics on this zulip, but doing it in the dedicated channel is even better.

[Mr Proof]

Just playing around with the notation, to see what looks nice. Just experiments don't take it too seriously.

Some observations:
I think if we're accepting a function into the div and curl it should also output a function.
I wonder if the right object to work with is (3+1) space-time 𝔼³ × ℝ ?

(Oh I missed the bit where you already had notation like this! But never mind)

import Mathlib

variable {n : ℕ}  {U} [NormedAddCommGroup U] [NormedSpace ℝ U]
open BigOperators EuclideanSpace

/- some notation-/
notation "𝔼^[" N "]"  => EuclideanSpace ℝ (Fin N)
notation "𝔼²" => EuclideanSpace ℝ (Fin 2)
notation "𝔼³" => EuclideanSpace ℝ (Fin 3)
notation "𝔼³⁺¹" => 𝔼³ × ℝ
notation "∂" => deriv
notation "⋆" => flip /-  (⋆φ)(t,x) == φ(x,t)   -/

/-- partial derivative -/
noncomputable
abbrev pderiv (i : Fin n) (u : 𝔼^[n] → U) (x: 𝔼^[n]) : U :=  ∂ (λ (h' : ℝ) => u (x + h' • basisFun (Fin n) ℝ i)) 0

notation "∂[" N "]" => pderiv N

noncomputable
def div (u : 𝔼^[n] → 𝔼^[n]) (x: 𝔼^[n] ) : ℝ  := ∑ i, ∂[i] ( ⋆ u i ) x

notation "∇ •" => div

noncomputable
def curl (u : 𝔼³ → 𝔼³) (x: 𝔼³) : 𝔼³ :=
  ![ ∂[1] (⋆ u 2) x - ∂[2] (⋆ u 1) x,
     ∂[2] (⋆ u 0) x - ∂[0] (⋆ u 2) x,
     ∂[0] (⋆ u 1) x - ∂[1] (⋆ u 0) x]

notation "∇ ×" => curl

def MaxwellEquations
    (ε₀ μ₀ : ℝ)
    (E : ℝ → 𝔼³ → 𝔼³)
    (B : ℝ → 𝔼³ → 𝔼³)
    (ρ : ℝ → 𝔼³ → ℝ)
    (J : ℝ → 𝔼³ → 𝔼³) :=
  ∀ t x,
    ∇ • (E t) x = (ρ t x)/ε₀
  ∧ ∇ • (B t) x = 0
  ∧ ∇ × (E t) x = - ∂ (⋆ B x) t
  ∧ ∇ × (B t) x = μ₀ • (J t x) + ε₀ • ∂ (⋆ E x) t

Trying to prove that these are equivalent to the 4-potential E=∂A-∂A, etc. but it's tricky! Need functions that split space from 𝔼⁴ to ℝx𝔼³

e.g.

noncomputable
def grad [NormedAddCommGroup α][NormedSpace ℝ α] (u : 𝔼³ → α) : (Fin 3) → 𝔼³ → α := ![ ∂[0] u  ,∂[1] u  ,∂[2] u ]

def toSpaceTime {α:Type} (A:(Fin 4)→α):α ×(Fin 3 → α) := (A 0, ![A 1, A 2, A 3])
def to3Vector {α:Type} (A:(Fin 4)→α):(Fin 3 → α) := ![A 1, A 2, A 3]
def timeComponent {α:Type} (A:(Fin 4)→α):α := (A 0)
def to4Vector{α:Type} (A:α × ((Fin 3)→α)):(Fin 4) → α := ![A.1, A.2 0, A.2 1, A.2 2]

def to3VectorInput (A:ℝ → 𝔼³ → u) (y:𝔼⁴) := A (y 0) (to3Vector y)
def to4VectorInput (A:𝔼⁴→ u) (t:ℝ )(x:𝔼³) := A ![t, x 0, x 1, x 2]

/- Try to define the Electromagnetic 3-tensor in terms of the 4-tensor potential -/

def EfromFourPotential (A:𝔼⁴→𝔼⁴): (ℝ → 𝔼³ → 𝔼³) :=
    fun t (y:𝔼³) =>  ( ∂  fun t' =>  to3Vector ( A (to4Vector (t',y)))  ) t     /-  - grad A -/

[Adomas Baliuka]

I think the fact that physiciats never actually compute integrals in going from Lagrangian to Euler-Lagrange equations suggests to me that the integrals are "formal" and should be defined that way (a "synthetic" approach). Then again, there are some applications of the calculus of variations where things are computed explicitly. Is it possible to have the best of both worlds here?

I think that the interesting formalization question for field theory is what are all "allowed manipulations" that physicists want to apply, are they inconsistent, and can one restrict the problem space to make them consistent (I'm not sure if it would be doable to prove in Lean that the manipulations are consistent). Maybe one could "lift" a subset of formal problems to well-defined integrals and prove that the formal manipulations always give the correct result.

[Mr Proof]

Indeed, I agree with the formal approach. Indeed when the fields are fermion fields, they can only be treated formally. With Grasmann integration rules. When the fields are bosonic then you have a choice whether to treat them formally or informally. This relates to the fact that an electromagnetic field can both be treated as a function with values at every place in space time OR as a formal symbol in which the wave function can be expanded to give the separate photon wave functions.

Not sure if Grassmann numbers are formalised in Lean yet (perhaps under a different name? The one dimensional case are called "DualNumber" in Lean)

A lot of text-books kind of "cheat" when discussing infinite integrals in that they first define it over a toroidal space of size L and then let L go to infinity (or at least very large). Infinite integrals are a cheat anyway since the Universe is not infinite if we think about only the region inside the cosmic event horizon.

[Adomas Baliuka]

I'm sure most people here are aware of it but this parallel thread seems highly relevant https://leanprover.zulipchat.com/#narrow/stream/395462-Natural-sciences/topic/Feynman.20diagrams/near/443771599
The two papers referenced there seem like a nice starting point

[Dean Young]

Mario Krenn's post on quantum physics in Lean

[Shreyas Srinivas]

I am very curious to know how that kind of pay for work is legal in German law relating to scientific employment. That's more than a postdoc's salary (netto) for roughly 2.5 months.

[Lode Vermeulen]

I believe the funding is not there anymore. I am actually doing work on this for my thesis (and some others have worked on this as well before me).

[Joseph Tooby-Smith]

@Lode Vermeulen Nice! Any of this work public?

[Lode Vermeulen]

Yes, some lean3 code about this written by Kevin Miller (and some others I believe): https://github.com/leanprover-community/mathlib/blob/kmill_hamiltonian/src/hamiltonian2.lean. And some (very very messy) code which I have contributed to in Lean 4: https://github.com/LodeVermeulen/Lean4_Bogdanovs_lemma.
I am now at the end of my project though, and Mathlib kind of lacked some graph theory necessary to prove Bogdanovs lemma (the goal of this project), so I also contributed there a little bit.

[Joseph Tooby-Smith]

Nice! Many thanks for sharing :)

[Dean Young]

Mr Proof said:

Indeed, I agree with the formal approach. Indeed when the fields are fermion fields, they can only be treated formally. With Grasmann integration rules. When the fields are bosonic then you have a choice whether to treat them formally or informally. This relates to the fact that an electromagnetic field can both be treated as a function with values at every place in space time OR as a formal symbol in which the wave function can be expanded to give the separate photon wave functions.

Not sure if Grassmann numbers are formalised in Lean yet (perhaps under a different name? The one dimensional case are called "DualNumber" in Lean)

A lot of text-books kind of "cheat" when discussing infinite integrals in that they first define it over a toroidal space of size L and then let L go to infinity (or at least very large). Infinite integrals are a cheat anyway since the Universe is not infinite if we think about only the region inside the cosmic event horizon.

Out of curiosity, these integrations are not subsumed by integration with values in l₂(ℝ) or l₂(ℂ)?

[Mr Proof]

@E. Dean Young I'm not sure. I don't know what the fields l₂(ℝ) do. Grassmann integration is generally only defined for improper integrals. (Which are coincidentally equivalent to Grasmann differentiation). e.g.

∫ ∫ (a+bθ₁ + cθ₂ + dθ₁θ₂) dθ₁dθ₂ = d

θ₁θ₂ = -θ₂θ₁

(θ₁)^2 = (θ₂)^2 = 0

[Dean Young]

@Mr Proof

Sorry I forgot to reply to this. I was unfamiliar with how the exterior algebra is called a grassman.