Intro: Joseph Tooby-Smith

Stream: new members

[Joseph Tooby-Smith]

Hi,

My name is Joseph, and I'm a postdoctoral researcher at the University of Cornell. While my primary background is in physics, my research leans more towards mathematical concepts such as functorial field theories and higher categories.

I'm interested in exploring the potential application of Lean in my research. Specifically, I'm curious about whether my work can be formalized using Lean and if there are broader areas of physics that could benefit from its application. In the long run, could Lean enhance the efficiency of physics research?

A logical first step might be to examine the undergraduate and master's level physics curriculum through the lens of Lean, similar to what's been done in mathematics. While I doubt that everything, like quantum field theory, can be expressed in Lean, it may be worth working out which areas can and which can't - and if this can be used in research or pedagogy. If this sounds interesting to anyone - let me know.

Joseph

[Patrick Massot]

You can have a look at the Natural sciences stream. But there is not much about physics in Lean yet.

[Tomas Skrivan]

I'm also interested in doing physics in Lean. One of my goals with Lean is to do symbolic calculations in calculus of variation. In my experience, calculus of variation is often explained in quite confusing way and there is a big disconnect in how physics and mathematicians do it. I think, having Lean guiding you through such calculations would be quite nice. For example, I never fully understood how you derive euler equations for rigid body motion from the action principle as there was always some mysterious step I did not fully grasp. Also, I'm not aware of any computer algebra system capable of doing such computations.

[Adomas Baliuka]

@Tomas Skrivan As a physicist, I'm quite surprised you'd expect formalization to reduce the gap between mathematics and physics. As a formally inclined person it has taken me a long time to come to terms with it but I think there are good reasons why physicists abuse math and despise rigour.

In math, you make some assumptions and go with them. I would think very few mathematicians find themselves having to question (even property learn?), let alone change the very basic axioms. You don't switch between finitist constructivist math and ZFC with extra ordinals depending on what kind of problem you face (maybe some mathematics do?). Sure, you can make a definition and later find that another definition would have been better, but that doesn't make that definition wrong or allow you to derive falsities.

A physicist who tries to model anything makes assumptions that they know to be wrong and they know that their model can derive a contradiction (with reality). You choose a theory (or mix several mutually conflicting ones) as you deem appropriate. This means you can never trust the formalism. You can only know from experience ("physical intuition") that the kinds of manipulations you choose to do will give results that are right enough for the purposes you care about.

Of course, it's a continuum and there's a point where theoretical physics and math smoothly merge. However, if it's just about the infancy phase for applied formally verified math, I guess physics is still far away. Mind you, I like formalization for the fun of it so if you make a PhysicsLib, I might contribute some operator theory eventually if I manage to learn Lean :D

[Tomas Skrivan]

Ohh I'm making a claim only about calculus of variation. In that particular case physicist despise rigor because mathematicians show them too stringent formalism that is useful for proving that solution exists but it completely useless when doing calculations. No wonder physics ignore it :)

[Adomas Baliuka]

I think historically it was more that the "physicists' way of doing it" was developed first and when the mathematicians made it rigorous a century later physicists didn't see any reason to change their notation or the way it is taught. So it's not so much that the mathematicians' rigorous version is stringent (although it may well be) but it doesn't allow you to do any calculations you weren't able to do already.

I think that happens a lot in the interplay between physics and maths (e.g. differential forms in thermodynamics, integration by substitution, distribution theory...).

[Tyler Josephson ⚛️]

ab said:

A physicist who tries to model anything makes assumptions that they know to be wrong and they know that their model can derive a contradiction (with reality). You choose a theory (or mix several mutually conflicting ones) as you deem appropriate. This means you can never trust the formalism. You can only know from experience ("physical intuition") that the kinds of manipulations you choose to do will give results that are right enough for the purposes you care about.

I think, at the moment, Lean enables us to formally verify the syntax of a derivation in physics. It requires us to be transparent and precise about our assumptions, after which logical tactics enable us to be sure that a conjecture follows. One could state the assumptions of Newtonian mechanics as hypotheses in a theorem and show some result which follows, and one could also state the assumptions of relativistic mechanics as hypotheses in a different theorem and show some other result which follows, and Lean could be used to prove both derivations. Which set of assumptions semantically connects to the real world is a different question, one that, in my opinion, need not diminish the value of ensuring the syntax is correct. But indeed, most scientists care most about whether a given physical model is suitably accurate relative to a physical context, and they tend to not worry about their derivations having math errors.

[Adomas Baliuka]

My point is that you can prove absurd things (not False, just uphysical) assuming any known theory of physics. For example, Newtonian mechanics has initial conditions for N-body problems that admit solutions only for finite time (some object reaches "infinity" at finite time). You can say "sure, it's Newton. This won't happen with relativity". Then special-relativistic Electrodynamics has unphysical "propagating shocks". You might say: "that's fine, it won't happen in QED or GR" (I don't know if that's true or whether the question is even straightforward to ask in QED). And then something else will come up.

My point is that in physics, to give correct and useful results for practical problems (which I hope is the ultimate goal of formal methods, besides giving us a very enjoyable puzzle game), it's neither necessary nor sufficient to be correct in the logic/math sense. There's some kind of reasonableness which is currently a very fuzzy thing. You might be able to somehow formulate and formalize it but that seems quite hard.

(As an aside, maybe that's somewhat analogous to paradoxes in math like Banach-Tarski, which I've always understood to mean that the real numbers aren't quite what we want but we use them anyway because they do what we want when it matters... Maybe that means my entire point is moot?)

That doesn't mean that formalizing physics is useless but I think the question "what is it useful for" must be asked separately from that question in mathematics. For what it's worth, I'm foolishly hoping to eventually use Lean for a small cute part of my physics research but I'm much more sure that it will be fun than that it's actually a good idea.

[Joseph Tooby-Smith]

I'm a physicist who is very close to the boundary with mathematics... I think most physicists would call me a mathematician, and most mathematicians would call me a physicist.

I agree with @Tyler Josephson ⚛️ here, that one should state the assumptions of e.g. classical mechanics or quantum mechanics and derive the results which follow from there. When these results are applicable to the physical world is, I agree, another question - and one that needs some input beyond mathematics - i.e. experiements. Nevertheless, one can take a completely `theoretical' viewpoint of this.

Why do I think formalising physics will be useful? I think that at some point in the future, maybe 5 years, 10 years or 100 years from now, we will have a mathematical rigorous notion of a physical theory. Something to replace the ill-defined notion of the path integral in quantum field theory. [One possibility for this is something called functorial field theory] I think it is very likely that this will be formalisable in lean, or some predecessor. A top-down approach would be to take this definition and use it to derive (rigorously) a bunch of results/theorems about the real world. Having a pre-existing library of results in physics formalised will make this task easier, and well-motivated.

As a completely separate point. If we get to the point of automated proof writing outperforms humans, then this will be useful to theoretical physicists too. Particularly in e.g. general relativity and mathematical physics.

[Adomas Baliuka]

I generally agree. However, what you said doesn't address my question at all. It simply dodges it.

I claim that physics and math are different and that one of the crucial differences is in how they interact with reality. Mathematics certainly interacts with reality, but mostly indirectly. You can (and should if you can!) do number theory for centuries before anyone finds an immediate practical use for it. What mathematicians at universities can get funding to research is influenced by what is done by physicists, computer scientists, philosophers, agricultural engineers, etc., and vice versa. But a mathematician is free to imagine any theory they fancy and derive consequences without anyone (mostly, as always) questioning if what they're doing is mathematics. Maybe in a hundred years ZFC will be a relic of the past and HoTT or some other thing most people don't understand will have taken over. But the "Gauss-Bonnet theorem" will remain a theorem, even if it is formulated differently and maybe deals with completely different objects. Nobody (I have the audacity to claim) will ever come around and refute it.

Computer science is a step closer to reality. You care about Turing machines and formally proving things about them in the sense of abstract math, enjoying the beauty of your platonic pantheon of theorems. But you also kind of care about being able to approximately well-enough solve actual instances of the traveling salesman problem and about building corporate IT infrastructure that mostly isn't hacked all the time. This is hard, but formal methods are actually useful for that because computers almost always do what you tell them to.

Meanwhile, in physics, you do some observations and routinely find situations where your current candidate "theory of everything" fails. You find situations where physicists disagree on how to model things and what the predictions should be, even though they claim to use the same "theory". Your experiments mostly don't do what you want. Instead, you need an army of PhD students who bully their equipment to conform to the subset of physical laws you choose to examine (I guess you can tell I'm an experimentalist). This is no surprise to anyone involved. The real world is just very messy and physicists have to deal with it. You just keep using the old "refuted" theories in cases where you expect them to work. You mix and match and use them it in ways that tend to work, which is taught by osmosis. This process of applying wrong theories to get correct predictions, I claim, is essential to physics. How do you start to formalize this? Is the situation really helped by formalizing the theories, together with their absurd consequences, just ignoring this?

Maybe! I'm willing to help try. But it's not obvious to me and seems worth thinking about. In any case, the usefulness and inevitability of formalization in mathematics is more obvious to me than in physics.

These kind-of-philosophical debates between formalists and other mathematicians have taken place in the past and it seems to me the formalists are winning. Maybe they will also win in physics eventually but I cannot visualize what that might look like. Meanwhile, I think https://arxiv.org/abs/0803.0417 is a "mathematical rigorous notion of a physical theory" and physicists have so far (I think quite rightfully) almost completely ignored it, along with other candidates.

By the way, keep working on making sense of path integrals. That's great, I'd love to see it done. It's great to know people much smarter than me are working on it. Most of my professors so far just dismissed the very notion of rigour when discussing those things...