Social Media

Stream: PhysLean

[Joseph Tooby-Smith]

So I often post about PhysLean on my own personal social media accounts (usually LinkedIn - which is the only one I really have), but last week I created a bluesky account for news related to the project:

:link: https://bsky.app/profile/physlean.bsky.social

The idea is to post about things happening in the project, and anything else related, with the aim to increase visibility amongst physicists.

If anyone has ideas for posts or anything else related to this, or wants to help run the account, this is a thread for that :).

[Alok Singh]

Twitter =)?

[Joseph Tooby-Smith]

Made a twitter account a few days ago - although haven't put so much effort into this yet: https://x.com/PhysLean

[Joseph Tooby-Smith]

New mastodon account: https://mathstodon.xyz/@PhysLean

[Afiq Hatta]

fwiw i have a plan to casually blog about my first commits to physlean on my blog + some motivating statements - the substack got around 10k views a month so hopefully would give physlean some visibility. https://chillphysicsenjoyer.substack.com/

[Joseph Tooby-Smith]

Nice! This would be very much appreciated :slight_smile: .

[Afiq Hatta]

i am surprised to the upside about the reception of this post

#PhysLean

its got 18 substack likes, which is a lot in the substack world!

[Afiq Hatta]

https://chillphysicsenjoyer.substack.com/p/we-should-formalise-physics

[Joseph Tooby-Smith]

Awesome! Thanks for writing this @Afiq Hatta and helping spread the word :).

[Afiq Hatta]

https://chillphysicsenjoyer.substack.com/p/try-to-prove-math-with-computers

[Afiq Hatta]

a more walkthroughy post for noobs like me ;)

[Kevin Buzzard]

I am slightly concerned that people will read this post and come away with the feeling that proving 0 <= 2 in Lean is somewhat of a complicated adventure, when in fact it is just closed immediately with the mathlib tactic norm_num, something which is never mentioned in that post.

[Kevin Buzzard]

Put another way, someone reading that post might think "wow, so presumably proving 1 <= 5 is basically impossible in Lean because it was so much work to prove 0 <= 2". Might I suggest that you mention at the end that

import Mathlib.Tactic

example : 37 ≤ 1000000 := by
  norm_num

works fine?

[Afiq Hatta]

good point @Kevin Buzzard - it was meant to be a pretty contrived example. I think what I'll do is put a healthy disclaimer in the beginning that there are standard libraries out there!

[Afiq Hatta]

really grateful for the feedback. i'll also put that piece of code at the bottom

[Afiq Hatta]

@Kevin Buzzard updated the post