Joseph Tooby-Smith: Physics and Lean

Stream: Lean Together 2025

[Joseph Tooby-Smith]

Here are my slides in advance of my talk.

[Ben]

How many of the 53 viewers are Physicists? (I am.)

[Bolton Bailey]

Copying over my dumb question from the zoom chat: What’s the outlook for formalizing higher level physics/chemistry using lower level physics in HepLean? If I wanted, could I define what it means for a volume of space to contain a proton or neutron, or formalize that a deuterium atom is stable, but helium-2 is not? What would the main obstacles be?

[Bolton Bailey]

I was also interested in @Matthew Ballard 's question: Is general relativity is in scope?

[Ben]

A couple related projects:

• https://assumptionsofphysics.org/ (not using Lean currently)
• https://derivationmap.net/ (my project, not using Lean currently)
• https://atomslab.github.io/LeanChemicalTheories/
• https://github.com/lecopivo/SciLean

[Jireh Loreaux]

In the Zoom chat, Joseph says:

Yes it is certainly in scope! Really I regret calling it “hep”lean because it sounds restrictive. But GR is certainly within scope

[Joseph Tooby-Smith]

No such thing as a dump question :). I know @Tyler Josephson ⚛️ is interested in the chemistry aspects, and has done some work on e.g. thermodynamics Ben has linked to their projects.

The things you mention about e.g. volume of space to contain a proton would be within scope of HepLean. It is not an area I am particularly familiar with though so can't really attest to what the main obstacles would be. I suspect there would be needed maths missing from Mathlib in that direction.

Bolton Bailey said:

Copying over my dumb question from the zoom chat: What’s the outlook for formalizing higher level physics/chemistry using lower level physics in HepLean? If I wanted, could I define what it means for a volume of space to contain a proton or neutron, or formalize that a deuterium atom is stable, but helium-2 is not? What would the main obstacles be?

[Joseph Tooby-Smith]

Jireh Loreaux said:

In the Zoom chat, Joseph says:

Yes it is certainly in scope! Really I regret calling it “hep”lean because it sounds restrictive. But GR is certainly within scope

Let me add to this - "HEP" is used quite broadly in the physics community to mean a whole load of areas, or anything related to 'fundamental physics'.

[Ching-Tsun Chou]

@Joseph Tooby-Smith , how do systems like SICM fit into your vision?
https://en.wikipedia.org/wiki/Structure_and_Interpretation_of_Classical_Mechanics

[Joseph Tooby-Smith]

@Ching-Tsun Chou are you asking about the computational part of that wiki article or the classical mechanics part?

[Joseph Tooby-Smith]

(or both)

[Ching-Tsun Chou]

Both.

[Joseph Tooby-Smith]

So classical mechanics should fit in the "physics repository"(HepLean - which maybe should be rename) that was in my vision, this is for sure within scope.

I'm not entirely sure about the computational content of SICM if it is to proof theorems that otherwise have analytic proof then I think the analytic proof would be better, but if only computational proofs exist then it for sure fits. There are many things in physics that only have computational proofs and I don't think they can be ignored. I had a plan at doing a project using a computational proof at one point, but things got busy. If it is just to provide examples, then I think it is less clear cut.

[Matthew Ballard]

Formalizing the Schwarzchild solution is a good challenge for both the mathematically and physically minded Lean communities.

[Viviana del Barco]

You mentioned in your talk that "informality" should play a role in a library for physicists. I am curious: how an "informal lemma" should look like for you, and how have a formal Lean proof of that should be -if any is expected. Thanks!

[Joseph Tooby-Smith]

@Viviana del Barco Maybe this was confusing in my talk. The informal lemmas currently in heplean (see e.g. here) are intended to be formalized one day.

However, it may be possible that some results just cannot be formalized for one reason or another - maybe they just don't have a well defined mathematical meaning. Including them into the library as a string literal in some way still has benefit - it allows them to be searched for and potentially connected to other lemmas. Maybe the statement of the result can be introduced formally but the proof can't - it could then be used in more formal results as well.

[Kim Morrison]

https://www.youtube.com/watch?v=U7Xf5p6jAUU&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg&index=25

[Tyler Josephson ⚛️]

Joseph Tooby-Smith said:

Viviana del Barco Maybe this was confusing in my talk. The informal lemmas currently in heplean (see e.g. here) are intended to be formalized one day.

However, it may be possible that some results just cannot be formalized for one reason or another - maybe they just don't have a well defined mathematical meaning. Including them into the library as a string literal in some way still has benefit - it allows them to be searched for and potentially connected to other lemmas. Maybe the statement of the result can be introduced formally but the proof can't - it could then be used in more formal results as well.

I use the term “mathematized” to describe what needs to happen to a derivation or concept in science before it can be formalized. For instance, a paper or textbook might have a derivation, but it doesn’t specify the types of any variables, what are premises vs intermediate statements, etc. It’s sometimes a novel and valuable task to informally answer these kinds of questions before starting to work on formalizing it. Formalizing might also prompt you to address these kinds of questions, too.

[Joseph Tooby-Smith]

Following on from my talk, I was thinking of the possibility of a channel on this Zulip for HepLean. Maybe at the moment this is premature but it may help in organizing and promotion etc. Any thoughts?

[Kevin Buzzard]

My instinct is that channels are cheap so I'd not be against this suggestion

[Kim Morrison]

The basic requirement, as usual, is to have someone put their hand up as moderator for the channel --- this person should either be a Mathlib maintainer, or someone known to the maintainers who would take responsibility for, at a minimum, escalating any issues to the Code of Conduct team as necessary.

[Kevin Buzzard]

I'd be happy to moderate.

[Joseph Tooby-Smith]

Thank you @Kevin Buzzard !

[Kevin Buzzard]

What do you want to call the channel, and do you want it private (so only people with invitations can see it), public (so only people with Lean Zulip accounts can see it) or web-public (so anyone on the internet can see it using a web browser, although they will not be able to contribute unless they make a Zulip account)? (the icons are padlock, hash-symbol and world, respectively, in the list of channels)

[Joseph Tooby-Smith]

For the name: HepLean, and web-public please :)

[Joseph Tooby-Smith]

Given no one has yet complained about this - @Kevin Buzzard would it be possible to now make such a channel? Many thanks.

[Johan Commelin]

Voila: #HepLean