Derivations, CAS, Lean, and Assumptions in Physics

Initially the Physics Derivation Graph documented expressions as Latex. Then SymPy was added to support validation of steps (is the step self-consistent) and dimensionality (is the expression self-consistent?). 

Recently I learned that Lean could be used to prove each step in a derivation. The difference between a Computer Algebra System (e.g., SymPy) and Lean is whether "a = b  --> a/b = 1" is a valid step -- it isn't when b is zero. Lean catches that; SymPy does not. 

While Lean proofs sound like the last possible refinement, there are two additional complications to account for not addressed by Lean. 

Challenge: Bounded ranges of applicability

In classical mechanics the relation between momentum, mass, and velocity is "p = m v". That hold when "v << c". Near the speed of light we need to switch to relativistic mass, 

m = m_{rest} / sqrt{1-((v^2)/(c^2))}.

The boundary between "v << c" and "v ~ c" is usually set by the context being considered. 

One response for users of Lean would be to always use the "correct" relativistic equation, even when "v << c."  A more conventional approach used by Physicists is to use

p = m v, where v << c

then drop the "v << c" clause and rely on context.

Challenge: Real versus Float versus experimental characterization

Lean forces you to characterize numbers as Real or Integer or Complex. This presents a problem for numerical simulations that have something like a 64 bit float representation.

In thermodynamics we assume the number of particles involved is sufficiently large that we focus on the behavior of the ensemble rather than individual particles. The imprecision of floats is not correct, but neither is the infinite precision assumed by Real numbers. 

Example applications of Lean proofs needing bounds on values

Math doesn't have convenient ways of indicating "finite precision, as set by the Plank scale."  The differential element used in calculus cannot actually go to zero, but we use that concept because it works at the scales we are used to. 

Physicists make simplifying assumptions that sometimes ignore reality (e.g., assuming continuous media when particles are discrete). Then again the assumption that particles are discrete is also a convenient fiction that ignores the wavefunction of quantum mechanics. 

Lean can be used to prove derivations in classical mechanics, but to be explicit about the bounds of those proofs we'd also need to indicate "v << c" and "assume space is Euclidean." 

For molecular dynamics, another constraint to account for is "temperature << 1E10 Kelvin" or whatever temperature the atoms breaks down into plasma. 

Distinguishing the context of (classical mechanics from quantum) and (classical from relativistic) and (conventional gas versus plasma) seems important so that we know when a claim proven in Lean is applicable. 

example interaction with ChatGPT 3.5 to produce a Lean proof

In a new conversation I provided the following prompt:

prompt

Answer the question based on the context below. Let's work this out in a step by step way to be sure we have the right answer.

Context: Lean is a proof assistant and programming language. Lean is based on the calculus of constructions with inductive types.

Context: There are multiple versions of Lean. This question is about Lean 4

`a=b` is a proposition. The variable `a` is Real valued and `b` is Real valued. Prove in version 4 of Lean that `(a=b) -> (a+2=b+2)`

ChatGTP 3.5 wrote in response

ChatGPT 3.5 response

Certainly! To prove the statement `(a = b) -> (a + 2 = b + 2)` in version 4 of Lean, you can follow these steps:

1. **Introduction of Variables**: Begin by introducing the variables and assumptions using the `variables` keyword. In this case, you have the variables `a` and `b` both being Real valued.

```lean
variables {a b : ℝ}

```

2. **Assumption**: State the assumption that `(a = b)`.

```lean
example (h : a = b) : a + 2 = b + 2 :=

```

3. **Transformation**: Use the assumption to transform the left-hand side of the conclusion `(a + 2)` to `(b + 2)` using the property of equality.

```lean
calc
   a + 2 = b + 2 : by rw h

```

Here, `calc` is used to chain together a sequence of expressions, and `rw h` applies the assumption `h`.

4. **QED (Quod Erat Demonstrandum)**: Conclude the proof.

```lean
   example (h : a = b) : a + 2 = b + 2 :=
   begin
     calc
       a + 2 = b + 2 : by rw h
   end

```

This step-by-step approach uses the Lean proof style to demonstrate the validity of the given proposition. The `calc` tactic is particularly useful for chaining together equalities.

On my computer I created a file "second_chatGPT_attempt.lean" and wrote

variables {a b : ℝ}

example (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end

and then ran

docker run -it --rm -v `pwd`:/scratch --workdir /scratch lean3onubuntu lean --run second_chatGPT_attempt.lean
second_chatGPT_attempt.lean:2:0: error: unexpected identifier; expected command
second_chatGPT_attempt.lean:5:0: error: unknown identifier 'begin'
second_chatGPT_attempt.lean:6:2: error: unexpected token 'calc'; expected command
second_chatGPT_attempt.lean:8:0: error: invalid 'end', insufficient scopes

I then told ChatGPT

prompt

When I run the script

```lean
variables {a b : ℝ}

example (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end

```

Lean 4 returns an error message: `error: unexpected identifier; expected command`

What should I do to fix the error?

ChatGPT 3.5 response

Apologies for the oversight. It seems I made an error in my previous responses. In Lean, you should use `theorem` or `example` as part of the proof declaration. Here's the corrected version:

```lean
variables {a b : ℝ}

theorem add_two_eq_add_two (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end

```

In this corrected version, I replaced `example` with `theorem`. You can use `example` as well, but `theorem` is more appropriate when proving statements. This should resolve the error you encountered.

I then created a second Lean script, third_chatGPT_attempt.lean, and wrote

variables {a b : ℝ}

theorem add_two_eq_add_two (h : a = b) : a + 2 = b + 2 :=
begin
  calc
    a + 2 = b + 2 : by rw h
end

which got the same error as before when I attempted to run the script using Lean 4:

docker run -it --rm -v `pwd`:/scratch --workdir /scratch lean3onubuntu lean --run third_chatGPT_attempt.lean 
third_chatGPT_attempt.lean:1:0: error: unexpected identifier; expected command
third_chatGPT_attempt.lean:4:0: error: unknown identifier 'begin'
third_chatGPT_attempt.lean:5:2: error: unexpected token 'calc'; expected command
third_chatGPT_attempt.lean:7:0: error: invalid 'end', insufficient scopes
  

HTML arxiv papers, semantic tagging, and formal verification

arxiv recently started experimenting with converting .tex files to HTML: https://info.arxiv.org/about/accessible_HTML.html

The first official announcement was in February 2022:
https://blog.arxiv.org/2022/02/21/arxiv-articles-as-responsive-web-pages/

The HTML from .tex effort is a collaboration between Deyan Ginev (a student of Dr. Kohlhase) and Bruce Miller (at NIST - https://www.nist.gov/people/bruce-r-miller). Kohlhase's group (https://kwarc.info/research/) focuses on semantic enrichment of Latex. Bruce provided the software to convert Latex.

The reason for this Latex to HTML conversion is because it's the first step for enabling semantic enrichment of content on the arxiv. There's immediate benefit for arxiv being able to support HTML, which I suspect is why arxiv cooperated with Kohlhase's group.

In the long term I see a need to connect semantic tagging (the focus of Kohlhase's group) with formal verification (e.g., derivations-as-proofs using Lean). The formally verified math expressions need to be tied to use in narrative text (e.g., arxiv papers). For example, if I'm referring to "x" in a publication, is that the same "x" specified in a Lean-based proof? One way of answering is to use tags like

<unique_variable_id=42>x</unique_variable_id>
 

in the narrative text document, and then have Lean reference the ID 42 in derivations. There are more conventional uses of tags like

<properties name_of_variable="distance" dimension_of_variable="length">x</properties>

but those tags don't address the question of whether two variables refer to the same concept.

Summary

I predict that the conversion of arxiv .tex files to HTML will enable semantic tagging. This will intersect with the challenge of "how do I relate the use of variables and expressions across multiple proofs in Lean?"

software for numerical calculations of derived expressions versus implementation of an algorithm

Suppose I have a Python program that takes "angle" and "initial speed" as arguments and calculates where a ball shot from a cannon lands. The program could be described using the function

f(\theta, s) = d

where \theta is the angle, s is the speed, and d is the distance from the cannon where the ball lands. The function could be expressed using a variety of languages like Python, C, Lean, etc.

If f(\theta, s) = d is derived from the equations of motion (like https://derivationmap.net/review_derivation/201726/) and each step is verified using Lean (as described in this post), then we can use Lean to calculate d from \theta and s. The difference would be that there's more explanation of where the result came from. Rather than just "here the equation to use," including the derivation step and proof of each step makes the assumptions explicit and the implementation correct. 

All software programs can be described as functions that take arguments and return results. That doesn't mean that all functions are derived. As an example of software that is a function but isn't derived, consider the A* routing algorithm. An algorithm outlines a sequence of steps for accomplishing a function.

While all programs could be written in Lean (because each program is a function), not all functions are derived mathematically. As a trivial example, printing "hello world" is not a derived function. In contrast, the first example in this post, the distance a projectile flies, is derived from the equations of motion. What distinguishes "hello world" and A* routing from the cannon ball trajectory?

The distinction is that the cannon ball example is a numerical simulation of a tangible scenario, whereas "hello world" is not describing physically-constrained reality. 

For numerical simulations, Lean can formally verify the derivation and the formula used for analytical calculation. Keeping both aspects in Lean results in a clear chain of custody. 

For algorithms (e.g., A* routing, "hello world"), the verification is to show that the implementation is consistent with the requirements. Here languages like Dafny and F* are relevant.

More on F*:

• https://en.wikipedia.org/wiki/F*_(programming_language)
• https://www.microsoft.com/en-us/research/project/the-f-project/
• https://github.com/FStarLang/FStar
• https://www.fstar-lang.org/
• https://fstarlang.github.io/

More on Dafny:

• https://en.wikipedia.org/wiki/Dafny
• https://www.microsoft.com/en-us/research/wp-content/uploads/2008/12/dafny_krml203.pdf
• https://homepage.cs.uiowa.edu/~tinelli/classes/181/Fall15/Papers/Lein13.pdf
• https://dafny.org/

Floats in Lean

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/floats.20vs.2E.20reals

float is not a ring.

Nor is there an injection; inf is not a real

https://github.com/verified-optimization/CvxLean/blob/main/CvxLean/Tactic/Solver/Float/RealToFloat.lean

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Real.20to.20float.20translation

relation between Inference Rules in the Physics Derivation Graph and Proofs in Lean

In this post I explore the concept that each derivation can be phrased as a proof of the initial declaration and the final result. Also, each step in a derivation can be phrased as a proof.

Lean Proofs of Derivation Steps

As per https://stackoverflow.com/questions/41946310/how-to-prove-a-b-%E2%86%92-a-1-b-1-in-lean Lean can prove that

(a=b) -> (a+1=b+1)

In comparison, a PDG Inference Rule is more generic:

add __ to both sides of (LHS=RHS) to get (LHS+__=RHS+__)

The PDG Inference Rule is generic because the types of LHS and RHS are undefined. Are they Real? Complex? Matrices?

The relevance of types for inference rules is because mixing types may not work. "Add 1 to both sides of (LHS=RHS)" won't work if LHS and RHS are 2x2 matrices.  

Translating between Physics Derivation Graph concepts and features in the Lean Theorem prover

In the blog post I try to figure out how all of those concepts map to features in Lean Theorem prover.

Concepts and relations of concepts in the Physics Derivation Graph

In the Physics Derivation Graph a derivation is comprised of steps. Each step has one inference rule. Inference rules can have

• zero or more input expressions
• zero or more output expressions
• zero or more feed values

Each expression is comprised of a LHS, RHS, and relation. "Relation" can be =, >, <, <=, >=.

The LHS and RHS and Feed values are comprised of symbols (e.g., a, b, x, y) and operators (e.g., *,+,/). 

Symbols are variables (e.g., a, b, x, y) or constants (\pi, e).

How Physics Derivation Graph concepts map to Lean

I think a PDG input expression is a proposition in Lean.

I think a PDG step is a theorem in Lean. 

Maybe the PDG output expression is a goal in Lean?

I think a PDG inference rule is a tactic in Lean. See https://leanprover.github.io/reference/tactics.html

"The type of a function that can inspect the proof state, modify it, and potentially return something of type A (or fail) is called tactic A.

source: https://leanprover-community.github.io/extras/tactic_writing.html

Equivalence of the PDG derivation step "add 2 to both sides of a=b to get a+2=b+2" with using Lean for the proof "(a=b) -> (a+2=b+2)"

In the Physics Derivation Graph the expressions "a=b" and "a+2=b+2" are related by the inference rule "add __ to both sides".

In Lean, "a=b" is a proposition. We have to specify that a is Real and b is Real. Then we can prove that

(a=b) -> (a+2=b+2)

Work in progress -- try something like

https://stackoverflow.com/questions/41946310/how-to-prove-a-b-%E2%86%92-a-1-b-1-in-lean

see also

https://stackoverflow.com/questions/67199246/apply-function-in-goal-in-lean-proof

https://proofassistants.stackexchange.com/questions/2080/equality-of-two-functions

https://xenaproject.wordpress.com/2020/07/03/equality-specifications-and-implementations/