notes from Preposterous Universe podcast episode 245

Notes from the podcast https://www.preposterousuniverse.com/podcast/2023/07/31/245-solo-the-crisis-in-physics/

Definitions of Understanding

• Strong understanding = unique, well-tested theory that accounts for all the data we have within the domain of applicability (defined by SMC at 14:00). 
• Consequences: There are no competing theories. Modifications or extensions are feasible, but the domain is "solved." The theory won't be displaced.
• Examples: general relativity, Newtonian dynamics, Newtonian gravity.
• Weak understanding = more than one theory can account for the data. Unable to discriminate which is relevant since theories make the same predictions. (defined by SMC at 15:44)
• Consequences: Not clear theory which is right. Right theory may not have been invented yet.
• Examples: 
• Foundations of quantum mechanics (e.g., Copenhagen interpretation, Bohemian, many worlds, jaggets platz)
• dark matter and dark energy in cosmology. Properties are known, but multiple theories
• dark matter: WIMPS, axions, 
• dark energy: vacuum energy, dynamical quintesense-like fields
• No understanding = have data but no theory (defined by SMC at 18:20)
• Examples: what happens at or before the big bang

SMC's claim: We have either a strong or weak understanding of everything that is accessible through measurement. (at 21:40) There's nothing that's experimentally accessible and not understood. That's new!

Survey of domains and relations

What is it that we know?

Newtonian dynamics. Space is separate from time. Deterministic Laplacian evolution.

Theory of relativity (1905, Einstein) explains space-time (as per Minkowski, 1907).  (SMC: 29:22)

Special Relativity: how space-time is when gravity is not important; when space-time is flat. (SMC 30:20)

General Relativity: space-time can be curved and that curvature is gravity. Predicts big bang, black holes. SMC 30:10)

Quantum Mechanics (1920, Heisenberg).
Replaces classical mechanics -- SMC 32:10

QM is about continuous wave function defined by Schrodinger Equation. 

Solving Schrodinger's Equation results in discrete solutions -- SMC 35:55

Quantum Field Theory. 
Under the umbrella of Quantum Mechanics -- SMC 32:33.
QFT is compatible with Special Relativity -- SMC 32:42

The world is made of fields, not particles. -- SMC 34:40

Fields resolve into particles when the fields are observed.

Relativistic QFT includes Special Relativity

Quantum Electrodynamics (QED) is the theory of interactions of electrons, positrons, photons.

Initial theory had infinities. Resolved infinities using renormalization by taking limit in a specific way.

Ken Wilson simulated QED using discretized space-time (rather than a continuous PDEs).
--> Lattice Quantum Field Theory eliminates the infinities. 

Infinities (represented as loops of Feynman diagrams) are reduced to (non-infinite) tree diagrams in Feynman diagrams. 

Rather than arbitrarily large momentum (small space), discretization constraints the infinities.

Limitation on the domain of applicability is the Planck scale. -- SMC 45:20

This is the ultraviolet cut-off. There's an energy above which we don't know what's going on. -- SMC 46:05

stopped at 53:30

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?"

a chain of custody for papers in arxiv to formal proofs in Lean

Papers published in arxiv using Latex contain narrative text and mathematical expressions. How could we have confidence that the content of a published paper is related to a formal proof?

The narrative text would refer to symbols, expressions, units, and quantities. The expressions and symbols could be embedded in the Latex source using a package that provides macros.

The author's .tex would include loading a package like

\usepackage{pdg}[server_address=http://serveraddressforpdg.net]

Then when the author references an expression they would use

\begin{equation}
\pdgexp{192839}
\end{equation}

When compiled to PDF, the macro \pdgexp calls to the server address http://serveraddressforpdg.net to return the Latex expression. The same could be done for an inline reference to a symbol, like \pdgsymbol{93831911}. 

In this approach there wouldn't need to be an appendix for the derivation because the derivation steps are hosted on the PDG server.

The chain of custody would be

arxiv PDF -- arxiv .tex -- .tex contains references to PDG expression and symbol IDs -- PDG server contains derivation steps -- steps are validated using Lean

The macro might need to cache the PDG database locally so the server doesn't get called every time the .tex is compiled PDF. 
Also, allow the author to force a refresh of the cache.

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/

computer algebra system (CAS) is inadequate for the Physics Derivation Graph (PDG)

I'm beginning to appreciate that a computer algebra system (CAS) is not sufficient for the Physics Derivation Graph (PDG). The evidence of this is that the variables I'm defining can be real or complex; that is not distinguished by the computer algebra system.

The simple story of starting with

a = b

and then adding 2 to both sides to get

a+2 = b+2

is appropriate for a computer algebra system. But if "a" is a matrix then the operation is invalid. The only way to distinguish "scalar a" from "vector a" from "matrix a" is to specify the difference. [SymPy does have support for predicates -- https://docs.sympy.org/latest/guides/assumptions.html#predicates .]

In the Physics Derivation Graph I want to be more specific about the possible values of a and b. Even for non-physics derivations like the Euler equations, there are assumptions about the possible values of each variable.

I don't know Lean, but I also don't know the foundational concepts of theorems and proofs.
Is a step a theorem?
Is a derivation a theorem?
The role of inference rules in steps in derivations does not map to anything in a theorem.