New members

Stream: PhysLean

[Joseph Tooby-Smith]

This is a thread for people new to the project to say hi, ask beginner level questions, and get ideas of how to contribute to PhysLean.

If a conversation on a specific topic goes on for an extend amount of messages, it may be moved to its own dedicated thread - which is an equally good place to start. (Note that there is a general Lean channel for new members too, which can be found here - this thread is specific to PhysLean :)).

[Taewoo Lee]

Hello everyone! I am recent graduate of bachelor's theoretical physics and I found this project very interesting to contribute. I hope that I will be useful addition to your community! I have a lot to learn from you guys!

[Joseph Tooby-Smith]

Hi @Taewoo Lee ! What areas do you think you'd be interested in - or still exploring :)?

[Taewoo Lee]

I have been skimmed through the TODO list and I am working on "lemma deriv_tanh"

[Joseph Tooby-Smith]

Nice, so I think @Afiq Hatta is also working on this

• #PhysLean > QM reflectionless potential @ 💬

but no harm in having two different solutions :). Ideally there should be a way to assign one self to a TODO-item, but I have yet to think of a good way of doing this.

[Taewoo Lee]

yeah, we are working together now haha. I mean "physically."

[Afiq Hatta]

we are sitting next to each other!

[Afiq Hatta]

helping each other out

[Joseph Tooby-Smith]

Perfect! :grinning_face_with_smiling_eyes:

[Taewoo Lee]

I feel there are nothing much I can contribute after I read TODO list thoroughly, as I lack both physics and pure math skills, plus I only know numbers

[Afiq Hatta]

@Taewoo Lee you have come farther than most , don't be discouraged, you did well today!!!

[Joseph Tooby-Smith]

Hi @Taewoo Lee ,

As Afiq has said, you are really doing great!

Let me remark about the TODO items. The idea of the TODO items is that when someone is formalizing some area, they think of a result which would be nice to have but don't have the time to formalize it right there and then. A lot of them I wrote, and as such they are currently tilted to the stuff I have being formalizing. Given this, it is probably the norm rather than the exception for one to look at the TODO list and not find anything one is comfortable contributing too. This should be added to the fact that my writing is often quite poor (I have pretty badly dyslexia), and as such a lot of the TODO items are not as clear as they could be.
All that to say - don't be discouraged by the TODO list, as it only represents a very small subset of the ways one can contribute.

The projects ideas page contains another way to contribute - and this contains ideas from different areas and levels of physics. I appreciate that with these, there is something else scary about them, which is "where does one start" - but for a given project that is a great question to ask on the Zulip. There is also golfing and helping improve documentation :).

Let me finish with something generic: The apache software foundation (which is an organization that supports some open source projects) has a saying, called the Apache way, which says "community over code". That is building a great community is more important than building great code. This is something I stand very much by for PhysLean. The consequence being that I, and many others here, are very much willing to help new people join, give them advice, suggest ways to contribute etc. independent of their background or experience. At one point or another, we have all found formalizing physics or maths difficult - mainly because it is difficult, and if we can help someone else from what we have learned - even better :).

[Joseph Tooby-Smith]

@Taewoo Lee, here is one potential way to contribute, which is something similar to what you and @Afiq Hatta where working on yesterday:

The proof of this result related to the 1d quantum harmonic oscillator could (I think) be golfed, that is made shorter by using better tactics or combining the ones that already exist.

[Taewoo Lee]

@Joseph Tooby-Smith Thanks for kind word and advice. It really helps. I will try work on 1d quantum harmonic oscillator. Thank you so much :)

[Joseph Tooby-Smith]

Let me post here that I've made two tutorials on how to contribute to PhysLean via:

• informal lemmas and definitions: https://www.youtube.com/watch?v=f9kJyQs92TM
  
• and module doc-strings: https://www.youtube.com/watch?v=EOYH1aJdnnM
  

I plan to make some more, in particular one on golfing.

[Joseph Tooby-Smith]

Here is said tutorial on golfing proofs:

https://www.youtube.com/watch?v=QL-mjkPQDHs

[Joseph Tooby-Smith]

I got a university supplied computer, so made a tutorial on how to download Lean and PhysLean on a Mac (there was probably an easier way of doing this then waiting till I got a new PC, but alas):

https://www.youtube.com/watch?v=UvteqIDBj38

[Shlok Vaibhav]

I have been going through this tutorial (Mathematics in Lean) and found it really helpful and minimal:
https://avigad.github.io/mathematics_in_lean/mathematics_in_lean.pdf
It's a succinct 200 page pdf with accompanying light GitHub repo with lots of exercises and solutions. Screenshots of TOC and a sample page are attached:

Screenshot_20260109_235546_Chrome.jpg

Screenshot_20260109_235559_Chrome.jpg

[Kevin Buzzard]

We even have a shortcut for it -- #mil

[Joseph Tooby-Smith]

I've been messing around with YouTube shorts - since they seem pretty quick to make. Thought it was worth mentioning this one: https://www.youtube.com/shorts/V7YT3jK1mhk, on helping with the structure of PhysLean via the API graph.

[Gregory Loges]

Hi everyone!
I am new to lean (having done the Natural Number Game a few years ago and watched some of the more high-profile mathematics projects here as a casual observer) and interested in trying my hand at some formalization.
I had in mind to do the O(4) symmetry of the hydrogen atom which allows one to compute the spectrum (which to my knowledge is not yet in PhysLean). This approach avoids solving differential equations and special functions.

I see there has been some discussion last year about the Schroedinger equation and operators. What is the current status of angular momentum operators in particular? I think my first goal would be to define $L_{ij} = x_ip_j - x_jp_i$ and prove some basic facts such as $[L_{ij}, f(r)] = 0$ and $[L^2, L_{ij}] = 0$.

[Joseph Tooby-Smith]

Hi Gregory! I think this is a great place to start. I don't believe we currently have anything on the angular momentum operator, so starting here seems useful.

[Rianna J]

Hello! I've recently completed an MSc in theoretical physics and am interested in formalization. I was thinking of starting a new project with the goal of formalizing some of the key results in SUSY from Witten's papers, and wanted to start with the Witten Index. Just wondering about thoughts on this, thanks!

[Joseph Tooby-Smith]

Hi @Rianna J ! Nice to meet you! I think something like this is totally feasible, though may require a fair amount of work and prerequisites, so I wouldn't expect this to be an easy endeavour.

The most similar thing we have to this currently in PhysLean is the derivation of Wick's theorem (see e.g. https://arxiv.org/abs/2505.07939). It maybe be possible to use some of the definitions in this for e.g. defining the Witten index.

I think for projects like this, (which is also relevant to @Gregory Loges's message above), it is important to think about what the generally useful data structures, definitions and results are and build around these. These can act as smaller useful milestones which can be e.g. contributed to PhysLean, on the way to your main goal.

[Zhidong Zuo]

Hello! My name is Zhidong Zuo, I am graduated from Imperial for BSc and MSc Theoretical Physics. I am also a big fan of Ai for physics!

I used AI to scan the current master branch for missing content (Please correct me if I am wrong). I plan to start with the two most basic missing parts to get familiar with Lean and physlean: Galilean transformations and Poisson brackets.

Once I’m comfortable, I’m very interested in pushing forward the following areas:
GR:
Christoffel/Levi-Civita connection pipeline, explicit covariant derivative machinery for GR physics, Riemann/Ricci/scalar curvature, geodesic equation, Einstein field equations with a cosmological constant, Schwarzschild solution.
QFT:
Klein–Gordon, Dirac, and Proca equation modules; explicit Fock space formalism; S-matrix/Dyson series pipeline; path integrals and generating functionals; renormalization and the renormalization group.
Particle physics:
Yang–Mills theory and non-abelian symmetries.

I hope to find a set of best practices for using AI to automatically translate into Lean.

[Joseph Tooby-Smith]

Hi Zhidong, nice to see you on here! This sounds like a great starting point to me. Concerning the Galilean transformations there is this PhysLean#911 which might help specify the requirements