Zulip Chat Archive

Stream: Geographic locality

Topic: San Francisco Bay Area, USA

Jalex Stark (Feb 28 2020 at 03:52):

I know at least one person who has been active on this server and lives in the Bay. (If someone else comments on this thread claiming to be in the Bay, I'll try to connect the two of you.)

Scott Morrison (Feb 28 2020 at 04:13):

I'm in the East Bay (Berkeley) for the next few months.

Rajiv (Apr 12 2020 at 16:14):

I am just starting with Lean. (In the process of getting the toolchain, emacs etc., setup). Currently in Cupertino. Once the shelter-in-place is over, will be heading to Bangalore, India.

Nam (Apr 12 2020 at 17:49):

I'm in Sunnyvale.

Grayson Burton (Apr 14 2020 at 05:03):

I'm in Santa Rosa :)

Noah Gundotra (Jul 13 2020 at 02:30):

I’m in San Jose!

Sam Estep (Jul 25 2020 at 16:37):

I'm in Menlo Park until August 15, then Mountain View :)

Alok Singh (S1'17) (Oct 01 2020 at 20:47):

berkeley

Kevin Buzzard (Oct 01 2020 at 22:36):

You're not the only one @Alok Singh (S1'17) -- have you seen #Berkeley Lean Seminar ?

Scott Viteri (Apr 15 2021 at 06:25):

Palo Alto

Haden Hooyeon Lee (May 15 2021 at 09:05):

I'm in SF

Nicholas (Jul 20 2021 at 02:22):

Hello all, Im in the south bay! Drop me a message if you want to Lean together :)

Paul Zeitz (Sep 30 2021 at 18:28):

Hi, I'm a newbie, living in Marin county. Waiting for the natural numbers game to get back online...

Kevin Buzzard (Sep 30 2021 at 22:15):

Sorry :-/

Ryan McCorvie (Jul 24 2022 at 20:47):

Hi Bay Area folks, I live near Berkeley in Oakland and am diving into lean and theorem proving. Let me know if you want to meet up.

Kyle Miller (Jul 24 2022 at 20:58):

(Ping @Thomas Browning and @Patrick Lutz, at UC Berkeley.)

Thomas Browning (Jul 24 2022 at 21:24):

Patrick Lutz is now at UCLA. But I'm still at Berkeley, and we've got a weekly Friday meeting at 11am, if you're interested.

Tom (Aug 07 2022 at 22:03):

Hello there, what is the typical content of these meetups? What aspects of Lean do you mostly focus on?

Moritz Doll (Aug 28 2022 at 17:03):

I am in Berkeley for a month

Rudi Cilibrasi (Oct 31 2022 at 04:07):

I live in Concord, California. Lean newbie but wrote a first order predicate logic linear resolution theorem prover using skolemization in the 1990's.

Evante Garza (Nov 01 2022 at 00:56):

Rudi Cilibrasi said:

I live in Concord, California. Lean newbie but wrote a first order predicate logic linear resolution theorem prover using skolemization in the 1990's.

Hello neighbor! I'm in Pittsburg, just over the hills from you.

Paul Wintz (Jul 17 2023 at 08:50):

I'm a PhD student at UC, Santa Cruz looking into applying Lean to dynamical systems and control theory.

Matthew Ballard (Dec 14 2023 at 14:36):

I'll be in the Yay area for the Spring (SLMath/MSRI). I am guessing there will be critical mass for something regular there.

Moritz Firsching (Jan 20 2024 at 16:17):

I'm in San Francisco now for a week, happy to meet people in the bay area. Ping me if you are interested or there is some lean talk going on..

Quinn (Feb 22 2024 at 00:14):

greetings. in berkeley. been writing coq (occasionally professionally, mostly personal side projects) for longer than I've been a professional dev of any kind. thinking about switching to lean

Thomas Browning (Jun 04 2025 at 17:15):

@Jasper van de Kreeke and I are holding a Lean camp this Summer, Fridays at 1pm in Evans 891, starting with two warm-up session on June 13 and June 20, and further weekly sessions throughout June-Aug. Anyone is welcome to join! Communication will take place in the #Berkeley Lean Seminar channel.

Matthias Köppe (Jun 13 2025 at 18:46):

Greetings from Davis, CA, where we pretend to be part of the Bay Area too sometimes

Srayan Jana (Sep 01 2025 at 16:55):

Hi! I'm East Bay, nice to meet yall!

Rado Kirov (Sep 01 2025 at 18:12):

Anybody interested in meeting in SF sometime after work or weekends?

Srayan Jana (Sep 01 2025 at 18:34):

I would be down. It would probably be a good idea to meet up at Sudo Room or Noisebridge though

Rado Kirov (Sep 24 2025 at 05:12):

I am going to try to see if there is interest in running a mini course on doing Tao's Real Analysis exercises in Lean with in person meetings somewhere in SF - #Analysis I > Teaching a class on Analysis I with Lean outside academia? @ 💬 Still gauging interest, but if someone has ideas how to get book venues for such meetups, please reach out.

Greg Shuflin (Nov 04 2025 at 05:22):

Rado Kirov said:

I am going to try to see if there is interest in running a mini course on doing Tao's Real Analysis exercises in Lean with in person meetings somewhere in SF - #Analysis I > Teaching a class on Analysis I with Lean outside academia? @ 💬 Still gauging interest, but if someone has ideas how to get book venues for such meetups, please reach out.

hey @Rado Kirov . there's a separate thread in this geographic localities section for San Francisco specfically, but it probably does make sense to have one common bay area location thread. anyway, the lean4 meetup in sf is currently on haitus as far as I'm aware, but I was attending it at the beginning of the year. it was being held at the Noisebridge hacker space, and if someone wanted to revive it, that might be a good option

Rado Kirov (Nov 04 2025 at 06:50):

I see @Alok Singh and @Kyle Ellefsen were previously attending the noisebridge meetup and they are regulars at this Build Mathematics from Scratch with Lean workings group we have been running the last month at MoxSF. We can chat next time about reviving the meetup if enough people are interested (the intent is different from the real analysis working group, but there might be enough interest in doing both). I never made the meetup previously because it was during work hours.

Alok Singh (Nov 04 2025 at 22:58):

Yo @Greg Shuflin come next Monday at 7 if you can it’s at mox

Last updated: Dec 20 2025 at 21:32 UTC