Seattle, WA

Stream: Geographic locality

[Gabriel Ebner]

:mountain:

[Sebastian Ullrich]

https://ismtrainierout.com/?

[Adam Topaz]

https://www.google.com/maps/dir/seattle/whistler/@48.857543,-123.8449303,8z/data=!4m14!4m13!1m5!1m1!1s0x5490102c93e83355:0x102565466944d59a!2m2!1d-122.3320708!2d47.6062095!1m5!1m1!1s0x54873cb203957b87:0x4ab741e875f5cff6!2m2!1d-122.9535117!2d50.1161686!3e0

[Eric Wieser]

I'll be around in Seattle either side of this weekend, looks like there's lots of smoke in store for me...

[Adam Topaz]

Welcome to the west(ern North America)

[Gabriel Ebner]

looks like there's lots of smoke in store for me...

Right now the smoke isn't nearly as bad as it sounds. You can see the haze when you look across the lake, but I can't even smell it.

[Xiyu Zhai]

I'm going to be PostDoc in UW starting September. Any other Lean fanatics in UW? I didn't know anyone from my current school.

[Adam Topaz]

Jarod Alper is (or at least was) interested in formalization, and I think there was a group of a few other people there as well.

[Adam Topaz]

Are you going to be a postdoc in math, cs, something else?

[Kevin Buzzard]

My impression was that maths department chair Max Lieblich was interested in Lean and in particular in establishing links with Leo's group, as Leo is also based in Seattle.

[Adam Topaz]

Oh, I didn't know Max was also interested in this!

[Xiyu Zhai]

I’m going to be a postdoc in cs, machine learning stuffs. I’m trying to combine the powers of llm and formalisation to avoid hallucinations.

[Adam Topaz]

I assume you know about #Machine Learning for Theorem Proving ?

[Xiyu Zhai]

I am also a great fan of number theory though. I attend the number theory class of Professor Wei Zhang at mit. I planned to learn the full proof of FLT before graduation, but it seems I’m too busy though.

[Xiyu Zhai]

Adam Topaz said:

I assume you know about #Machine Learning for Theorem Proving ?

Yeah, I know. I recently read a lot on that thread

[Newell Jensen]

I am in Vancouver WA, about 3 hour drive south of you. Would be nice to see Lean take off at UW (I got my Masters there in Electrical Engineering over a decade ago FWIW). I would be up for taking the train up there for a hackfest or something of that sort if it ever got organized. Best of luck on the postdoc.

[Xiyu Zhai]

Great to hear that! Looking forward to seeing you there!

[John Leo]

Sorry I'm seeing this late @Xiyu Zhai but I'm at UW and am interested in Lean as well. I was an undergrad at MIT and did a PhD in number theory at UCLA; I'm now a guest of the PLSE group in UW CSE. I've also talked briefly with Max Lieblich and he is indeed very interested in Lean and apparently has a couple students working with mathlib. There are some people in PLSE also interested in Lean and a chance the graduate PL class might convert from Coq to Lean next school year. Look forward to meeting you this Fall!

[Patrick Massot]

If there are courses using Lean there then don’t forget to submit a contribution to https://leanprover-community.github.io/teaching/courses.html

[Xiyu Zhai]

John Leo said:

Sorry I'm seeing this late Xiyu Zhai but I'm at UW and am interested in Lean as well. I was an undergrad at MIT and did a PhD in number theory at UCLA; I'm now a guest of the PLSE group in UW CSE. I've also talked briefly with Max Lieblich and he is indeed very interested in Lean and apparently has a couple students working with mathlib. There are some people in PLSE also interested in Lean and a chance the graduate PL class might convert from Coq to Lean next school year. Look forward to meeting you this Fall!

Great! See you there soon!

[Vasily Ilin]

Patrick Massot said:

If there are courses using Lean there then don’t forget to submit a contribution to https://leanprover-community.github.io/teaching/courses.html

I added the course I am teaching at UW now!

[Vasily Ilin]

The UW people here may be interested in the newly-created Math AI seminar. The broad focus of the seminar is math-computer interaction, with emphasis on math formalization and machine learning. Two sample talks are: one, two. If you want to receive emails about future events, subscribe to the mailing list here: https://lists.uw.edu/postorius/lists/math_ai_seminar.lists.uw.edu/.

[Vasily Ilin]

John Leo said:

Sorry I'm seeing this late Xiyu Zhai but I'm at UW and am interested in Lean as well. I was an undergrad at MIT and did a PhD in number theory at UCLA; I'm now a guest of the PLSE group in UW CSE. I've also talked briefly with Max Lieblich and he is indeed very interested in Lean and apparently has a couple students working with mathlib. There are some people in PLSE also interested in Lean and a chance the graduate PL class might convert from Coq to Lean next school year. Look forward to meeting you this Fall!

Are you still at UW? I would be happy to tell you more about our Lean group. It's led by Jarod Alper, we have 3 PhD students (including me) involved, and several undergrads.

[Carina Hong]

Hi JMM Lean folks!

If any Lean expert is at JMM in Seattle right now and would like to discuss about Lean infra / what would be great to have (like a hammer!) and also to just nerd out together, please hit me up! I can be found either here at Zulip, or via 650-201-2166 (text/ WhatsApp/ signal). As a mathematician I'd love to understand the engineering aspect of Lean more, so pardon my questions in advance!

Best,
Carina

[Andrés Goens]

Maybe this could be more visible in the #Geographic locality stream? (No idea what JMM is, but it sounds like it's some place in the USA from your description)

[Andrés Goens]

also note that this stream is web-public, so in principle your phone number could be googleable from this post (sorry if you knew this already, just making sure)

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

It's the Joint Mathematics Meetings :)

[Jason Rute]

Which is the largest annual mathematics conference in the United States.

[Notification Bot]

5 messages were moved here from #lean4 > JMM Lean Infrastructure Wishlist Chat by Kevin Buzzard.

[Kevin Buzzard]

I've moved the discussion because it's probably not of interest to most people who follow #lean4 and may be of interest to people in Seattle who don't follow #lean4 . Regarding googling phone numbers; AFAIK google doesn't index Zulip, but anyway this channel is not web-public.

[Adam Topaz]

I’ll be in Seattle at about 11am today. Would be great to meet up with some Lean folks!

[Jason Rute]

Any talks that people at JMM recommend? (I had to come late, but I’m here now.)

[Carina Hong]

There’s a whole afternoon session at skagit 2 at 800; and then 5-6 Yann Lecun lecture; tomorrow again morning session 8-12 all cool stuff skagit 3 at 800; then 1-2:30 4C at 705; and 5-6 Jarod Alper lecture

[Carina Hong]

A few of us plan to meet at Cheesecake factory at 7:30pm tonight for dinner to talk about AI4math, formalization, cool project ideas etc! Join us if you can:)