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