theorem Boyle in Lecture1.lean isn't boyle's law

Stream: Lean for Scientists and Engineers 2024

[Bulhwi Cha]

Bulhwi Cha said:

import Mathlib.Data.Real.Basic

lemma Boyle
    -- Variables
    (P1 P2 V1 V2 T1 T2 n1 n2 R : ℝ)
    -- Assumptions
    (a1 : P1 * V1 = n1 * R * T1)
    (a2 : P2 * V2 = n2 * R * T2)
    (a3 : T1 = T2)
    (a4 : n1 = n2) :
    -- Conjecture
    P1 * V1 = P2 * V2 := by
  rw [a3] at a1
  rw [a4] at a1
  exact (rfl.congr (Eq.symm a2)).mp a1

lemma just_a_random_example (x₁ x₂ y₁ y₂ z₁ z₂ w₁ w₂ k : ℝ)
    (h₁ : x₁ * y₁ = w₁ * k * z₁) (h₂ : x₂ * y₂ = w₂ * k * z₂)
    (h₃ : z₁ = z₂) (h₄ : w₁ = w₂) : x₁ * y₁ = x₂ * y₂ := by
  rw [h₁, h₂, h₃, h₄]

theorem Boyle_is_just_a_random_example : Boyle = just_a_random_example := rfl

I think the lemma Boyle should be removed from LeanChemicalTheories. It's not a correct formalization of Boyle's law; it's merely an example of using rewriting. We need to formally define the pressure and the volume of a confined ideal gas. Then we should use those definitions to state Boyle's law correctly in Lean. But currently, I have no idea how to define them.

Bulhwi Cha said:

Quote

Perhaps the following code will further clarify that the lemma Boyle is equal to some statement that doesn't describe the relationship between pressure and volume of a confined gas. In the lemma this_isn't_Boyle, the real variable R_mul_inv represents the reciprocal of R, the gas constant.

import Mathlib.Data.Real.Basic

lemma Boyle
    -- Variables
    (P1 P2 V1 V2 T1 T2 n1 n2 R : ℝ)
    -- Assumptions
    (a1 : P1 * V1 = n1 * R * T1)
    (a2 : P2 * V2 = n2 * R * T2)
    (a3 : T1 = T2)
    (a4 : n1 = n2) :
    -- Conjecture
    P1 * V1 = P2 * V2 := by
  rw [a3] at a1
  rw [a4] at a1
  exact (rfl.congr (Eq.symm a2)).mp a1

lemma this_isn't_Boyle
    -- Variables
    (n1 n2 T1 T2 V1 V2 P1 P2 R_mul_inv : ℝ)
    -- Assumptions
    (a1 : n1 * T1 = P1 * R_mul_inv * V1)
    (a2 : n2 * T2 = P2 * R_mul_inv * V2)
    (a3 : V1 = V2)
    (a4 : P1 = P2) :
    -- Conjecture
    n1 * T1 = n2 * T2 := by
  rw [a1, a2, a3, a4]

theorem Boyle_eq_this_isn't_Boyle : Boyle = this_isn't_Boyle := rfl

[Tyler Josephson ⚛️]

Thanks for linking this! We'll discuss this tomorrow :)

[Bulhwi Cha]

I think you should refrain from using theorems that aren't correctly formalized for lectures.

[Tyler Josephson ⚛️]

Do you have any you'd like to contribute? My group is coming up with problems and we'd love to have more to choose from!

[Tyler Josephson ⚛️]

Keep in mind, examples need to fit somewhere in the schedule. So, for example, since we're avoiding topology, that means no filters.

[Tyler Josephson ⚛️]

Also, this is the perfect place to share any of your thoughts on syntax and semantics, something we're discussing tomorrow at length. I understand that you joining live isn't really feasible since it's in the middle of the night in South Korea, but the conversation can continue on Zulip.

[Bulhwi Cha]

Tyler Josephson ⚛️ said:

Do you have any you'd like to contribute? My group is coming up with problems and we'd love to have more to choose from!

I feel frustrated because I still don't have a clue about how to formalize Boyle's law. I have so much to do before attempting to formalize classical mechanics or thermodynamics. Right now, I'm continuing to learn C programming. After I finish it, I'll study undergraduate and graduate mathematics.

[Christian Tzurcanu]

@Bulhwi Cha may you give here an example of a theorem that you consider correctly formalized, for contrast?

[Christian Tzurcanu]

to note: the utility of "starting in the middle" as touched also in lecture 1 is high: you do not need to be completely rooted in previous formalizations and still reap benefits.
In this case: just showing the mechanics of the reasoning in Lean has already significant pedagogic benefits.

If we can find something that is by consensus correctly formalized that is as easy to start and as well-known as Boyle's Law, we can make an attempt to improve the lesson even further. That information would be considered constructive criticism.

[Bulhwi Cha]

Christian Tzurcanu said:

Bulhwi Cha may you give here an example of a theorem that you consider correctly formalized, for contrast?

As I said earlier, I don't have any examples. I've tried to make one but failed so far.

[Bulhwi Cha]

But I can give you an example of a wrong way to formalize classical mechanics: https://leanprover.zulipchat.com/#narrow/stream/395462-Natural-sciences/topic/defining.20the.20force.20applied.20to.20a.20mass.20pulling.20a.20string/near/450381079.

[Bulhwi Cha]

Christian Tzurcanu said:

In this case: just showing the mechanics of the reasoning in Lean has already significant pedagogic benefits.

We could've achieved this using the following example instead of theorem Boyle:

lemma just_a_random_example (x₁ x₂ y₁ y₂ z₁ z₂ w₁ w₂ k : ℝ)
    (h₁ : x₁ * y₁ = w₁ * k * z₁) (h₂ : x₂ * y₂ = w₂ * k * z₂)
    (h₃ : z₁ = z₂) (h₄ : w₁ = w₂) : x₁ * y₁ = x₂ * y₂ := by
  rw [h₁, h₂, h₃, h₄]

[Bulhwi Cha]

Christian Tzurcanu said:

If we can find something that is by consensus correctly formalized that is as easy to start and as well-known as Boyle's Law, we can make an attempt to improve the lesson even further. That information would be considered constructive criticism.

[Bulhwi Cha]

I haven't found a formalized library of classical mechanics and thermodynamics. I can only say about my rough plan to formalize them: drawing inspiration from physics-based simulation software such as Chrono. I want to understand the underlying theories behind it.

[Kim Morrison]

(Disclaimer: I think physics should be done from the very bottom, with no fear of mathematical sophistication.)

I think the place to start doing physics is:

• Define the characters (wrong name, oops) of an algebra (if we don't already have this??) as the subset of linear functionals preserving 1.
• Define the states of a star algebra as the subset of characters preserving positive elements.
• Prove basic properties, e.g. convexity.
• Do an example, e.g. identifying the states of 2x2 complex matrices as the Bloch sphere.
• etc: states in tensor products ("disjoint systems"), states on commutative algebras ("classical"), sufficient development of C* and vN algebras to state GNS and define vector states ("Hilbert space QM")

In my admittedly twisted view of the world, this is genuinely physics, doable at the moment with the present state of formalised material, and a viable path towards more physics.

[Joseph Tooby-Smith]

@Kim Morrison I agree that there should be no fear of mathematical sophistication when doing physics. But I think one needs to be careful, as there is no single 'bottom' for physics. In other words it is not (currently) possible to reach every bit of physics from a single (mathematical or physics) theory.

When formalising physics in Lean I think it is really important to ask "what is the goal". There are two main ones I see. Firstly, to "digitalise physics" i.e. to write results from the literature into lean in a way that is easy to use to derive new results and check calculations etc (and in the correct mathematical language). Secondly, to "formalise physics" i.e. to provide a solid-interconnected library of results founded on a single mathematical principle.

IMO, the former is (currently) more useful to the working physicist, whilst the latter would be near impossible given the state of the physics literature.

[Kim Morrison]

I think the lack of a single bottom is a distraction. There are similarly "bottoms" for some versions of QFT, stat mech, classical mechanics, etc. The example I gave of a starting place was illustrative (and dear to my heart).

[Kim Morrison]

I'm very skeptical of formalisation that doesn't start from the bottom up. e.g. compare the relative outcomes of formal abstracts and mathlib.

[Kim Morrison]

I think another great "bottom" (and that would have some enthusiasm from mathematicians) is developing some symplectic geometry ("Hamiltonian mechanics").

[Kim Morrison]

I know that the people behind the manifolds library are excited to go in this direction, although I'm not sure if there are technical roadblocks or just availability of competent people to do the setup.

[Joseph Tooby-Smith]

I agree. I misunderstood your original message. I agree that starting at the 'bottom' of a given theory (e.g. starting with the foundation of stat mech and deriving thermodynamics) is the best way of doing things, if your goal is to create a robust library which stands the test of time. If your goal is to convince other scientists that using Lean is a good idea, then other social factors come into play.

[Kim Morrison]

I shouldn't have said "the place", but rather "a place", sorry for the confusion. What I should have said instead of "the" is that this particular place already has many of the mathematical prerequisites in place, and the foundational definitions are clear, so it is a good place to start.