Level of rigor in PhysLean

Stream: PhysLean

[Joseph Tooby-Smith]

Given this comes up a lot, and it came up again at #PhysLean > Vector calculus @ 💬, I thought I was worth making a thread dedicated to this, which can be referred back to. Below I'm going to give my philosophy but I am very much open to ideas and suggestions of what people think is best.

One thing I learned in my pre-Lean days is that you will never get a consensus on what level physics should be done at. I myself lean towards the more (discrete) mathematical side, I occasionally spout about higher category theory, number theory etc on this Zulip. But I've worked with physicists who are much closer to experiments and couldn't care less about my category theory :(. This naturally lead to arguments, or 'academic debates', but usually some sort of consensus was found.

All this to say, the only way I think we can attempt to please everyone in PhysLean is to openly allow different levels of rigor (in a controlled and non-duplicatory manor, of course). After all, these different levels of rigor are all part of the landscape that make up physics, and we are still waiting on that theory of everything.

Let me call these different levels of rigor different approaches, since this is actually what they are.

The ideal situation (to me) is where we connect each of the different approaches together, in a way where the integrity of each approach remains intact. This might not be easy - but neither formalization nor physics ever claimed to be easy.

To give an explicit example, take classical mechanics. Let A be the conventional approach to classical mechanics. Let B be the approach using symplectic geometry (a fancy area of maths). Let C be the approach using jet bundles (another fancy area of maths).

To me, PhysLean should have all three approaches A, B and C.
Approach A should be done in a way that it is useable to, for example, undergraduates, and such that they can contribute to it and be onboared using.
This integrity should not be effected by the formalization of B & C. It would be great for B & C to have the necessary API so that they can be connected to approach A (a perhaps to each other), so that you don't have to replicate theories from approach A in B and C.

Anyway this is my philosophy on this. I could be wrong, but I really do think this is the only way of making everyone happy.

[Kevin Buzzard]

Shouldn't you be doing B or C under the hood but have good API to mean that people can just do A?

In mathlib we have some kind of incomprehensible proof that the derivative of sin is cos but it's a simp lemma and various tactics can use it so undergraduates can access it without worrying about what's going on under the hood

[Joseph Tooby-Smith]

I think this is an option, yes. I guess it would open up the debate of whether it should be B or C (assuming they are 'incompatible' in a sense). But as long as the API is good this should not matter.

Another option would be to have the necessary definitions in A independent of B or C and to show that definitions in B and C are equivalent (in certain limiting cases) to those of A. Then you could go back from A to B or C when necessary.

There is likely some pretty diagrams with cleaver notation one could draw showing the different options of how things could interconnect. I think the choice in a given situation is going to depend on the explicit details.