Boston, USA

Stream: Geographic locality

[Alex J. Best]

I'm in Boston, no idea if there are any other lean users in the area!

[Jason Rute]

I live in Somerville. MA. USA and work in Cambridge. MA. USA. Obviously I’m not leaving my home anytime soon, but when the CoronaVirus thing lets up I’d by happy to meet up with Boston area Lean users.

[Sam Stites]

I'm in Somerville as well! I used to try to do a daily lean exercise (I'm very new) but I'm currently in deadline mode. I'm thinking of trying to go through https://mitpress.mit.edu/books/topology after, mid May.

[Miguel Raz Guzmán Macedo]

Mexico City, Mexico / UNAM

[Jalex Stark]

I just moved to Cambridge. I'm happy to meet people outside for distanced, masked conversations / walks.

[duck_master]

I'm somewhere around this area too! (I don't want to give much more info because of privacy.)

[Zygimantas Straznickas]

+1 for Cambridge MA. Happy to meet and talk about Lean 4 and applying ML for theorem proving once people are vacinnated!

[John Burnham]

I'm also in the Boston area!

[Xiyu Zhai]

+1 Cambridge MA

[Omri Schwarz]

+1 MA, USA (Medford)

[Kyle Miller]

Hi @Omri Schwarz!

[Chris Martens]

hello from jamaica plain! i'm faculty at Northeastern

[Peter Li]

Chris Martens said:

hello from jamaica plain! i'm faculty at Northeastern

Hey Chris, I'm a third year CS undergrad at Northeastern, are you a professor in the math department?

[Graham Leach-Krouse]

Hi Everyone. I just moved to (just outside of) Boston, now residing in Arlington. Formerly faculty at Kansas State University, soon to be joining Draper Laboratory.

[Michael Fishman]

Greetings! I live in Boston. I work as an ML engineer at Boston Dynamics AI Institute in Cambridge. I'm studying lean on the side.

My interests in lean are:

1. I want to express stronger guarantees about programs
2. I want to close the gap between math theory and the algorithms that implement it
3. I want math to be more inspectable. Often when trying to understand math in a paper, I want to see what the types of the terms involved are, and more detailed or alternative proofs of the statements.
4. I occasionally want to prove theorems

Let me know if any of you want to meet up!

[Tyler Josephson ⚛️]

Welcome! You may it helpful to subscribe to the #Machine Learning for Theorem Proving stream - though more often, discussions are about applying machine learning to theorem proving rather than applying theorem proving to machine learning

[Michael Fishman]

Tyler Josephson ⚛️ said:

Welcome! You may it helpful to subscribe to the #Machine Learning for Theorem Proving stream - though more often, discussions are about applying machine learning to theorem proving rather than applying theorem proving to machine learning

Thanks for the suggestion!

[Mark R. Tuttle]

I'm learning Lean at Amazon in the Seaport district of downtown Boston. I'm interested in connections between Lean and protocol verification and machine learning.

[Derek Rhodes]

Hi everyone, I'm a programmer located just to the north in New Hampshire, hoping to move down to the greater Boston area, possibly NYC. My relevant interests are in online math education with Lean, but I'm also planning to learn more about formal verification for both software and hardware.

[Alok Singh]

I am also in Boston now

[Rob Simmons]

I didn't mention I was in Boston when I joined the Zulip (though my partner @Chris Martens did) but I've joined the FRO as of Monday as (I believe) the FRO's first Boston representative, hello Boston Lean folk!

[Anthony Wang]

I'm an undergrad at MIT and also in the Boston area!

[Ammar Husain]

I am in this area

[Alok Singh]

Would any of you guys like to meetup sometime? I’m in the cic building downtown Kendall square

[Anthony Wang]

Sure! Kendall Square is within walking distance of where I live so maybe we could meetup somewhere there?

[Gavin Zhao]

Undergrad at Brown. I'm in Providence but I'm often in Boston during weekends, happy to meet up too!

[Joris Roos]

I'm in Allston, would be down for meetups!

[Alok Singh]

This week?

[Michael Fishman]

I’m down to meet this week. I work in Kendall. Want to get lunch or coffee on Thursday?

[Rob Simmons]

There's a food truck at MIT Open Space (292 Main St) on Thursday, what about a noon meetup?

[Javier Burroni]

I'm in Amherst, MA.
I cannot make it this Thursday, but I would like to join you for a larger event!

[Anthony Wang]

Thursday at noon at the MIT open space works for me!

[Olivia Brode-Roger]

hi! I should be able to make it. I'm a Somervillain, former MIT under+grad and current Brown PhD

[Gavin Zhao]

*sad Providence noises

[Gavin Zhao]

Can't make it Thursday unfortunately, happy to meetup next time!

[Rob Simmons]

The weather today is awful — what do people think about a rain check to next Thursday? @Olivia Brode-Roger @Anthony Wang @Michael Fishman @Alok Singh

[Jason Rute]

I'm open to meet sometime (I live in Somerville), but I'm out of town this week.

[Alok Singh]

I can still meet up, I’m at Kendall anyway

[Alok Singh]

In case anyone feels like braving the rain

[Zixiao Wang]

Hi boston gang! This is Zixiao a PhD at Harvard, great to connect here! are we still meeting this thursday?

[Zixiao Wang]

Also, I am working on math agent and seeking collaboration, DM if you are open to chat!

[Rob Simmons]

I'm up trying again Thursday though I won't be able to stay long (potentially have to leave around 12:30).

Unfortunately last Thursday was the last food truck Thursday at MIT Open Space, are there any good fast-take-out or easy-to-gather (ideally outside?) environments people know of? Unfortunately we're reaching the end of eating-outside season but I'd greatly prefer that even if it's nippy.

[Cody Roux]

I kind of miss Mamaleh, maybe they do takeout? We can chill in that area maybe

[Michael Fishman]

I’m down to meet near mamelah tomorrow

[Anthony Wang]

Sounds good. Is this the Mamaleh's with address 15 Hampshire St?

[Cody Roux]

Yep, that's the one

[Rob Simmons]

Sounds great, see people there noonish (managed to reschedule my conflicting appointment)

[Cody Roux]

Ah poops, my pup is sick, I'll probably stay home with her, sorry.

[Cody Roux]

PXL_20251002_122328139.jpg

[Jason Rute]

I don't know if I can make it today, but if I do, what is the plan exactly? Where and when?

[Michael Fishman]

Meet in or outside mamelah’s at noon. I’ll ping this thread when I get there.

[Rob Simmons]

(Mamelah’s on Hampshire street in Cambridge)

[Michael Fishman]

I’m at mamelah’s in black pants, black hoodie, black hat, green/blue shirts

[Rob Simmons]

Be there in a moment, blue constructive logic hoodie

[Cody Roux]

Rob will be witnessably there

[Rob Simmons]

Good seeing you @Anthony Wang and @Michael Fishman !

[Rob Simmons]

@Cody Roux I also made this as a future existential witness to meetups image_picker_C6B976DE-C1DA-4D71-9E66-F082C515073C-1402-0000004E20DD8F41.jpg

[Cody Roux]

I am seeing a lot of people calling the tool LEAN rather than Lean.

[Rob Simmons]

Please do not shout, already leaning and might fall over

[Rob Simmons]

Alternatively we could make a good backronym

[Cody Roux]

Fine, but I'm pronouncing it Lee-anne

[Rob Simmons]

Ok Cod-E :fish:

[Cody Roux]

Logic Enabled Automated Nathematics is my vote

[David Renshaw]

Logic Enforcer Automating Nitpicks

[Cody Roux]

Aggravating Nitpicks

[Rob Simmons]

I'd like to propose 2025-10-23T12:00:00-04:00 for an encore; Mamelah’s on Hampshire street in Cambridge was a good location, and has reasonable indoor seating as well as outdoor seating in case the weather makes outside infeasible.

[Zixiao Wang]

i would be down for it! Sorry didnt catch the message last time...

[Anthony Wang]

Are we having a meetup again this Thursday?

[Rob Simmons]

Let's do it! Weather looks passable for still sitting outside, Mamelah’s on Hampshire street in Cambridge at noon. CC @Anthony Wang @Zixiao Wang @Michael Fishman @Cody Roux and either @Nehal Patel or @Nehal Patel , who gave a :thumbs_up: on the Oct 3 post.

[Cody Roux]

I'll try, though things are a little crazy on my side

[Jason Rute]

I'll see if I can make it. I often have a meeting on Thursdays at noon.

[Nehal Patel]

I should make it -- cheers, nehal

[Michael Fishman]

I’ll be there

[Jason Rute]

I'm going to try to make it, but I'll also be a bit late. (I'm ending a meeting at noon-ish and then I need to bike over.)

[Cody Roux]

I'll also try to make it

[Cody Roux]

I had fun!

[Nehal Patel]

Same here! Nice to meet everyone

[Nehal Patel]

@Jason Rute

Here are the steps to quickly get up and running with claude-code and Lean

<install node.js>
> npm install -g @anthropic-ai/claude-code
> claude

in claude, run:

/plugin marketplace add cameronfreer/lean4-skills
/plugin install lean4-theorem-proving
/plugin install lean4-memories

And then tell it what to do:

in @McpDemo/Basic.lean  add a theorem for adding the first n natural numbers. In the comment
  above, add a natural language statement of the same theorem

For the first attempt, having a video reference is probably useful -- have a look at this (suggest running it at 2-3x speed):
https://www.youtube.com/watch?v=zderx5uXoWE

See everyone at the next meetup!

[Nehal Patel]

https://github.com/cameronfreer/lean4-skills

[Cody Roux]

Unrelated, but here's a Lean MCP server: https://github.com/oOo0oOo/lean-lsp-mcp

[Nehal Patel]

these two projects are pretty related -- same folk contribute to both -- lean-mcp-server has been around for a few weeks, lean-skills is the latest thing, came out a few days ago, lean-skills launches lean-lsp-mcp_server for you

[Cody Roux]

Leans Kills... sounds ominous

[Jason Rute]

Thanks @Nehal Patel ! That also reminds me. We should invite @Cameron Freer to our next Cambridge Lean hangout.

[Cameron Freer]

Thanks, @Jason Rute -- I'd be excited to join next time!

[Cameron Freer]

re the LSP MCP, here is what the skill tells Claude about some ways to interact with it (based on patterns that I've found helpful):
https://github.com/cameronfreer/lean4-skills/blob/main/lean4-theorem-proving/references/lean-lsp-server.md

[Nehal Patel]

Small world

[Rob Simmons]

Same time same place next Thursday possibly?

[Cameron Freer]

I'll be out of town next Thursday, but could join earlier in the week, or the week after. Or if the meeting does happen on Thursday, I hope to meet you all the next time!

[Jason Rute]

Tuesday and Friday work well for me if we want to switch days. Thursday is a maybe.

[Cameron Freer]

Tues Nov 11 works well for me (as do most Tuesdays).

[Nehal Patel]

Tuesdays before 2:30 are hard for me. Fridays work well

[Rob Simmons]

I can't do Tuesday — does Zulip have polls? Let's try reaction poll for this week, :two: for Tuesday the 11th works for you, :four: if Thursday the 13th works for you, :fries: if Friday the 14th works for you, all noon at Mamelah's for simplicity.

[Kevin Buzzard]

Go with your reaction poll this time but just to let you know that Zulip does have polls:

Screenshot from 2025-11-10 13-13-09.png

[Johan Commelin]

Reminds me of https://en.wikipedia.org/wiki/Doomsday_rule#Mnemonic_weekday_names

[Jason Rute]

It looks like Thursday won (by a narrow margin). I didn't vote for it (I nominally have a meeting then), but I'll see if I can still make it regardless.

[Cameron Freer]

Sounds good -- have a nice meetup, and hope to catch you all next time!

[Jason Rute]

@Cameron Freer you mentioned you knew a few local people who might be interested. If you haven't already, can you let them know?

[Cameron Freer]

Yep -- I mentioned it already to a few of them and will also tell a few others (though I think this week may not be great for most of them).

[Weiyi Wang]

Hi all, I didn't notice this channel till today, and it looks like there is a meet up soon? I am also in Boston area. Is it at Mamaleh's at noon? I might drop by

[Cody Roux]

I don't have it in me to shlep out there, sorry. Next time!

[Jason Rute]

Sorry. I just have too many meetings today (more than usual for Thursday), so I can't make it. I'll try next time.

[Rob Simmons]

Not a problem (never a problem truly!) we’ve got some folks at a table in the corner

[Cody Roux]

Rob Simmons said:

Not a problem (never a problem truly!) we’ve got some folks at a table in the corner

I love that country song!

[Mako Bates]

Bumping this local! I'm actually up in Portland, ME, but excuses to take the train down are nice :)

[Michael Fishman]

I’m down to meet again in January!