# Zulip Chat Archive

## Stream: general

### Topic: Formalizing Chemical Theory pt. 2

#### Max Bobbin (Sep 18 2022 at 17:57):

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 (Sep 18 2022 at 18:20):

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 (Sep 18 2022 at 18:36):

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 (Sep 18 2022 at 18:38):

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 (Sep 18 2022 at 18:49):

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 (Sep 18 2022 at 18:53):

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 (Sep 18 2022 at 18:54):

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 (Sep 18 2022 at 18:55):

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

#### Eric Wieser (Sep 18 2022 at 19:09):

Unicode has no subscript d

#### Moritz Doll (Sep 18 2022 at 19:16):

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 (Sep 18 2022 at 19:23):

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 (Sep 18 2022 at 19:34):

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 (Sep 18 2022 at 19:51):

Another observation; your`zero_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 ⚛️ (Sep 18 2022 at 22:14):

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 (Sep 18 2022 at 23:37):

Your `motion_cont_diff_everywhere`

typeclass has a field which is false too

#### Max Bobbin (Sep 19 2022 at 01:13):

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 (Sep 19 2022 at 01:15):

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 isfalse(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 thatas it standsyou 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 (Sep 19 2022 at 01:25):

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 (Sep 19 2022 at 05:47):

`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 (Sep 19 2022 at 08:22):

I think with similar reasoning, `thermo_system`

should be structure not a class

#### Tomas Skrivan (Sep 19 2022 at 08:41):

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 (Sep 19 2022 at 14:00):

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 (Sep 19 2022 at 14:59):

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 (Sep 19 2022 at 15:00):

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 (Sep 19 2022 at 15:03):

I will try that out, thanks for the suggestion

#### Max Bobbin (Sep 19 2022 at 16:06):

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 (Sep 19 2022 at 16:08):

`class`

is syntax for `@[class] structure`

, so in some sense the question is "when do I need `@[class]`

?"

#### Eric Wieser (Sep 19 2022 at 16:11):

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 (Sep 19 2022 at 16:56):

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 (Sep 19 2022 at 18:05):

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 ⚛️ (Oct 24 2022 at 17:44):

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

Last updated: Aug 03 2023 at 10:10 UTC