Pittsburgh, PA

Stream: Geographic locality

[Koundinya Vajjha]

Pittsburgh represent!
The Pittsburgh area has a very active Lean community, centered around Carnegie Mellon University and the neighboring University of Pittsburgh.

We have weekly Lean meetings every Tuesday at 4.30pm in Thackeray Hall at Pitt. (At least we used to, until the university closed down.)

[Jeremy Avigad]

We use the cmu-lean mailing list on Google groups for the weekly meeting announcements. It is a private mailing list but anyone is welcome to join. You should be able to find it on Google groups and click a button to send a request, but in any case you can email me at avigad@cmu.edu and I will send an invite.

The meetings are informal. Sometimes we just talk shop, but I generally try to line up a volunteer to present something they are working on or a paper they are reading, or lead a discussion. The topics are not restricted to Lean; participants are generally interested in all aspects of formal methods and their applications to mathematics.

We have had a few meetings by Zoom since the lockdown began. We'll take a break this week, but we're still planning to meet sporadically, as people volunteer to present. I have nearly all the slides done for a talk I was going to give at a phil math conference last week (https://princetonphilmath.wordpress.com/), so I'll present those a week from Tuesday (April 21) unless we get a better offer.

[Tim Daly]

Tim Daly

Out near the KPIT airport, just behind the Raccoon State Park.

[William Sealy Gosset]

I am in Bethel Park. Once this whole pandemic thing has resolved itself, I hope to become more involved with the Lean community at CMU and Pitt. My background is in financial engineering, and as a result my mathematics background is more on the applied side.

[Tomas Skrivan]

Just arrived to Pittsburgh, I'm joining CMU to work on scientific computing in Lean. Looking forward to meeting everyone!

[Kevin Buzzard]

Oh that's great news! Expecting more great things from SciLean!

[Joel McCracken]

Hi, I'm in Pittsburgh. I don't know how involved I will be with the local lean community, but if I can make any event I will do it! I'm a professional programmer, write haskell in my day job, and interested in Lean.

[Joel McCracken]

Also, I help run the pgh functional programming meetup group. We haven’t really had many events since pandemic, but our slack chat is active and we get together many weeks via zoom to chat about what we’ve been hacking on lately. If any of you are interested, let me know and I’ll get you an invitation. And if anyone would like to give a talk on any topics, either over zoom or in person, we’d be happy to host you!

[Jeremy Avigad]

@Joel McCracken, we've been doing an informal software verification reading group at the Hoskinson Center at Carnegie Mellon on Fridays at 10am. (There is no meeting this week; it's spring break.) If you might want to attend some of them, let me know, and I'll send you an invite to our Google group mailing list.

[Joel McCracken]

@Jeremy Avigad Sure, i'd love to be on the mailing list at the very least; you can send the invite to mccracken.joel@gmail.com

[Joel McCracken]

Funnily enough, I just read http://philsci-archive.pitt.edu/20979/7/talk_archive.pdf

[Patrick Massot]

I just joined the Hoskinson center in Pittsburgh for one year! During the fall semester I'll be at CMU for sure at least on Monday, Wednesday and Friday since I'll be teaching interactive theorem proving those days.

[Timo Carlin-Burns]

Hi all, big Lean enthusiast here. I'll be in Pittsburgh tomorrow and would love to pop by the Hoskinson center and introduce myself! Would that be okay? If so, let me know if there's a better or worse time. I'm a big fan of all of your work, and I'm hoping to become a more active contributor to the Lean ecosystem in the coming months.

[Patrick Massot]

I won’t be on campus tomorrow, sorry.

[Tomas Skrivan]

Hey Timo, I'm happy to meet. I have office at the Hoskinson center and will be there the whole day tomorrow.

[Tomas Skrivan]

Too bad you are not coming today as we have a weekly meeting and you could meet more people. Otherwise people are spread all around the campus or working from home.

[Jason Rute]

I will be visiting Pittsburgh from Saturday March 30 to Saturday April 6. If anyone wants to get together and chat in that time frame, e.g. @Sean Welleck, @Jeremy Avigad, @Patrick Massot, @Mario Carneiro, @Wojciech Nawrocki, and others (I'm not sure who all is in Pittsburgh right now), I'd love to schedule something.

[Patrick Massot]

I’ll be around, and happy to talk. I’m usually on campus on Mondays, Wednesdays and Fridays. We have the weekly Hoskinson center meeting on Wednesday afternoon at 4:30 where you are very welcome.

[Timo Carlin-Burns]

I just moved to Pittsburgh and will be studying math at CMU this semester! I'm looking forward to seeing some of your faces around campus :)

[Li Xuanji]

Are the Wednesday Hoskinson center meetings happening tomorrow? I would like to check it out if so

[Jeremy Avigad]

No, we take a break over the summer, because lots of people travel, do internships, or work at home. But some of us are around; I'll be on campus on Thursday. Are you in Pittsburgh? If so, how long will you be here?

[Li Xuanji]

I work and live here! (I’ve just been generally not free on Wednesdays)

[Nadim Farhat]

Hi, I just found out about this channel . did the weekly meetings resume?

[Nadim Farhat]

I should have introduced myself. I am Nadim , I have been in Pittsburgh since 2012 . I have been working in scientifc computing ever since, from medical image analysis , to electromagnetic and ultrasound simulation to medical robotics. I earned my PhD from University of Pittsburgh working at ultra high field MRI . When i was trying to prove some propostions by Jaynes in his book Probability theory , I found i am incapable to verify my own proofs. so I started looking for computer assisted proofs which led me to lean 4

[Jeremy Avigad]

We're meeting at 4:30 today as usual in Baker Hall 139, and online at cmu.zoom.us/my/avigad. Nadim, you are welcome to join us any time. Shall I add you to our mailing list? It's usually just a weekly reminder.

[Nadim Farhat]

Yes can I be added to the mailing, please use nadim.farhat@gmail.com. This time i will join online. Thank you for the invite.

[Anish Rajeev]

Hi, I'm Anish; Im a current undergrad studying math at CMU, mainly interested in formal logic and programming languages. I've been programming in lean for the past 1-2 months and have been really enjoying it. I was curious if these meetings still happen, and if I could also be added to the mailing list?

[Jeremy Avigad]

@Anish Rajeev I just sent an invite!