Formalizing Chemical Theory pt. 2

Stream: general

[Max Bobbin]

We are excited to announce the culmination of several months of work. Lean Chemical Theories has been a project the ATOMS lab has worked on for a while now, and some of you may remember a previous post we had done. Since then, we have made many changes to our code and advancements in our understanding of Lean. Now we have finished our first paper, Formalizing_Chemical_Theory.pdf aimed at exploring the use of Lean for scientific mathematical formulation. This paper is aimed at scientists to get them interested in using theorem provers for scientific purposes, mainly formalizing the math behind scientific theories. Our paper focuses on our formalization of two adsorption models, kinematics, and thermodynamics. The paper is styled as a tutorial on using Lean, meaning we choose to keep some proofs (like the Langmuir proof) simple for readability while sacrificing applicability (although we do talk about ways to improve on that proof in the supplementary section).
We are definitely excited to see how the scientific community reacts and to collaborate with others as we continue with this project. We are also excited about the next steps we want to take. Some of you may remember my post about formalizing dimensional analysis. While I have started entirely redoing our code (and am sure I will be back soon in Zulip asking for guidance :big_smile: ), I am excited about what we will be able to achieve. We are also looking at expanding our formalization of thermodynamics and classical mechanics, with a long-term goal of tackling parts of Noether's theorem.
We wanted to share the project with the Lean community to get some feedback on our code and to give an update on our project. Attached Is a link to our code and a draft of our paper.

This project has been possible with the work of @Samiha Sharlin ⚛️ @Parivash @Catherine Wraback @An Hong Dang along with our P.I. @Tyler Josephson ⚛️

[Kevin Buzzard]

Everything in Lean is a Type, whether natural numbers or real numbers, functions, Boolean conditions, or even entire proofs.

I think it would be more accurate to say that everything in Lean is a term of a type. For example the real numbers are a type, but the real number $\pi$ is not itself a type, it is a term of type $\R$.

[Kevin Buzzard]

In your code you have a lot of repetition, for example you prove
filter.tendsto (λ x : ℝ, x^7/x) (nhds_within 0 (set.Ioi 0)) (nhds 0) and then filter.tendsto (λ x : ℝ, x^8/x^2) (nhds_within 0 (set.Ioi 0)) (nhds 0) and then filter.tendsto (λ x : ℝ, x^9/x^3) (nhds_within 0 (set.Ioi 0)) (nhds 0) and so on. It would be much more compact to prove a more general result involving x^a/x^b, just once, and then deducing all of these theorems from the more general case. In fact this is in some sense what formalisation is encouraging you to do -- instead of doing similar work multiple times, figure out the common general result and just prove it once.

[Kevin Buzzard]

There is a problem with theorem tendsto_at_top_at_zero_radius. Right now one of your hypotheses is (hx : ∀ x, x ∈ {r : ℝ | r ≠ 0}), and this hypothesis is false (because x could be zero), which means that if you assume it then you can deduce any conclusion at all. No doubt this is just a misstatement of what you actually mean but it does mean that as it stands you will never be able to apply this theorem in a useful situation because you will never be able to supply a proof of hx in any application.

[Kevin Buzzard]

My final comment is: do you think you'll be able to publish this kind of work? Is there anywhere in the chemistry ecosystem which would be interested in your work? I am only asking because I know nothing about the chemistry ecosystem!

[Kevin Buzzard]

Oh, actually, one more comment:it's very frustrating that you can't write $r_{ad}$ for your variable name in Lean (so you can make the code look more like the informal text). Is the problem that "subscript d" is not a thing in unicode or that it's there but there's just no short cut for it in VS Code?

[Andrew Yang]

An interesting approach to formalizing classical thermodynamics (and especially the second law) would be to follow Carathéodory's formalization. Buchdahl's book is also a great reference on this approach.

[Andrew Yang]

This would also be a great test to the manifold and differential forms library of mathlib.

[Eric Wieser]

Unicode has no subscript d

[Moritz Doll]

Andrew Yang said:

This would also be a great test to the manifold and differential forms library of mathlib.

We have differential forms already?

[Eric Wieser]

Your motion_cont_diff_everywhere typeclass has a field which is false too:

∀ (n : with_top ℕ) (m : ℕ), ↑m < n ∧ cont_diff 𝕜 n (deriv^[m] motion.position)

or from the paper, section 3.5:

The field contdiff states that for all n, defined as a natural number including positive infinity, and for all m, defined as a natural number, m is less than n, and the mth derivative of position is continuously differentiable n-times. The carrot [sic] symbol is the logical symbol for and, which requries both sides to true.

with counterexample m = n = 0. I assume you meant:

∀ (n : with_top ℕ) (m : ℕ) (h : ↑m < n), cont_diff 𝕜 n (deriv^[m] motion.position)

[Eric Wieser]

Even the motion typeclass it derives from is quite strange; motion real (fin 3 -> real) as a typeclass means "there is a canonical position trajectory associated with 3D spacetime" aka that there is a particle that is more canonical than any other particle. Thankfully it's at least not uninhabitable though!

[Eric Wieser]

Another observation; yourzero_lt_rpow hx hy exists already as docs#real.rpow_pos_of_pos hx. It can sometimes be hard to guess whether the zero_lt or pos naming convention is used.

[Tyler Josephson ⚛️]

Kevin Buzzard said:

My final comment is: do you think you'll be able to publish this kind of work? Is there anywhere in the chemistry ecosystem which would be interested in your work? I am only asking because I know nothing about the chemistry ecosystem!

Thanks for the feedback! We wondered for a bit where to submit this, since the concept is pretty new. We'll first submit it to ACS Central Science, a general-purpose journal that I've found has been receptive to promising new areas, like when machine learning + chemistry was an up-and-coming thing. We'll also post it to the arXiv and share it on Twitter after a final round of edits with y'all's feedback, which should also generate interest.

[Eric Wieser]

Your motion_cont_diff_everywhere typeclass has a field which is false too

[Max Bobbin]

Kevin Buzzard said:

In your code you have a lot of repetition, for example you prove
filter.tendsto (λ x : ℝ, x^7/x) (nhds_within 0 (set.Ioi 0)) (nhds 0) and then filter.tendsto (λ x : ℝ, x^8/x^2) (nhds_within 0 (set.Ioi 0)) (nhds 0) and then filter.tendsto (λ x : ℝ, x^9/x^3) (nhds_within 0 (set.Ioi 0)) (nhds 0) and so on. It would be much more compact to prove a more general result involving x^a/x^b, just once, and then deducing all of these theorems from the more general case. In fact this is in some sense what formalisation is encouraging you to do -- instead of doing similar work multiple times, figure out the common general result and just prove it once.

That is true and that is a plan, sorry there should've been a comment in there explaining that. I was just in a time crunch to prove that result of lennard jones and brute forced the method. I plan to return to it eventually.

[Max Bobbin]

Kevin Buzzard said:

There is a problem with theorem tendsto_at_top_at_zero_radius. Right now one of your hypotheses is (hx : ∀ x, x ∈ {r : ℝ | r ≠ 0}), and this hypothesis is false (because x could be zero), which means that if you assume it then you can deduce any conclusion at all. No doubt this is just a misstatement of what you actually mean but it does mean that as it stands you will never be able to apply this theorem in a useful situation because you will never be able to supply a proof of hx in any application.

Yes, I am aware of that. I was running into a lot of problems applying theorems about the lennard-jones derivative due to the discontinuity and that was a version I got to in order to get things to work. Thats also on the to-do list to fix

[Max Bobbin]

Eric Wieser said:

Even the motion typeclass it derives from is quite strange; motion real (fin 3 -> real) as a typeclass means "there is a canonical position trajectory associated with 3D spacetime" aka that there is a particle that is more canonical than any other particle. Thankfully it's at least not uninhabitable though!

Could you elaborate on what you mean? I don't understand what you mean by a particle is more canonical than any other. Also, I will make those fixes to the cont_diff part

[Jireh Loreaux]

motion is a data-carrying type class. As such, up to definitional equality, there should only be one instance of that your class on a given type (otherwise Lean will not know which of the different instances to prefer). For this reason, data-carrying classes should only be used when there is a "canonical" instance for each type.

In particular, position is one of the data-carrying fields. So, for example, there should only be one instance of motion real (fin 3 -> real), and hence only one position in 3d space. So only one canonical particle in 3d space.

In this case, my guess would be that you probably just want motion to be a structure which takes the inner product space as an argument instead of extending that class.

[Tomas Skrivan]

I think with similar reasoning, thermo_system should be structure not a class

[Tomas Skrivan]

The fourth kinematic equation, Equation 20, uses the inner product. ... we were unable to prove
Equation 20 for complex time.

You must be talking about the Equation 19 not 20. With complex numbers, Equation 19 should be $v^2(t) = v_0^2 + \mathbb a \cdot \mathbb d + \mathbb d \cdot \mathbb a$ (It should work if I didn't make a mistake on paper). Over real numbers we have $\mathbb a \cdot \mathbb d = \mathbb d \cdot \mathbb a$ so the equation reduces to the Equation 19 as stated. Also I'm probably blind, but I do not see the definition of $\mathbb d$, I had to check wikipedia to figure out what it means.

[Max Bobbin]

Tomas Skrivan said:

The fourth kinematic equation, Equation 20, uses the inner product. ... we were unable to prove
Equation 20 for complex time.

You must be talking about the Equation 19 not 20. With complex numbers, Equation 19 should be $v^2(t) = v_0^2 + \mathbf a \cdot \mathbf d + \mathbf d \cdot \mathbf a$ (It should work if I didn't make a mistake on paper). Over real numbers we have $\mathbf a \cdot \mathbf d = \mathbf d \cdot \mathbf a$ so the equation reduces to the Equation 19 as stated. Also I'm probably blind, but I do not see the definition of $\mathbf d$, I had to check wikipedia to figure out what it means.

I will check to see if the equation is wrongly referenced, but we found out that the equation only works for real numbers and not complex numbers, which is what we discuss in the paper. In contrast, all the other equations worked fine for complex numbers, but that's because they didn't use the inner product

[Tomas Skrivan]

I would suggest changing Equation 19 to $v^2(t) = v_0^2 + \mathbf a \cdot \mathbf d + \mathbf d \cdot \mathbf a$, then I'm fairly confident it can be proven even in the complex case. After that you change the discussion such that the formalization guards you from doing incorrect generalizations of Torricelli's equation from real to complex numbers, or something along those lines.

[Tomas Skrivan]

You can also prove that over the reals numbers it reduces to the original form of Torricelli's equation, $v^2(t) = v_0^2 + 2 \mathbf a \cdot \mathbf d$.

[Max Bobbin]

I will try that out, thanks for the suggestion

[Max Bobbin]

I asked this before in a different post, but I didn't fully understand it; what is the difference between structure and class. I see that you all mentioned something about data-carrying. What does that mean?

[Eric Wieser]

class is syntax for @[class] structure, so in some sense the question is "when do I need @[class]?"

[Eric Wieser]

A simple rule of thumb is "Am I ever going to write instance : my_type X := _?" If the answer is not a strong yes, then you should not make my_type a class.

[Kevin Buzzard]

Every class has at most one instance, not so for structures. As Eric said, a class is just a structure with a tag attached to it (the @[class] "I am a class" tag). The basic example I use to explain the difference to mathematicians is: it's very rare in maths to define two multiplications on the same set (e.g. if $x$ and $y$ are real numbers, then you want $x\times y$ to mean usual multiplication and it would be unwise to start defining another one), so things like has_mul and group are classes. But groups typically have many subgroups -- given one group you might well want to talk about two subgroups of it; this would not be abnormal. So subgroup is a structure but not a class.

[Patrick Stevens]

Or: in some sense, it's reasonable to say that there's "only one way" a set is finite - either it's finite or it isn't - so there's no need for any data associated with that fact, it's just a fact. Knowing that there is a proof of finiteness is enough; you never care what the proof is. So it would be reasonable to represent "ways in which a set is known to be finite" as a class, because we don't care about any differences between proofs of finiteness.

But most structures are not meaningfully classes: for most structures, we do care about the differences between objects of that structure type. For example, a tuple is (morally) a structure, and most times you use a tuple in day-to-day programming, you do so because you want your program to choose what to do based on what specific data lives inside the tuple. (It's meaningful to create different tuples, all with the same type, which are different in ways we actually care about!) Classes are in some sense the "unusual" thing.

[Tyler Josephson ⚛️]

Update - as recommended, we changed all of our classes to structures, and incorporated some other feedback as well. We posted this manuscript to the arxiv - thanks everyone for helping us get this far!

https://arxiv.org/abs/2210.12150