Maintainer team for PhysLean

Stream: PhysLean

[Joseph Tooby-Smith]

One of the things that was discussed yesterday in the PhysLean café was the putting together of a voluntary maintainer team for PhysLean. I am very keen to do this, not because of any workload issues, but because I think it is best to maximize the community nature of the project. It is also a recipe that seems to work with Mathlib, and therefore something we could replicate.

This has also being discussed here:

#Lean Together 2026 > Leopoldo Sarra - autoformalization in physics / engineering @ 💬

The two main responsibilities would be to:

1. Review PRs for physical correctness, readability, style etc. (including those of other members of the Maintainer team)
2. Help structure and guide the project.

(The default for PhysLean on policies etc. has been and I think always will be to just default to Mathlib's policy.)

Because of these responsibilities I think the minimum requirements to be on the maintainer team are:

1. Some experience of the Mathlib review process and what that involves.
2. Some background in physics (or have a lot of experience with Mathlib to balance this).
3. Ability to act impartially and independently from any other affiliations.

At the moment I suspect the workload to be very small <=1 hour a week. As I said above, this would have to be done completely voluntary, as is true for all open source projects, but it would hopefully give people a chance to have a bit of ownership over the project.

If you are interested send me a DM. If you have comments on this in general (e.g. want to suggest other responsibilities or requirements) feel free to below.

[Rein Zustand]

I think that formalizing the style into a document would be useful, as I raised in #PhysLean > EPR paradox formalization @ 💬 .
The example was

There are many properties of SU(3) x SU(2) x U(1) which are important to physics, and do not hold for general reductive Lie groups, or we do not care about these properties for general reductive Lie groups. The philosophy here would be just to include the properties for SU(3) x SU(2) x U(1). Someone can always come along later and fill in the more general versions.

But the devil is in the details. More examples would help contextualizing the Reddit post quoted in that message.

[Winston Yin (尹維晨)]

@Joseph Tooby-Smith I'd love to be listed as a maintainer for PhysLean. I've mainly been writing mathematical foundations for Mathlib, but this'll be a good motivation to help contribute to PhysLean.

[Joseph Tooby-Smith]

@Rein Zustand I think this is a great idea, but like all things it is something that takes time! hopefully I (or someonelse) will get around to writing something in detail at somepoint. But I think clarifying resources like examples would be great.

[Joseph Tooby-Smith]

Hi @Winston Yin (尹維晨) awesome! I think this makes perfect sense, and I had you in mind when I wrote that message to Leopoldo on the other thread. Will message next week with more details.

[Winston Yin (尹維晨)]

Thanks! Looking forward to more details.

[Joseph Tooby-Smith]

I put together a summary of the role of the maintainer team here:

https://github.com/HEPLean/PhysLean/pull/925/changes

Basically copied from:

https://leanprover-community.github.io/teams/maintainers.html

Except I changed the term period from 2 years to 1 years, which I think makes more sense, given the much earlier stage of the project.

[ZhiKai Pong]

Hi, I've been following the project for about a year now, and now that I've wrapped up my studies I'm looking to contribute to PhysLean again. I'd say my knowledge is a bit lacking in all aspects (Lean, mathematics, theoretical physics), but I also think I have some idea about the challenges and intricacies of formalizing physics. I'd love to join the maintainer team and also learn along the way if that's ok.

[Joseph Tooby-Smith]

Awesome @ZhiKai Pong ! It would be great to have you on the team :)

[Joseph Tooby-Smith]

At the moment this makes four of us: @Winston Yin (尹維晨), @ZhiKai Pong , @Daniel Morrison (who messaged me privately) and myself. I think this is a good start :). Many thanks for volunteering.

[Joseph Tooby-Smith]

(You should have all got a GitHub invite from me)

[ZhiKai Pong]

https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/The.20Github.20organization/with/556998830

I think this is a good opportunity to officially rename the organisation for better visibility and avoid confusion for new comers? (Changing the organisation name from HEPLean to physleanorg or similar)

[Joseph Tooby-Smith]

/poll The organisation name for PhysLean
physleanorg
physlean-community
petition to move under leanprover-community
lean-phys-community

[Joseph Tooby-Smith]

@ZhiKai Pong I agree that now is the right time to do this :).

[Joseph Tooby-Smith]

@Johan Commelin Do you know if moving PhysLean under leanprover-community is something that would hypothetically be possible? Maybe there are good reasons why we shouldn't do this, from the side of leanprover-community and PhysLean. (Also sorry if you are not the right person to be asking :)).

[Rein Zustand]

Extrapolating, would it make sense if all future similar formalization efforts be moved under leanprover-community as well? E.g. ChemistryLean (https://atomslab.github.io/LeanChemicalTheories/), BioLean, EconLean, etc?

[Joseph Tooby-Smith]

In any case it seems like lean-phys-community is the winner, so....

tada: https://github.com/lean-phys-community/PhysLean

Turns out the change was easier than I was expecting. But you may have to update where locally stored versions of PhysLean point to!

[Rein Zustand]

Turns out the change was easier than I was expecting. But you may have to update where locally stored versions of PhysLean point to!

This is not necessary. GitHub automatically does a redirect of the old URL endpoint to the new one.

[Joseph Tooby-Smith]

Ok, good to know - there was some warning along these lines when I moved it. But if everything ends up working , then great :).

[Alex Meiburg]

The links at on many pages, e.g. the bottom of https://physlean.com/ProjectIdeas , are now broken!

[Alex Meiburg]

(In fact it may be worth making a new org to "camp" on the name HEPLean, to act as a redirect. Fight link rot!)

[Joseph Tooby-Smith]

I created a new organisation with the name HEPLean - which I will never use for anything :). Thanks - yeah I think this will prevent someone making e.g. ./HEPLean/PhysLean which would ruin the links etc.

[Joseph Tooby-Smith]

On the website do you mean specifically the link in "PhysLean is maintained by HEPLean."? Which I agree is incorrect -just checking you don't mean anything else. Though we should likely just do a ctrl+f on the website.

[Alex Meiburg]

Yeah I think it's just that one that I noticed