Deduction of physical principles?

Stream: Natural sciences

[Mario Krenn]

Hi! My name is Mario. I am leading a research group within the Max Planck Society in Germany. My work focuses on quantum physics and AI for science. I have little experience with Lean, and aside from supervising one bachelor’s thesis on quantum optics in Lean, I have mainly been watching talks by Kevin Buzzard and others.

Until recently, it was quite unclear to me how Lean could contribute to physics. However, after a call with @Tyler Josephson ⚛️ last week (who suggested I say hello here), I spent the weekend reading papers and watching @Joseph Tooby-Smith’s talk.

I now think there might be an incredibly exciting possibility for using these tools in physics -- namely through automated inverse deduction. Let me explain in a very simple way, and I am very curious about your thoughts.

Induction is the derivation of mathematical laws from experimental data -- essentially a form of advanced curve fitting. In AI, this is sometimes called symbolic regression (examples include Planck's fitted formula for black body radiation or the Lorentz fit describing the Michelson-Morley experiment). While useful, this approach doesn’t reveal much about the underlying physics.

A different way to gain scientific insight is deduction, where one starts with a set of simple assumptions and derives scientific laws. For example, Einstein’s special relativity theory derives the Lorentz transformation from the postulates of the constant speed of light and the invariance of physical laws for observers in relative motion.

I saw in a paper by Tyler that derivations of laws from simpler assumptions are possible. Similarly, parts of special relativity theory have been derived in Coq from five axioms.
Deduction: simple assumptions -> physical laws.

Inverse deduction, on the other hand, would look like this:
simple assumptions <- physical laws.

In other words, given physical laws, which sets of assumptions could lead to them? See one non-automated example in quantum physics. I think, if this is possible -- even at a small scale -- it could have an enormous impact. It would mark the first time that true physical principles could be discovered in an automated way (to my knowledge, no other automated method even comes close to having the ability to achieving this).

I am very curious to hear your thoughts. Thanks a lot!

[Joseph Tooby-Smith]

Hi @Mario Krenn ! Nice to meet you! How do you envision inverse deduction being automated?
I'm also a bit confused about what you see the rules of the game being i.e. where does one stop with the simple assumptions e.g. does one go all the way back to the axioms of a set - I guess not?

[Eric Taucher]

Mario Krenn said:

However, after a call with @Tyler Josephson :atom: last week (who suggested I say hello here)

I also want to give a thanks to @Tyler Josephson ⚛️, I had the pleasure to watch his Lean for Scientists and Engineers! remotely and learned quite a bit; glad to see him here.

[Mario Krenn]

Joseph Tooby-Smith said:

How do you envision inverse deduction being automated?

The inverse problem is a search problem, it is very related to many inverse problems in science i think. My research group's main focus for instance is on the automated design of new physics experiments, which is basically the inverse of a standard forward computation (experiment to experimental result that can be performed with simulators). There are many techniques developed for inverse problems, one can try different ones, the simplest (to show whether it works) is just to enumerate all possibilities. The crucial point is: The forward step should not make too much problems, thats a usual property of inverse problems. E.g. computing the expected physical results given an experimental setup requires "just" solving Maxwell/Schroedinger. In this case, the forward-step goes from axioms to equations of motions. It will be crucial to get this to work, its likely a challenging part of this idea.

[Mario Krenn]

Joseph Tooby-Smith said:

I'm also a bit confused about what you see the rules of the game being i.e. where does one stop with the simple assumptions e.g. does one go all the way back to the axioms of a set - I guess not?

Not all the way down to axioms of math, but all the way to simple assumptions, i was very inspired by Tyler's paper on chemistry and his derivation of Langmuir adsorption in Lean (see assumptions in eq.(1) and (2)). In special relativity for instance, one would have as assumptions the constancy of speed of light, and the fact that one cannot distinguish in any way whether you are moving constantly or standing still (the Coq paper on SRT shows one option).

[Tyler Josephson ⚛️]

I have many thoughts about this, because I’ve been wondering how this might work out for a few years now.

First, it’s important to recognize that Lean isn’t really made to do reasoning without a goal. In other words, science and engineering problems that involve the idea of “solve for x” are typically hard to do in Lean since you’d need to state what “x” is, and that sort of defeats the point of asking the question (for a scientist or engineer). But this is a problem being worked on in the Lean community - it goes by names like, “how can Lean be more like a computer algebra system?”

The other issue is more fundamental to logic, and doesn’t depend on Lean per se. If you just ask, “here are my assumptions, what can I derive from them?”, you’ll find you can derive an infinite number of statements. Think about this paper: https://link.springer.com/article/10.1007/s10489-017-0954-8 and this one:
https://arxiv.org/html/2405.06677v1
You might even imagine tasks like, “what if an AI started with the core of Lean and just went off, imagining new maths?”
How would it need to be coaxed into constructing useful maths? Beautiful maths? Math libraries that are practical to use? You could do this from many starting points, as long as you ensured each was free of contradictions.

The forward “automated theory construction” is about growing a complex, many-branched tree from a root, where you have a mechanism for validation at each branching point.

Now, what about reversing the process? You need to grow your way backwards to the root (or perhaps, many possible roots). I can’t think of many examples of this in logic. “If and only if” goes both ways, but most of Mathlib is about defining an object and showing that it has properties — this is implication in one direction. It’s hard to imagine “state a property, then generate definitions that have that property,” but I suppose that’s what you have in mind?

[Alex Meiburg]

There's a version of this that has had mild success within universal algebra (where, generally, the axioms are much simpler to state than physics). First, you have someone state - or prove - some set of necessary and sufficient axioms A1. ("Necessary and sufficient" as in they are true in the theory, and imply the whole theory - the axioms could still be redundant with each other!) Then you can search for some 'minimal' set of axioms A2 that is equivalent to A1.

What metric defines "minimal", and what form you want your axioms to take, is a bit subjective of course. You can always reduce to a single-axiom theory A1' by combining all of the axioms in A1 with a logical AND. But often there's also some kind of idea of 'expression length' or 'variable count' that maybe should be reduced.

In physics, the types of relevant expressions are often much more flexible, but having an AI propose "notably small" basic sets of axioms by any intuitive measure would certainly be good.

[Alex Meiburg]

Besides GPTs, another decent example on a physical system is https://arxiv.org/pdf/2311.07476 .
For context, since that's kind of a specialized topic:

• The relevant theory here is "quantum circuits"
• There is an obvious axiomatic interpretation of quantum circuits which is "interpret everything as unitaries of size 2^n", which in some sense tells you everything you'd want to know about quantum circuits.
• You can show that the simpler question of "when are two quantum circuits equal?" is actually also sufficient - if you have a theory that tells you which circuits are equal, you can also use that to prove (in a meaningful sense) everything about their output probabilities and so on. This reduces the theory in some complexity. But determining which circuits are equivalent is hard to express.
• Another work had established a minimal set of axioms that precisely determine when two circuits are equivalent. It was phrased in terms of ZX-calculus. ZX-calculus involves working with somewhat exotic objects that don't correspond to any physical circuits. But, you can lift all actual circuits into a "ZX diagram"; and they gave minimal axioms for proving which ZX diagrams are equivalent.
• The paper I linked (or rather, a slightly earlier paper) then finally found some axioms purely in terms of the circuits - as an equational theory - that were equivalent to the ZX calculus axioms. This was the first statement of "circuit equivalence" purely in terms of circuits.
• Then there was work to reduce and simplify those axioms, which is the actual paper I linked. They reduced the axioms in size and number, and showed that they were non-redundant (in the sense that removing any single axiom was not sound).

[Matteo Cipollina]

I think a particularly interesting direction to explore, among others, would be to use the idea of invariance under transformation as a foundational principle and to draw inspiration from reverse mathematics (https://plato.stanford.edu/entries/reverse-mathematics/), potentially using physical equivalences to guide / constrain our exploration of the space of possible physical theories, much like logical equivalences (via model theory) guide the exploration of mathematical foundations in reverse mathematics: i.e. symmetry and invariance but also dualities between theories, conservation laws, and invariance under changes of representation (like coordinate or basis changes).

[Mario Krenn]

Thanks a lot @Tyler Josephson ⚛️, great papers. Let me call Atotal=(A1, A2, ...) the total list of assumptions and X the physical law/equation of motion etc.

I think why this is much simpler than automated proof search:
1) in physics it is usually very easy to derive equation of motions from a set of assumptions (a small number of simple algebraic steps), at least compared to mathematical proofs.
2) We know what X is (those are specific equation of motions, e.g. SRT, ART, or Schroedinger), do not need to explore any expression that follows from Atotal.

What is required boils down to the forward pass:
Given some Atotal, does X follow from it or not?

If the forward pass can reasonably be automated, then there are many inverse methods that can be applied (that work externally and just use the forward pass as a tool for exploring possibilities).

[Tyler Josephson ⚛️]

The forward pass can be definitely automated if only simple logic is required. But expressing and doing proofs about Schrodinger’s equation will require higher-order logic, so no guarantees. You’d need two steps:

1) ensure consistency of Atotal (avoid principle of explosion, https://en.m.wikipedia.org/wiki/Principle_of_explosion)
2) attempt to prove that X follows from Atotal

Either step would be undecidable, but you could always try letting one of the open-source ML tools for theorem proving give it a try.

I wonder if, in physics, you’ll also need to do extra work to carefully define your semantics. In a few hours I can share what I mean.

[Tyler Josephson ⚛️]

Suppose you wanted Atotal to consist of "classical mechanics" (e.g. Newton's laws of motion, gravity, linear and angular momentum, derivative relationships among position, velocity, acceleration, etc.). We know we can derive the kinematic equations from this, which describe projectile motion. We can also derive equations for the motion of planets, pendulum, mass on a spring, stability of a car driving around a turn, a mass on a pulley, etc. You might imagine making some set of these things be "X" and show that Atotal --> X, and then start your exploration of alternative versions of Atotal that might also explain X. But it's ultimately not going to be quite this simple, because you'll need to define, semantically, what a "projectile" is and what a "pendulum" is and what a "pulley" is and so forth. There needs to be some kind of guidance (most likely, a formal specification) around what aspects of Atotal are relevant in this or that situation.

I don't know what that's going to look like in the situation you have in mind, but I think it's something important to think about.

[Alex Meiburg]

you'll need to define what a "pendulum" is and so forth

Yeah, this is why I think working in a slightly more closed setting is good. Fix what form your data takes, so that the operational meaning is fixed; then look for the minimal constraints on the data to be well-behaved.

• Quantum mechanics is typically described in terms of operators and expectation values. If you boil down the axioms you need to get a 'sensible' theory, you arrive at the study of von Neumann algebras.
• Classical physics can be described in terms of differential equations with forces, or an action that gets minimized, or symplectic geometry. Those are different kinds of data, and each one has an operational meaning. We have corresponding ways to interconvert. The "axioms" are then properties the data should have, like the action should probably at least be continuous. You could also define it as the limit of quantum systems.
• GPTs describe both quantum and classical physics; now the data is "preparation" and "transformation" and "observation" probabilities. There are some common axioms all GPTs should follow. And then there are additional axioms that are known to uniquely determine quantum or classical physics (or other exotic realities).
• In my example above, the theory of quantum circuits is a PROP (no relation to the type theoretic Prop) with a standard operational interpretation: that a circuit has "output probabilities". It was some human ingenuity to show that the output data is in some sense redundant, and that circuit equality determined the operational semantics. Then there's a bunch of math to get minimal axioms.

Those all kind of talk about the same problem, but they all have different starting data, so the answer is very different.

[Alex Meiburg]

These problems aren't unique to physics, they also apply to e.g. compiler correctness. You need some initial model of compiler behavior, and axioms on how it should behave.

There are stronger and weaker models of compiler equivalence (does it have to preserve the memory layout of the heap? Of structures? Can a function be inlined away? Does it have to preserve order of syscalls, or can some commute?), the data can take different forms ("a compiler is a function from C to assembly" or "a compiler optimization is a function from assembly to assembly" or "a compiler optimization is a function from memory layout to memory layout"), and then there are different appropriate initial axiom sets for each combination. The initial axioms are usually the "obvious thing" that it should preserve x y and z, which ends up being a very long definition that requires a full explanation of how the computer operates.

And then you can look for the minimal axioms that still guarantee correctness, which are indeed often much shorter.

[Mario Krenn]

Matteo Cipollina said:

I think a particularly interesting direction to explore, among others, would be to use the idea of invariance under transformation as a foundational principle and to draw inspiration from reverse mathematics (https://plato.stanford.edu/entries/reverse-mathematics/)

This is very closely to what I would like for physics, awesome link thanks!

I was looking now a bit into @Joseph Tooby-Smith 's HepLean to understand the assumptions. Ideas like the CKM-Matrix are too complex, can one derive them from some simpler physical assumptions?

@Tyler Josephson ⚛️ , in your Digital Discovery paper to proof Langmuir, what were the assumptions (Atotol)? Do i understand right that you have, for instnace, as one assumption, "assuming equlilbrium" (for eq2). This seems to be the level of complexity of the assumptions that i hope one could also use in physics. This proof seems (by hand) rather trivial. What was the most difficult part to get it to Lean, and how far could automated theorem provers help?

In the auto-search for physical principles, one would have many Atotal -- parametrized in such a way that hopefully your set is part. Then a trivial algorithm would go through all Atotal_i, and tried to derive eq(6). Very curious!!

[Tyler Josephson ⚛️]

You can find a Lean 4 version of the Langmuir proof here:

https://github.com/ATOMSLab/LFSE2024/blob/d7aa531d0fd9b8e5089dc2ae2375e069d4dab1bc/Lean%20Code/Lecture8_post_lecture.lean#L71

This shows that 9 “premises” imply the conjecture. But really, for a scientist, the 9 premises are not all equal. hK is just a definition of the equilibrium constant. hc1-hc3 are needed to get the proof around division by zero, but more meaningful constraints would require S, A, k_d, etc. to be positive or non-negative.

You can see my student proved this with 4 tactics followed by a calc block. I don’t know for sure, but I highly suspect the latest ML tools for proof completion should be able to handle proofs like this.

Keep in mind this is a “low-quality” proof in that only one term is actually defined outside the theorem (the function Langmuir). If you want your theory to include interconnected ideas, then the hypotheses in the theorem statement (hrad- hS_tot) as well as the function Langmuir, must be defined in some kind of definitions or structure outside this theorem, which you then invoke here.

[Joseph Tooby-Smith]

@Mario Krenn So the assumptions underlying the CKM matrix are essentially that you have 3 families of fermions in the universe, (e.g. up-quark, charm-quark and top-quark) obeying certain symmetry properties.

No one knows for sure why we have 3 families of fermions - this is an open question but there are lots of potential solutions each relying on assumptions.

Basically most of the "assumptions" in fundamental physics come down to naming a Lie group and the representation of particles under this Lie group. Quantum field theory takes things from there.

Quantum field theory is not perfectly well defined, but there are more attempts to formalize it which do work on very basic assumptions. You can get to topological field theories by making simple assumptions about locality etc.

[Mario Krenn]

Thanks for the extra details. I am trying to understand now in general which physical/chemical derivation (equation of motion or other transformation laws) might be most suitable. What is absolutely necessary: Its a very simple proof that ATP can tackle. That's requires to use an automated forward pass for the inverse-search of the set of assumptions. Will chat with Joseph this week to understand better the HepLean axioms. Hope ot come back with more concrete ideas. Any concrete suggestions until then are much apprechiated, especially of derivations of physical laws/principles from very simple assumptions in Lean.

[Tyler Josephson ⚛️]

https://arxiv.org/abs/2503.04772

Point something like this in the direction of physics?

[Mario Krenn]

Hi Tyler, thanks for the link. There ar three points:
1) Axiom system
2) Theorems / physical laws
3) Proofs /derivations (logical connection of (1) with (2))

This paper starts with a constant (1) and finds new (3). I describe to find new (1), which is physically very different.