PhysLean moving again

Stream: PhysLean

[Joseph Tooby-Smith]

This is just to make this community aware that PhysLean may be moving organisation again, this time to leanprover-community where it will join with the QuantumInfo library run by @Alex Meiburg to form "Physlib" - a definitive library for physics in Lean.

This decision has been made to help prevent fragmentation, with a similar concept to CSLib and Mathlib.

This hopefully should not affect the experience of the average contributor to the project, though there may be some tweaking issues as this process takes place - for which I apologise.

[Rein Zustand]

But e.g. scipy and scikit-learn are 2 separate libraries and they don't overlap as much, even though the latter is a subset of the former? In fact, scipy is a dependency of scikit-learn: https://github.com/scikit-learn/scikit-learn/blob/0731b161ada9ef8a610c70f20ce0a969fb949e0b/pyproject.toml#L11. Wouldn't it be more modular to keep them separate?

[Alex Meiburg]

In principle, there's no common code at the moment - neither one has the other as a dependency, and I'm not aware of any particularly duplicated efforts. But I believe that in principle they should have common ground and common development. At a minimum, some of the more specific stuff to Hilbert spaces and CPTP maps (for instance) would make sense to share between them.

There's always room for more modularity, certainly. Isabelle's AFP, for instance, is very modular. But I think the big success of Mathlib has been precisely that it isn't modular, it's really trying to get everything together and tightly integrated, and that has been key to its success. I hope that eventually something similar can happen for physics. There's been a string of small "standalone" physics efforts lately which explicitly had zero interest in upstreaming anything, and there there definitely has been duplication of work, and/or poor or incompatible deifnitions, and I worry about a future where physics results end up scattered all over. (There are also projects that are trying to upstream and that causes me no worried, only happiness!)