What would be useful for a beginners guide to PhysLean

Stream: PhysLean

[Joseph Tooby-Smith]

I'm thinking of putting together (or persuading someone else to put together) a webpage corresponding to 'A beginners guide to PhysLean'.

There is already a get involved page but I don't think this is too helpful for people who have never seen lean before.

I'm also not wanting to reinvent the wheel - there are some great resources out there for Lean more generally, and I think these should be linked to rather than reproduced.

Naturally it will link to the Natural numbers game, and @Tyler Josephson ⚛️'s lectures.

If anyone has suggestions of what would be useful here that would be great!
Maybe some sections like: "Adding your first definition", "Creating a new file", "Adding documentation"?

I'm particularly interested in hearing from actual beginners on what would help here, and what would lead them to get more involved.

[Tyler Josephson ⚛️]

I’ve been imagining, for a couple years now, a “Newton’s game” or something like that. The scaffold would be the natural number game, but the content would be physics.

[Tyler Josephson ⚛️]

I don’t have anyone working on this at the moment though.

[Daniel Morrison]

I can give my perspective as someone who found the project recently but has decent Lean knowledge, so my thoughts are less about learning Lean and more about the specifics of the PhysLean project.

• The link to the curated notes is broken.
• The informal results graph is empty, not sure if that is intentional or if something is broken.
• The mini-projects and the Github issues/project board are what I found most helpful.
• Adding more details to issues and the project board would be very helpful in understanding what you are looking for, right now it's a little vague and cover a potentially large amount of content. Small and specific issues are easiest to work with.
• What is really helpful is if you can structure sorry-ed theorem definitions and we know exactly what you are looking for.
• One question I had which I'm not clear on is what we want to assume in each situation, like I was looking at the classical harmonic oscillator and it's not clear to me how the system is being solved. Like is it ma = F = -kx or conservation of energy or what? What are we taking as the most fundamental thing we assume and prove everything else with? I guess in some sense this is partly what we are figuring out, but it's very hard to think about structing a lean file without that information. (I expect this is a lot harder than the other items I've listed here)

[Joseph Tooby-Smith]

Many thanks for this Daniel! This is extremely useful.

Let me address your comments in turn:

• The link to the curated notes is now fixed.
• Yeah the informal results graph is broken I think. I've removed the link to it from the website until it's fixed. Informal definitions and lemmas still appear in the TODO list.
• Good to know the mini-projects and the Github issues/project board are useful.
• I understand that the lack of details in the issues and todos and project board etc is a fairly big problem. Some of them I only a vague idea of what is wanted (but I think even making this clear would be helpful). I plan to make an effort to go through and improve these sometime soon.
• I want to keep PhysLean sorry-free but I think proof_wanted is something which can be used here. There is an open issue regarding this here.
• I think your last point may be solvable with better documentation. But yeah, I think this is part of the challenge of this whole project. In the actual case of the classical harmonic oscillator, currently nothing is being solved and there are some TODO items related to this.

Thanks again Daniel!

[Joseph Tooby-Smith]

I've created an GitHub issue regarding the classical harmonic oscillator. See here. There are a number of other modules where this sort of issue can be made.

[Joseph Tooby-Smith]

To help with improving details in issues and projects I've made it so that each TODO item has a unique tag so it can be uniquely referred to and linked to. For example:

• TODO (6VZG4): file PhysLean.ClassicalMechanics.HarmonicOscillator.Basic

This allows the creation of issues like this - and hopefully issues regrading improvements of the TODO items.

[Joseph Tooby-Smith]

Concerning proof_wanted I've updated things so that you can now use semiformal_result. This is essentially the same as proof_wanted but it made so it appears in the TODO list, can handle definitions and accepts a tag (see above point). An example is:

• semiformal_result (6V2FZ): gaugeGroupℤ₆SubGroup (Click the See on GitHub button to see the implementation).

And I'm in the process of adding some more related to electromagnetism.

[Daniel Morrison]

This is a nice improvement! For tags, will it generate the labels for us or do we need to specify a label? If we need to specify the tag, is there a system to avoid duplicating tags?

Also, if I can wish for something on the TODO list, it would be great to sort by TODO/informal def/informal lemma.

[Joseph Tooby-Smith]

You can generate tags with lake exe make_tag- which produces a tag based on time since the Unix epoch. There is also (as a back up) a system which checks for duplicate tags.

I'll see what I can do regarding sorting.

[Joseph Tooby-Smith]

I've added filters to the TODO list to separate based on TODO, informal def etc.

[ZhiKai Pong]

A section on github basics, e.g. how to setup PhysLean (just fork the repository?), how to create a new branch, how to push etc. is probably helpful

Maybe something like https://leanprover-community.github.io/contribute/index.html that outlines the overall workflow

[ZhiKai Pong]

Some general comments as a beginner: currently SpaceTime seems to be central to defining everything happening in "our usual 3D space", but the set up is quite obfuscated. If this is necessary then I feel like there should be documentation (and tutorial) to explain how things are defined and how to use definitions within it etc.

[Joseph Tooby-Smith]

@ZhiKai Pong Agreed. The reason SpaceTime is set up in this way is so it works nicely with index notation. I agree this needs better documentation and a better API around it. Maybe this should be a short-term priority.

[Joseph Tooby-Smith]

Regarding the 'Beginners guide' this is what I have so far:

https://physlean.com/GettingStarted

I might have gone a bit over-the-top with the colors.
It's source files etc are located here:
https://github.com/HEPLean/PhysLean_Website

[Joseph Tooby-Smith]

Joseph Tooby-Smith said:

ZhiKai Pong Agreed. The reason SpaceTime is set up in this way is so it works nicely with index notation. I agree this needs better documentation and a better API around it. Maybe this should be a short-term priority.

Maybe https://notes.physlean.com is a good place for us to put detailed documentation etc. related to space-time. I created an issue regarding this here.

[ZhiKai Pong]

Joseph Tooby-Smith said:

Regarding the 'Beginners guide' this is what I have so far:

https://physlean.com/GettingStarted

I might have gone a bit over-the-top with the colors.
It's source files etc are located here:
https://github.com/HEPLean/PhysLean_Website

Currently I don't think there's a link to the "getting started" page, might want a link from the get involved page (and maybe the PhysLean readme as well?)

[Joseph Tooby-Smith]

Thanks @ZhiKai Pong . I added it to the readme as well as the get involved page.

[ZhiKai Pong]

https://physlean.com/GetInvolved.html

It's not displaying for me yet, is there a delay in the site updating?

[Joseph Tooby-Smith]

Ugh, thanks for pointing this out. The website build failed, because there was a duplicate TODO tag in PhysLean. I've fixed this but it will take a couple of hours to update from here.

[Joseph Tooby-Smith]

(Just made a related issue which will prevent this).