New York City, USA

Stream: Geographic locality

[Jalex Stark]

I'm in NYC and would be happy to meet with anyone for pair-programming type sessions (with the aspiration of eventually having something like the ICL Xena group meetings or the Cambridge group meetings)

[Luis O'Shea]

I too am in NYC and would be happy to meet up to discuss Lean (or related topics, e.g. "The Little Typer" and Pie).

[Jalex Stark]

There is a private NYC stream, and either posting here or sending me a PM is a good way to get added to it.

[Julian Berman]

Jalex Stark said:

There is a private NYC stream, and either posting here or sending me a PM is a good way to get added to it.

@Jalex Stark Hey! (Also from NYC and super new). Would love to get added to this.

[Yakov Pechersky]

Same, also I'm NYC

[Julian Berman]

@Yakov Pechersky ah cool, hi!

[Jalex Stark]

both added

[Benjamin Davidson]

Just discovered this stream. I'm also in NYC!

[J. O.]

hello. im from new york as well

[Matej Penciak]

I just moved to NYC from Boston! Looking forward to meeting other Lean enthusiasts!

[Dean Young]

Hi! I'm Dean and I'm a grad student at NYU, with an interest in category theory, algebraic geometry, and number theory.

[Ruchir Khaitan]

Hi I'm Ruchir I just started learning Lean and living in Brooklyn. Excited to meet local lean folks

[David Renshaw]

I'll be in NYC (staying Long Island City) next week, Monday the 9th through Wednesday the 11th, and potentially available for meeting up with local Lean enthusiasts. Would anyone be interested? (if so, please DM me, to keep noise down on the public stream here)

[Carter Schonwald]

i'm in nyc

[Carter Schonwald]

Who’s in nyc these days ?

[Julian Berman]

Considering we just randomly met in the dog park, the number is at least the two of us :D

[Enrico Borba]

I'm out here until Feb/March or so

[Julian Berman]

If anyone else in the area is up for it, perhaps it's around the time to arrange some informal meetup. Maybe speak up if so and we can decide on a coffee shop, university and/or living room for some Lean.

[Matej Penciak]

That sounds fun! I'd be down to join

[Jonatas Miguel]

Ahoy all, I'm also in the NYC area. I'd be interesting in meeting up with other peeps, provided they're ok with a complete amateur joining up.

[Timo Carlin-Burns]

I'm in NYC now too and would love to meet other enthusiasts!

[Timo Carlin-Burns]

@Jalex Stark is there still a private NYC stream? I would love to get added

[Julian Berman]

There is though it's even less active than this thread :D, and probably can be public at this point, I think it was private for hysterical raisins.

[Julian Berman]

For what it's worth I tend to work from cafes lots of mornings, and occasionally do random Lean things when I get a moment. If anyone's near LES that's maybe a cheap way to meet up on an ad hoc basis.

[Julian Berman]

Otherwise I'm also around this week most days personally, so if others are perhaps we coordinate something for the next few days.

[Timo Carlin-Burns]

I moved to the upper west side recently and have not yet settled on a cafe to work from, so I would be totally down to try hanging out at one of your go-to cafes!

[Dean Young]

I am also in NYC. I think meeting is a great idea... what do people think of Veselka?

[Dean Young]

https://veselka.com/

[Jonatas Miguel]

I'd be down to meet in person, starting next week works best for me. I've never been to veselka, I'd be interested in trying it out.

[Matej Penciak]

I'd love to join as well! I live in Manhattan so Veselka or most other places are easy for me to get to.

I'm traveling for a conference in the first half of April, so I might not be able to make it to the first meetup... I'll be back after April 17, but certainly don't delay on my behalf!

[Timo Carlin-Burns]

I'm happy to meet anywhere! My schedule's very flexible

[Julian Berman]

Timo Carlin-Burns said:

I moved to the upper west side recently and have not yet settled on a cafe to work from, so I would be totally down to try hanging out at one of your go-to cafes!

On days when I bring my dog with me you can find me at Boris and Horton which is most weekday mornings. I'll be there Monday morning I'm sure, 10ish to 1ish. Other days I go to Stumptown in the Ace hotel. And yeah Veselka is also cute, happy to head there as well.

[Matt Diamond]

I'm in Greenwich Village, would be down to meet up as well... not a mathematician, though, just a lowly software engineer :smile:

[Timo Carlin-Burns]

Don't worry I'm not really a mathematician either :)

[Timo Carlin-Burns]

@Julian Berman I'm free in the mornings starting Wednesday. Want to plan to both work at Boris and Horton Wednesday morning? (And no worries if we end up cancelling or postponing)

[Julian Berman]

Sounds like a plan!

[Jonatas Miguel]

@Matt Diamond @Timo Carlin-Burns same here on not considering myself a mathematician

[Patrick Massot]

There is nothing wrong with not being a mathematician!

[Jonatas Miguel]

Hah, was not trying to imply that there was something wrong with not being one, just wanted to make sure certain expectations were not going to be set up about my level of experience. :D

[Dean Young]

@Matej Penciak @Jonatas Miguel @Timo Carlin-Burns @Julian Berman @Matt Diamond @Patrick Massot I missed this Wednesday meetup, hope it was a good one. What do you all think of this Wednesday at 11am? We could meet at Veselka.

[Julian Berman]

I've been overseas the past month but I actually will likely be back in NYC this week and the following, assuming they don't cancel my flight again tomorrow. Should be around and available.

[Timo Carlin-Burns]

I can do Wednesday at 11 at Veselka! Thanks for moving this forward

[Timo Carlin-Burns]

@Dean Young @Julian Berman does tomorrow at 11 still work? @Matej Penciak @Jonatas Miguel @Matt Diamond want to join?

[Matt Diamond]

appreciate the invite... unfortunately I'm busy with work during weekdays so I can't join you then, but I'm free most evenings/weekends

[Julian Berman]

@Timo Carlin-Burns Does for me!

[Timo Carlin-Burns]

Since Wednesday at 11 was just the first time Dean threw out, I'm guessing nobody's very attached to it. I think doing an evening or a weekend makes sense because I imagine Matt's not the only person who works during the day.

[Timo Carlin-Burns]

How's this Sunday (may 5th) for people? I don't have any plans yet

[Timo Carlin-Burns]

Also, Dean, are you imagining we'll be using laptops at Veselka's or just eating and getting to know each other? Another thing we could try is meeting somewhere, pulling out computers, and doing a bit of a show and tell with Lean stuff we're playing with

[Timo Carlin-Burns]

Dean, Julian, and I ended up deciding to push back today's meetup at 11. Let's see if we can make this happen soon though. Please each let me know how this coming Sunday works for you

[Julian Berman]

Should work for me!

[Dean Young]

I like the idea of an evening, the fifth is great. I'll bring my computer and I think show-and-tell is a great idea. Sorry for any confusion. So, we might want to switch the location to make sure we can pull out our computers. Timo, didn't you have a place that worked before?

[Dean Young]

At the meeting, I'd like to share the details of a recent PR I made with Jiazhen Xia. It's about extending a function from a jar shape to a cylinder shape. Our next PR will complete a proof of the Whitehead theorem, which divides into HEP (homotopy extension) and REP (CW-replacement). Here's a picture:

proj.png

[Timo Carlin-Burns]

Julian and I met at Boris and Horton before which is a dog cafe (he brought his dog). It's actually only a few blocks from Veselka if we wanted to meet there for show and tell and eat at Veselka after. I don't know the area well so I'm happy to meet anywhere. I think any cafe would do nicely

[Timo Carlin-Burns]

@Matej Penciak @Jonatas Miguel @Matt Diamond are you available to meet up some time on Sunday?

[Matej Penciak]

Timo Carlin-Burns said:

Matej Penciak Jonatas Miguel Matt Diamond are you available to meet up some time on Sunday?

Unfortunately I'll be traveling this Sunday, but in general I should be able to make most Sundays!

[Dean Young]

@Julian Berman

[Timo Carlin-Burns]

(I didn't ping Julian there because he already said yes to Sunday)

[Austin Letson]

Hi! I don't have anything specific to show and tell on Sunday, but I would like to come and meet others interested in Lean!

[Julian Berman]

For what it's worth Boris and Horton gets packed on Sunday (on the weekend in general). Not saying we shouldn't go there.. well I'm kind of saying that, they don't allow laptops after 10AM on the weekends and yeah it's a mad house from what I hear (I never go on the weekend). And by the way, big secret, don't tell anyone but I'll be there this morning in case anyone cares to drop in. But for Sunday if that neighborhood is good for folks... I'll try to think of some other place perhaps?

[Julian Berman]

Depending on how sunny it is just heading to Thomkins Square park might not be a bad one, there are a bunch of different places around for donuts or coffee or whatever to pick on, and we can just pick a corner in the park.

[Jonatas Miguel]

I should be available to meet up on Sunday. Just need a definite time and place.

[Jonatas Miguel]

We could all meet at Boris and Horton or Veselka and if we find it's too busy, move to another location nearby. I feel like just getting together can help us start to get the ball rolling on further meetups.

[Dean Young]

Let's all meet at Vesekla, that way we can figure out what place to pull out computers once we're there. Should I make reservations for 6pm?

[Timo Carlin-Burns]

Works for me!

[Matt Diamond]

Veselka this Sunday at 6 PM? That's not too far from me... I'll try to make it!

[Austin Letson]

6 PM at Veselka works for me!

[Austin Letson]

Unfortunately I am unable to come this evening. I will see you all at the next one!

[Timo Carlin-Burns]

Jonatas and I are in line. Looks pretty packed. @Dean Young @Julian Berman

[Julian Berman]

Just getting here. Sounds like Veselka :)

[Timo Carlin-Burns]

That was fun and it was great to get to know you both! I'm glad we finally made the meetup happen :smiley:

[Matt Diamond]

Sorry to have missed it! Perhaps I'll make it to the next one :)

[Jonatas Miguel]

So, the question about frequency of the meetup came up and we weren't sure if weekly, bi-weekly, or monthly was the ideal. What's everyone's thoughts on this? I'll start a poll in the next message to this thread.

[Jonatas Miguel]

/poll What should the cadence of our meetings be?
Weekly
Bi-Weekly
Monthly
Other (reply to poll with other option)

[Dean Young]

@Jonatas Miguel @Timo Carlin-Burns @Julian Berman @Austin Letson

Seems like we're pretty close to fifty-fifty on the cadence, but we could also average at tri-weekly.

Meanwhile it's been little while since the 5th so maybe we can schedule our next meetup. The tri-weekly pace would make for the 26th (Sunday).

[Timo Carlin-Burns]

The 26th works for me!

[Austin Letson]

The 26th works for me too!

[Julian Berman]

I'm out of the states until July I'm afraid, but hope to catch y'all at a later one!

[Antoine Chambert-Loir]

Just to tell that I am here for two weeks, busy with math and some jazz concerts, but ready to meet friends.

[Dean Young]

Hi Antoine, it'd be great to meet you too. Does the 26th work for you? I think we can work around it if not.

[Jonatas Miguel]

The 26th works for me. What time are we thinking and where will we meet up this time?

[Dean Young]

How is Lady Bird at 1pm?

[Timo Carlin-Burns]

Any time on the 26th works for me. Can I counter-propose Chelsea Market? It's a food court with a bunch of really yummy options and I like the idea of a more casual setting. I think it's also a shorter trip for most of us

[Dean Young]

Oh wow that's great. I went ahead and made this thing-

https://docs.google.com/spreadsheets/d/1jacOALD5CfVLAVZlSXL5C6bwsczrR465b3Y4c5wRUxc/edit#gid=0

[Austin Letson]

Chelsea Market at 1pm works for me!

[Jonatas Miguel]

Chelsea Market at 1pm works for me as well.

[Antoine Chambert-Loir]

Cool, I tag this on the agenda!

[Dean Young]

At that link, I made a section for events in case people want to paste a link or noticed something interesting.

[Matej Penciak]

I'm sorry I can't make it again (traveling again...) I definitely will try to make it to the next one, but the 26th unfortunately won't work for me.

[Dean Young]

Hey guys. Something has come up and I can't make it at 1pm. Could one of you at the meetup send me a message if you're still going at 3pm? I'd still love to come but have to be late :-(

[Austin Letson]

Will do @Dean Young

[Austin Letson]

Where in Chelsea Market should we meet?

[Timo Carlin-Burns]

I've only been to Chelsea market once before so I don't know the landmarks. I think I'll be entering at 9th Ave and 15th st

[Austin Letson]

I believe I will enter at the same corner. Want to meet at that corner?

[Timo Carlin-Burns]

Sure!

[Jonatas Miguel]

I'm currently outside of Sarabeth's Bakery

[Antoine Chambert-Loir]

I will leave my apt (in the village) in a few minutes to join you.

[Timo Carlin-Burns]

I'm gonna head inside and look for jonatas

[Austin Letson]

Sounds good. I am running a few minutes late. Will you let me know where you are sitting?

[Timo Carlin-Burns]

Right now jonatas is sitting at sarabeths bakery. I'm grabbing some food at takumi Taco

[Jonatas Miguel]

Some seats next to me opened up, I am going to hold onto them as best as I can.

[Austin Letson]

I am coming outside to sarabeths bakery right now

[Jonatas Miguel]

I'm sitting at the glass table with some kind of old motor looking thing serving as the table base. I can see Eat Offbeat right in front of me.

[Norman Paskus]

Where did you guys settle?

[Norman Paskus]

Sorry it’s Dean

[Austin Letson]

Nice to meet you all! I look forward to the next meetup @Antoine Chambert-Loir Safe travels!

[Austin Letson]

Sorry @Dean Young I had already left by 3

[Timo Carlin-Burns]

Likewise! I had a lot of fun getting to know you all and getting to geek out on some specific math

[Jonatas Miguel]

I had a great time meeting you all! I really appreciated all of the topics that we were able to touch on in our discussions! I hope to see all of you again sometime in any of our future in person sessions! Or online if anyone decides to start up a more worldwide recurring Lean meetup session via zoom.

[Jonatas Miguel]

@Antoine Chambert-Loir safe travels!

[Jonatas Miguel]

Thanks again @Antoine Chambert-Loir, @Timo Carlin-Burns, and @Dean Young for the in person problem solving sessions!

[Dean Young]

It was great meeting you all. Talking over these tutorial puzzles was great.

[Jonatas Miguel]

So, it's about that time again folks! Is anyone interested in meeting up this Sunday the 9th of June, around 1pm?

How would we feel about doing it at Chelsea Market again?

[Dean Young]

That sounds good to me.

[Austin Letson]

I will be out of town, but I hope to join at the next one!

[Timo Carlin-Burns]

I'm now living a bit farther away from the city but there's a chance I decide to make the trek and come Sunday!

[Matej Penciak]

I think I'll finally be in town for it this Sunday, so count me in!

[Jonatas Miguel]

Hey all, I'll be waiting at the glass table right outside of Sarabeth's Bakery.

[Dean Young]

I'm going to be a little late, like 1 : 20

[Dean Young]

@Matej Penciak @Jonatas Miguel sorry... it looks like I can't make it this time. Hope it goes well

[Jonatas Miguel]

@Dean Young we'll be looking forward to the next time you come out! @Matej Penciak it was fun hanging out!

[Matej Penciak]

Jonatas Miguel said:

Dean Young we'll be looking forward to the next time you come out! Matej Penciak it was fun hanging out!

I had a great time at the meetup! I don't know if I'll be able to join next time, but if I'll try to show up whenever I get the chance.

[Julian Berman]

A selfish idea -- perhaps it would be a nice idea for future meetup(s) if one of us came with some short(ish) paper we could try hacking on / formalizing together -- I'm sure it would mean being quite patient teaching some of us the math bits and dividing up the work but might be a nice way to do something productive + interesting.

[Yakov Pechersky]

I've been working on https://www.sciencedirect.com/science/article/pii/S0747717113001193?via%3Dihub

[Yakov Pechersky]

Which comes from https://pallini.di.uniroma1.it/

[Yakov Pechersky]

Trying to figure out if I can implement their algorithm in lean, show that it is as fast as their binary, and also prove it correct. And build out graph algorithm lib

[Yakov Pechersky]

Not sure when I'll be able to come to the next meetup, but hope to one day!

[Austin Letson]

Julian Berman said:

A selfish idea -- perhaps it would be a nice idea for future meetup(s) if one of us came with some short(ish) paper we could try hacking on / formalizing together -- I'm sure it would mean being quite patient teaching some of us the math bits and dividing up the work but might be a nice way to do something productive + interesting.

I like this idea a lot!

[Julian Berman]

I've been working on https://www.sciencedirect.com/science/article/pii/S0747717113001193?via%3Dihub

Very nice! Yeah I'm back myself now so same here, looking forward to one.

[Austin Letson]

The Carleson project is another idea of something we could hack on.

[Austin Letson]

It is advertised in that thread as a relatively accessible project due to the blueprint and combinatorial flavor.

[Austin Letson]

Yakov Pechersky said:

Trying to figure out if I can implement their algorithm in lean, show that it is as fast as their binary, and also prove it correct. And build out graph algorithm lib

Thanks for sharing. This is an interesting project. Do you have a GitHub repo where you are working on this?

[Yakov Pechersky]

I have a mathlib branch for this, not sure if pushed. I'm on parental leave at the moment, and as such, haven't had much keyboard time

[Jonatas Miguel]

Ahoy all,

I'm not going to make it to NYC today, but if anyone is thinking of meeting up, remember we've been getting together at the Chelsea Market around 1PM.

[Austin Letson]

I can't make it today because I am out of town. In the future, would others be interested in meeting somewhere quieter than Chelsea Market? What was the noise level of Veselka during the first time you all met this spring?

[Jonatas Miguel]

We never made it inside because it was packed that time we tried to meet up there.

If we are thinking of looking for a new place, I think we need to make sure we choose a place where we can open up our laptops and lounge around for a while.

Do you all think any local university would be willing to open up some space for a group like this?

[Noah Stebbins]

Hey guys, I live in NYC too. Nice to meet you :wave:

When & where is the next meetup? I'd love to join.

[Julian Berman]

I've got access to Baruch and Columbia but not sure how many people I can get in.

[Julian Berman]

I also likely don't mind offering up my apartment to be honest, long as we're say 3-5 people.

[Julian Berman]

Any more and I won't have enough chairs :)

[Julian Berman]

When & where is the next meetup? I'd love to join.

I don't think we've got one planned just yet, perhaps next week though is a good target? Are folks around?

[Jonatas Miguel]

Hello @Noah Stebbins, we usually meet every two weeks. We've been meeting up at the Chelsea Market at 1PM.

Today is one of the meet up days, but I'd hold off from heading over there until someone else says they'll be going, otherwise you risk being the only one there.

[Noah Stebbins]

Thanks @Jonatas Miguel for the info. :thumbs_up:

I'd be happy to host you guys at my place. I've got a lounge in my apartment building that I can reserve for free that has plenty of seating space & WiFi. I live on 28th St between 10th & 11th Av. Lmk if you guys are interested & I can make a lounge reservation.

[Synergylab 003]

(deleted)

[Jonatas Miguel]

Hey all, not going to be able to make it out there today.

If anyone is interested in meeting up please coordinate through here.

[Austin Letson]

I really like Julian's idea of picking a paper we could try hacking together at the next meet up. Another similar option would be to choose one of the theorems tagged with proof_wanted in batteries to hack on together (link to GitHub filter). I think HashMap.insert_find? is the only one which doesn't have an open PR.

[Austin Letson]

Are folks around this weekend to hack on something together (July 13 or 14th)?

[Henrik Böving]

If you are interested in verifying HashMap stuff just a little remark: Since this Friday Lean core has a HashMap implementation that is a lot further than the batteries one in terms of verified operations: https://github.com/leanprover/lean4/tree/master/src/Std/Data

[Austin Letson]

Henrik Böving said:

If you are interested in verifying HashMap stuff just a little remark: Since this Friday Lean core has a HashMap implementation that is a lot further than the batteries one in terms of verified operations: https://github.com/leanprover/lean4/tree/master/src/Std/Data

Ah, thanks for calling this out Henrik. Is there an equivalent of proof_wanted for the data structures in Lean core?

[Henrik Böving]

Not to my knowledge no. I also don't know if the HashMap implementation is considered open for contribution at the moment (and if it is what kind of contributions). Maybe @Markus Himmel wants to comment on that.

[Austin Letson]

Got it. In that case, the proof_wanted route might be a dead end for NYC meetup topics.

[Julian Berman]

I'm around personally, either day!

[Austin Letson]

What about Saturday at 11am?

[Austin Letson]

I looked through the outstanding tasks for the Carleson project. I think we could take a stab at lemma 5.1.1. I am not knowledgeable in this area, but I understand that lemma enough to get started, and it would at least be a good learning experience! If others have ideas for other things we could hack on, feel free to throw them out!

[Julian Berman]

Works for me on both parts (the time and also looking at something in Carleson, though I haven't tried to understand the lemma yet)

[Julian Berman]

Though Saturday is somewhat "far off", maybe that will get checked off by then judging by how fast things move :)

[Julian Berman]

Ah nice I see you claimed it though, so good.

[Austin Letson]

Julian Berman said:

Works for me on both parts (the time and also looking at something in Carleson, though I haven't tried to understand the lemma yet)

Yay!

[Austin Letson]

Hi! Are other folks around this weekend and interested in joining me and Julian tomorrow morning at 11 to hack on Carleson or any other project you would like to work on together?

[Floris van Doorn]

Great if you end up working on the Carleson project. Lemma 5.1.1 that you claimed is really small. I also claimed Lemma 5.2.9 if you want to continue after that. That lemma should still be elementary. No worries if you don't get to it though!

[Austin Letson]

Floris van Doorn said:

Great if you end up working on the Carleson project. Lemma 5.1.1 that you claimed is really small. I also claimed Lemma 5.2.9 if you want to continue after that. That lemma should still be elementary. No worries if you don't get to it though!

I chose 5.1.1 in part because it was marked as very easy and I am not very familiar with the area. We will take a look at 5.2.9 as well. Thank you for the pointer!

[Austin Letson]

Good morning! Where should we meet today? I was thinking a quiet coffee shop or library

[Julian Berman]

Morning! Stumptown maybe in the Ace Hotel? There should be plenty of seats/tables in the lobby usually. That close to you? https://maps.app.goo.gl/VerLjuZQdm9oqiHo7

[Austin Letson]

Sumptown works for me. Does 11 still work?

[Julian Berman]

Perfect, yeah I'll convince myself to stop lounging by then :). See you in a bit.

[Austin Letson]

Sumptown works for me. Does 11 still work?

[Austin Letson]

Is anyone around this weekend to work on another lemma from Carleson. @Julian Berman and I figured out 5.1.1 on Saturday, but Floris said that 5.2.9 is likely also manageable! I am also open to working on something different if others have projects they want to bring. Potentially on Sunday?

[Julian Berman]

Email: ## Enjoy $2 off your next visit to Stumptown!

Clearly Stumpdown doing what they can to encourage Lean development.

[Austin Letson]

Sumptown and the Ace Hotel, unofficial sponsors of Lean NYC meetups :coffee:

[Matej Penciak]

Austin Letson said:

Is anyone around this weekend to work on another lemma from Carleson. Julian Berman and I figured out 5.1.1 on Saturday, but Floris said that 5.2.9 is likely also manageable! I am also open to working on something different if others have projects they want to bring. Potentially on Sunday?

I should be in town for this one!

[Austin Letson]

Should we meet at Sumptown at 11 on Sunday? @Julian Berman, would it be easier to meet closer to you to keep an eye on the puppy? @Matej Penciak, where are you located?

[Matej Penciak]

I live in upper manhattan, but I don't have too much going on Sunday so as long as it's not too far out I should be good

[Julian Berman]

Stumptown works again yeah, pup will be fine.

[Austin Letson]

Awesome!

[Austin Letson]

Good morning. My ETA at sumptown in the Ace hotel is 11:15. See you soon!

[Matej Penciak]

Sounds good! I'm waiting for a downtown A, but should be getting there around the same time.

[Austin Letson]

Just arrived at sumptown. Looks like there is plenty of space for us to sit

[Austin Letson]

It was great to get together @Matej Penciak and @Julian Berman

[Austin Letson]

4de174e7-275c-4ba6-afe9-1f9898500a85.jpg
I saw this walking to the train. Maybe it is trying to tell us something :eyes:

[Julian Berman]

I don't know about you two Austin/Matej but even though I gave 5.2.9 another half hour or so I didn't have any epiphanies for how to move on from where we got stuck

[Julian Berman]

Matej not sure if you feel stuck, but I would love to not give up on it though :) -- so (completely not NYC related) but maybe we can convince someone more experienced to screenshare with us and give us hints? Does that sound like something you'd (either of you) would be interested in -- if so probably we should figure out some time that works for us + whoever we can sucker into answering our question(s).

[Julian Berman]

For me at least a screenshare would be better than posting what we have, because I'm sure if we do someone would simply tell us answers, so I'd rather struggle a bit to even explain why we're stuck.

[Austin Letson]

@Julian Berman I love that idea!

[Austin Letson]

I also gave ~30 min with nothing more than renaming variables and moving things around.

[Austin Letson]

I was going to take another look tomorrow morning. If someone with more experience and context is willing to show us their thought process I would greatly appreciate it.

[Austin Letson]

We could also choose a specific sorry to ask about and see if that gives us some ideas for the rest of the proof.

[Yaël Dillies]

I don't really know the context yet (haven't had time to look at Carleson), but I should note that I am quite literally currently employed to help people out with Lean. If you feel like it, I am available all day in GMT+3

[Austin Letson]

Yaël Dillies said:

I don't really know the context yet (haven't had time to look at Carleson), but I should note that I am quite literally currently employed to help people out with Lean. If you feel like it, I am available all day in GMT+3

I am interested :hand: Thank you @Yaël Dillies! The next time that would work for me is Friday morning NYC time (GMT-4) which would be sometime after 2PM GMT+3. @Julian Berman and @Matej Penciak (if you are interested as well) what is your availability?

[Julian Berman]

Ooh. Yeah that does work for me too, though I may selfishly steal time earlier too given I'm free today.

[Austin Letson]

Sounds good. Let me know if you have an aha moment today

[Kevin Buzzard]

What goal are you stuck on?

[Yaël Dillies]

Julian and I are on a call right now, so hopefully things will be cleared up soon :smile:

[Julian Berman]

I had many small "a ha" moments, so thanks Yael! Not done yet but we hung up so I wasn't simply letting Yael tell me answers and could fight a bit to see if I can finish it off.

At the beginning where we were trying to figure out how to translate "Let I \mem L u" and we weren't understanding how we were allowed to break up the volume into some sum of sets, Yael pointed us to docs#MeasureTheory.measure_biUnion_le and docs#tsum_le_tsum and started showing me how to do this as a calc proof (and said it was a standard way to do this kind of argument) -- so, I'm not unhappy we didn't figure that out, it seems like a pattern one needs to know about how to do this kind of argument.

[Austin Letson]

Yay, thanks Yael! @Julian Berman do you have a branch where I could take a look at the progress you made?

[Austin Letson]

Is anyone around this weekend to meet up? I am down to continue to hack on Carleson.

Additionally, I am interested in making an attempt at a minimal lake tree. It may be a nice change of pace from proving theorems.

[Austin Letson]

I thought it would be a good candidate for collaboration since it would involve brainstorming about design/UX decisions, would be easy to divide and conquer, and wouldn't require mathematical context.

[Yaël Dillies]

If ever you need help from me, I should let you know that I'm giving a (in-person) workshop from 2024-08-01T14:00:00+03:00 to 2024-08-01T18:00:00+03:00. You can still ask questions but I might not be super reactive.

[Julian Berman]

I've been away/offline for a few days in Toronto (and will be away for a few more) so think I'm not making this one unfortunately @Austin Letson -- but definitely down for both or either idea in the next one.

[Austin Letson]

Julian Berman said:

I've been away/offline for a few days in Toronto (and will be away for a few more) so think I'm not making this one unfortunately Austin Letson -- but definitely down for both or either idea in the next one.

Enjoy Toronto Julian! See you at the next one.

[Julian Berman]

@Austin Letson shall we try again this weekend? I guess we have 2 (and I'll add a third) options --

• finish off (hopefully?) 5.2.9 and/or anything carleson in general
• lake tree
• pick a math textbook to go through, which I think is an even "easier" idea (if we're not already familiar with the material) than the paper one I originally threw out

Could do a little of all 3?

[Julian Berman]

Obviously that message / doing another applies equally to anyone else in the area!

[Austin Letson]

I am out of town this weekend. What about next weekend?

These options sound good to me. I like the idea of doing a little of each. Do you have a textbook in mind?

[Julian Berman]

Next weekend it is then.

[Julian Berman]

Do you have a textbook in mind?

I have a list of stuff I try to occasionally read and ultimately fail at reading, either because I get distracted, it's too hard, or I get stuck on something specific and can't convince myself to leave it alone. Every so often I try to go through Generatingfunctionology with or without Lean. Maybe that? https://www2.math.upenn.edu/~wilf/gfology2.pdf -- I feel like something that is reasonably short, and/or pretty accessible regardless of how much we know (which for myself isn't much) is most tempting.

[Julian Berman]

(Enjoy your own trip by the way!)

[Austin Letson]

Julian Berman said:

Do you have a textbook in mind?

I have a list of stuff I try to occasionally read and ultimately fail at reading, either because I get distracted, it's too hard, or I get stuck on something specific and can't convince myself to leave it alone. Every so often I try to go through Generatingfunctionology with or without Lean. Maybe that? https://www2.math.upenn.edu/~wilf/gfology2.pdf -- I feel like something that is reasonably short, and/or pretty accessible regardless of how much we know (which for myself isn't much) is most tempting.

I am interested in working through some of generatingfunctionology. The preface is intriguing.

[Austin Letson]

@Julian Berman could you send me the version of the 5.2.9 proof after your session with Yael so I could take a look at it before we take another stab?

[Julian Berman]

Sent!

[Chris Henson]

Austin Letson said:

I am interested in working through some of generatingfunctionology. The preface is intriguing.

I am in Philly, but if you'll be working on this I might make the short train ride up. I've played around with generating functions before (and skimmed that book) and would be curious to follow along with some more experienced Lean folks.

[Julian Berman]

That'd be great! If you do come up obviously just confirm you're coming, mostly so I can be sure to stay as long as you will and not just run off 3 hours into the meetup or whatever -- may as well take advantage of the time if you're going to make the journey!

[Kim Morrison]

Another really fun book, that has relatively low mathematical prerequisites, but would be amenable to formalisation (and if done completely really awesome!) is "A=B".

(An author in common.)

[Dean Young]

@Kim Morrison Do you have any books Kim?

[Julian Berman]

Nice! Thanks for the recc Kim, will have a look at that as well!

[Kim Morrison]

A=B is freely available online, btw.

[Austin Letson]

How does Saturday work for meeting up?
@Julian Berman @Chris Henson and anyone else in NYC who wants to work on Carleson, lake tree, and generatingfunctionology

[Julian Berman]

Good for me!

[Chris Henson]

I'll be able to make it too, looking forward to meeting you both!

[Austin Letson]

Chris Henson said:

I'll be able to make it too, looking forward to meeting you both!

Yay! Looking forward to meeting you as well Chris. What are your travel plans? I was going to suggest 11 at Stumptown Coffee, however I am flexible on Saturday. My only preference would be to meet during the day as opposed to the evening.

[Chris Henson]

11 would be good for me too, I'll be headed back to Philly that evening. Just to make sure, you mean the Stumptown on 29th, right?

[Austin Letson]

Yes, it is in the Ace Hotel

[Julian Berman]

Awesome see you both there/then!

[Noah Stebbins]

Hey guys, mind if I join too on Saturday? Full disclosure: I'm a bit of a Lean noob

[Austin Letson]

Of course @Noah Stebbins! The more the merrier

[Chris Henson]

Unfortunately my bus got just cancelled/overbooked, so I won't be able to make it today. (One company bought another, it's utter chaos lol). Hopefully I'll be able to make it up some other time!

[Austin Letson]

What bad luck :( Another time! Generatingfunctionology has enough material for many more meetups :)

[Julian Berman]

Oy, terrible luck yeah. We have an unofficial NYC Lean coffee sponsor, clearly we need a bus operator

[Noah Stebbins]

Running 5 minutes late. I'll see you guys soon!

[Austin Letson]

Are others interested in meeting up on Saturday?

[Austin Letson]

For Carleson (I have a good feeling about this week) and more generatingfunctionology?

[Julian Berman]

Yes here!

[Noah Stebbins]

I have a wedding this Saturday but I'll definitely catch the next one

[Ruben Van de Velde]

Congratulations?

[Austin Letson]

11 tomorrow at Sumptown? @Julian Berman and any one else who wants to join

[Julian Berman]

It's absurdly nice out -- @Austin Letson you up for maybe trying to do outside? Could go to Madison square Park which is still in this neighborhood?

[Julian Berman]

I've got a mobile hotspot if needed but there's also park wifi

[Julian Berman]

We could get coffee first and bring it there (just an idea obviously)

[Austin Letson]

Madison square Park sounds great! Given that we aren't reliant on Sumptown's seating, would you recommend a different coffee spot nearby?

[Austin Letson]

No disrespect to our unofficial sponsor

[Julian Berman]

There's Coppa -- https://maps.app.goo.gl/TsHtHytLsdHpa1nv8 -- for which my Google Maps note says "I had to nag the owner that charging more for a macchiato than for a cortado makes 0 sense -- he said they'd fix it". Possibly this says more about my ability to be annoying than the shop, but you probably knew that already from our previous 3 Lean meetups. (The coffee was OK to my recollection). So there?

[Austin Letson]

Sounds great! We obviously need to find out if they have straightened that pricing inconsistency out :coffee:

[Julian Berman]

Oh unironically absolutely.

[Johan Commelin]

Don't leave us in suspense... did they?

[Julian Berman]

They... Did not. Never again Coppa, never again :)

[Johan Commelin]

You seem to have an unofficial NYC Lean coffee sponsor, now it seems you can also have an official anti-sponsor :wink:

[Austin Letson]

Do others want to meet this weekend? If it is nice, I would like to meet outside again. Maybe we could meet your pup @Julian Berman ?

[Julian Berman]

Yes! Sounds good to me

[Matej Penciak]

I should finally be back in town this weekend as well, so count me in!

[Julian Berman]

Good good, we need to compete with that San Francisco thread.

[Kevin Buzzard]

I'll be in New York and free 8th to 11th September (also 12th and 13th but busy working, and leaving 1st thing on 14th).

[Julian Berman]

I'm likely free all of those days at this point besides the evening of the 10th -- probably others would be good to share when works for you all so we can take advantage of having Kevin in town!

[Julian Berman]

Here's a Doodle even, maybe that's easier: https://doodle.com/meeting/participate/id/eEGxVrmb

[Kevin Buzzard]

Just to clarify -- I'm arriving at midnight on 7th so any time on 8th is basically OK

[Julian Berman]

1AM meetup at JFK.

[Eric Paul]

I'm in NY this weekend and wondering if I could join you guys!

[Julian Berman]

Yes please do!

[Eric Paul]

Great, do we know where and when the meeting is?

[Julian Berman]

Usually we meet at 11 -- last week it was at Madison Square Park, with a stop for coffee first and then walked over to the park -- I suspect we'll probably do the same, though with a different coffee stop :D -- @Austin Letson + @Matej Penciak (+ you Eric) do you want to maybe meet at https://maps.app.goo.gl/YhiAruLHmnwcEggQ6 perhaps?

[Julian Berman]

(And for any late stragglers we'd probably be at the park by 11:20-11:30)

[Austin Letson]

11 at Copper Mug works for me. Are we meeting on Saturday?

[Julian Berman]

Saturday yeah!

[Austin Letson]

Sounds great. I am excited to meet the dog :puppy:

[Julian Berman]

I'm sure so is she... For at least an hour :D

[Julian Berman]

(which will be good, I'll drop her home whenever she gets restless and then come back)

[Austin Letson]

Maybe she can help us with 5.2.9

[Julian Berman]

I can guarantee she can help turn 529 pigeons into 5.2.9 of them

[Noah Stebbins]

Cool I'll join in tomorrow too :thumbs_up:

[Julian Berman]

NYC representing.
PXL_20240831_170824098.RAW-01.MP.COVER.jpg

[Julian Berman]

If anyone's wondering why there's only one laptop open, we are just all that good at Lean.

[Dean Young]

Wow what a nice time

[Austin Letson]

I can meet any time on Sunday. What works for others?

@Kevin Buzzard we usually meet at 11am. Would that work for you on Sunday?

[Kevin Buzzard]

Sunday 8th at 11am sounds great to me! Let me know the coordinates and I'll attempt to be there!

[Yakov Pechersky]

I'd love to join but this Sunday I have a family thing. And Saturdays never work for me...

[Julian Berman]

Should do a second one later in the week then, when works Yakov?

[Austin Letson]

Kevin Buzzard said:

Sunday 8th at 11am sounds great to me! Let me know the coordinates and I'll attempt to be there!

Sumptown Coffee @ 40.7457949, -73.9881841 is the go to spot. Looking forward to seeing everyone!

[Kristoffer Josefsson]

Hi, long time listener first time caller here. I’ll come to the meetup this morning, looking forward to meeting everyone, hopefully there’s enough space.

[Austin Letson]

Kristoffer Josefsson said:

Hi, long time listener first time caller here. I’ll come to the meetup this morning, looking forward to meeting everyone, hopefully there’s enough space.

Yay! See you soon

[Austin Letson]

Great to meet you @Kristoffer Josefsson

[Austin Letson]

Good luck with the rest of your visit to NYC @Kevin Buzzard!

[Kristoffer Josefsson]

Thanks for organizing - I made the ferry with little margin.

[Julian Berman]

Anyone around to meet up again tomorrow? @Austin Letson ?

[Austin Letson]

I am down. Could you meet at 1 tomorrow? Weather forecast looks nice :sun_face: :puppy:

[Julian Berman]

Let's do it.

[Matej Penciak]

I can't make it this week, have a good time!

[Austin Letson]

@Julian Berman where should we meet? Is Ellie joining us?

[Julian Berman]

Yeah I'll bring her. MSQ Park again? Nice out seems like.

[Austin Letson]

Sounds good. See you soon

[Julian Berman]

If you want to grab coffee somewhere we can meet somewhere around the park again too -- I have some cold brew I made in the fridge so I probably will just go with that

[Julian Berman]

Heck I can bring some extra too.

[Austin Letson]

Julian Berman said:

Heck I can bring some extra too.

Thank you for the offer! I am good with no coffee. I have had a few cups this morning already

[Austin Letson]

Are you at the park yet? I am looking for some shade

[Julian Berman]

Just got here, we're considering joining the parade

[Austin Letson]

When is the parade?

[Austin Letson]

I found a table by the shake shack

[Austin Letson]

Shaded by buildings

[Julian Berman]

Who's in for Sunday this week?

[Aaron Hill]

I'm interested - this will be my first time attending

[Austin Letson]

I would love to, but I am moving this weekend so I can't make it. I will be closer to our meet up spot for the next one though!

[Julian Berman]

Good luck with the move!

[Julian Berman]

Aaron (and/or anyone else) let me know if you still care to meet up tomorrow, I should be around.

[Aaron Hill]

What time are you planning on?

[Julian Berman]

Does somewhere around noon work in Madison Square Park area?

[Aaron Hill]

Would 12:30 work for you?

[Julian Berman]

Yep!

[Julian Berman]

See you in 10 yeah?

[Aaron Hill]

I'm on a bench with a backpack, near the pond

[Julian Berman]

There in 2

[Austin Letson]

Are others around this Sunday to meet up?

[Julian Berman]

Yep yep for me!

[Aaron Hill]

I'm available

[Jonatas Miguel]

Ahoy! It's been a while since I've joined an in person session. I'll be available this weekend, looking forward to joining you all again.

[Austin Letson]

How does 11:30 Sunday around Madison Square Park work for others?

[Kristoffer Josefsson]

I’ll be there as well! Looking forward.

[Julian Berman]

Wow, up to 5 then hopefully! Proving New York doesn't just turn up for Kevin :D

[Austin Letson]

Should we meet at Sumptown?

[Julian Berman]

Considering the mist, yeah think so.

[Austin Letson]

:thumbs_up: I will be at sumptown around 11:40

[Jonatas Miguel]

That's the stumptown on 29th right?

[Julian Berman]

Yes! https://maps.app.goo.gl/ccPAqv2Jj6RucX3KA This one.

[Aaron Hill]

I'm inside at the couch by the long table

[Jonatas Miguel]

Going to arrive a bit late, I was only about to catch the bus now

[Austin Letson]

Great to see everyone! My legs got a good workout standing haha. Hopefully next week we can resume our outdoor series :sunny:

[Julian Berman]

Yes! Same here!

[Aaron Hill]

What was the github repo for the generating functions stuff?

[Julian Berman]

https://github.com/Julian/generatingfunctionology.lean/tree/second-recurrence

[Austin Letson]

Are others around on Saturday to meet up?

[Jonatas Miguel]

I'll try to make it out there again.

[Julian Berman]

(Ah I actually forgot I'm away this weekend as well, so I'll miss this week. See y'all next one...)

[Austin Letson]

We will miss you @Julian Berman!

[Austin Letson]

@Jonatas Miguel @Aaron Hill what do you think of meeting outside if the weather is nice?

[Austin Letson]

The weather looks nice :sunglasses:

[Austin Letson]

How do others feel about 1pm in Madison Square Park?

[Jonatas Miguel]

@Austin Letson apologies, I thought we were meeting on Sunday, I'm not going to be able to meet up today as I'm visiting my brother.

[Jonatas Miguel]

Sorry for the confusion :(

[Jonatas Miguel]

I'll see you all next time for sure.

[Austin Letson]

Jonatas Miguel said:

Austin Letson apologies, I thought we were meeting on Sunday, I'm not going to be able to meet up today as I'm visiting my brother.

No worries. See you next time!

[Austin Letson]

@Aaron Hill I am getting the ferry across now. Should be to Madison Square Park at 1

[Aaron Hill]

I'm close by, but I'm trying to get around the parade

[Austin Letson]

I can hear the parade but I don't see it yet

[Austin Letson]

I just entered the north east corner of the park

[Austin Letson]

I am walking over to the seating area near shake shack

[Austin Letson]

I found a table near shake shack

[Aaron Hill]

I'm here

[Austin Letson]

Are others around this weekend to meet up?

[Kristoffer Josefsson]

I’m out of town again unfortunately

[Austin Letson]

@Julian Berman and @Aaron Hill Does Sunday work for you?

[Austin Letson]

See you another time @Kristoffer Josefsson! Enjoy your trip

[Julian Berman]

Yep good for me!

[Aaron Hill]

I'd prefer saturday if possible, but sunday works as well

[Jonatas Miguel]

Either day works for me this week

[Matej Penciak]

I'm still out of town unfortunately (but I am having a great time in Portugal @Jonatas Miguel!!)

[Jonatas Miguel]

Nice! Where'd you end up in Portugal?

[Austin Letson]

Either Saturday or Sunday works for me

[Austin Letson]

@Julian Berman does tomorrow work for you?

[Julian Berman]

Yeah should be ok

[Austin Letson]

The weather looks like we may be able to sneak in another outdoor meetup before it gets cold

[Austin Letson]

How is Madison Square Park at 12 tomorrow?

[Austin Letson]

Based on ferry timing, I am going to get there at 12:20

[Austin Letson]

I found a table near shake shack

[Jonatas Miguel]

I'm close by, heading your way now

[Austin Letson]

Are others around on Saturday to meet up?

[Austin Letson]

I am interested in trying out ImProver this weekend. That is something we could look into if others are interested

[Julian Berman]

I can't make Saturday this week. Could do Sunday if you're around then or otherwise will see you next week!

[Aaron Hill]

Sunday would work for me

[Alex Nguyen]

I'd love to join if that's ok. I'm taking the train from Princeton so the afternoon would be better for me since it takes 2 hours by train !

[Austin Letson]

Sunday works for me too. How about 1pm?

[Matej Penciak]

I should be able to make it this week!

[Thomas Zhu]

I am at CMU working with ImProver authors for potentially its next steps (I did not work on ImProver itself). I am currently in NYC over the weekend, and would like to discuss/know what people think about it, or any other Lean topic!

[Austin Letson]

Hi Thomas :wave: You are welcome to join! We usually meet around Madison Square Park

[Julian Berman]

Do we want to attempt the park again or just say we meet at Stumptown?

And hopefully those of you coming from out of town know where to head? If not let us know. Looking forward to meeting you both.

[Austin Letson]

I think the weather is nice enough for the park :sunglasses:

[Julian Berman]

Good deal, sounds good, see you there.

[Matej Penciak]

I'm running late, but I'm on my way now!

[Thomas Zhu]

I will be ~10 minutes late

[Austin Letson]

I found a table near shake shack

[Austin Letson]

Near the south west entrance to the park

[Julian Berman]

There in 3.

[Thomas Zhu]

Sorry I don't know what you guys look like. I have arrived and I'm in a CMU hoodie

[Austin Letson]

Are others around on Sunday to meet up?

[Julian Berman]

Yep yep, good for another here.

[Jeremy Avigad]

I will give a talk, "You Want Proof? I'll Give You Proof! Mathematical Arguments from Euclid to Lean," at the National Museum of Mathematics (MoMath) on November 6. It will be a quick tour of mathematical proof from Euclid to the present day, with a brief Lean demo at the end.

I was asked to provide a 25-minute activity after the lecture. Ipads will be available, and I will invite participants to choose between two activities: doing geometric constructions with Euclidea or playing the Natural Number Game.

I will give the lecture twice, once at 4 pm and once at 7 pm. Having a few Lean friends on hand would be great to help participants with the activities. @Alex Kontorovich will introduce me, @Hannah Fechtner will come to New York to help, and @Julian Berman will come to at least one of the lectures. If you can join the fun, please register and let me know.

[Austin Letson]

My girlfriend and I just registered for the 7 pm talk. We are looking forward to it!

[Austin Letson]

@Julian Berman and @Aaron Hill are you still down to meet up today?

[Julian Berman]

@Austin Letson I had a friend come into town who I'm gonna meet for lunch around 1. I would still come for an hour or two if you want to do earlier (like 11 till 1, or whatever works for you) if it's worthwhile. Or obviously if @Aaron Hill is around and will stay the whole time.

[Austin Letson]

Unfortunately, I can't make it to the Madison Square Park area until around 1.

[Julian Berman]

OK all good -- yeah I also could do when I'm back if you want to do more like 5 (especially if you care to do it at my place so I can keep an eye on Ellie and her lil' cone head), or otherwise might be a week to skip unless Aaron says he's around.

[Aaron Hill]

I'm available for the rest of the day

[Julian Berman]

Nice! Well if the two of you end up meeting up I'll join after then.

[Austin Letson]

@Aaron Hill want to meet at Sumptown at 1?

[Austin Letson]

@Julian Berman how long does Ellie have her little cone for? :heart:

[Austin Letson]

Does she try to get out of it?

[Julian Berman]

The guidelines say 10 days, so another 8 it seems. She's starting to learn how to move with it on (it's day 3 after the surgery). The "worrying" bit for leaving her alone for long periods is that she wasn't previously even happy to get off the couch (which she owns), so she won't go get herself food or water or whatever. But she looks like she's getting a bit more confident and turning back into a feisty puppy now that she's probably a bit less groggy. So... positive progress it seems. And yes that also includes her now figuring out she can try to get out of it. I swear she is smarter than I am. But I've now fastened the cone on her with her collar (instead of just gauze), so the ball is back in her court for proving whether she can still wiggle.

[Aaron Hill]

I'm running a little late

[Austin Letson]

Aaron Hill said:

I'm running a little late

Perfect, me too haha

[Austin Letson]

I got a seat at one of the high tables

[Aaron Hill]

Anyone available tomorrow?

[Austin Letson]

I am watching the marathon tomorrow, but I am down for next weekend

[Julian Berman]

I'm also tied up this weekend but hopefully see you at Jeremy's talk? And/or next weekend

[Julian Berman]

Nice to see (some of) y'all yesterday. What we thinking for the weekend, anyone have prefs on Saturday vs. Sunday this time around?

[Austin Letson]

Yes, so fun to see you all at a Lean event. Saturday works best for me this weekend.

[Aaron Hill]

That works for me

[Julian Berman]

Sounds like a plan then

[Matej Penciak]

Sounds good to me as well!

[Bo Qin]

:+1:

[Austin Letson]

Does 1 at Sumptown work for others?

[Julian Berman]

@Bo Qin hopefully you'll come join us! Just in case, that's https://maps.app.goo.gl/mbzS7kYUjEYBbiXF8

[Aaron Hill]

Anyone around tomorrow?

[Julian Berman]

Today was a wash, but tomorrow I should be yeah!

[Austin Letson]

I am not free until around 2:30. I can join late if you all are meeting earlier

[Austin Letson]

I have one sorry left on Carleson 5.2.9 that I think one of you might know how to dispatch quickly.

[Julian Berman]

Ooh nice, ok. Yeah let's slay the beast.

I'm waiting for a groceries delivery which was supposed to be now but seems delayed to early afternoon. @Aaron Hill what's your timing look like? Should we just plan for 3?

[Aaron Hill]

That works for me

[Austin Letson]

Are we meeting at Sumptown?

[Austin Letson]

I am going to be a few minutes late

[Julian Berman]

Yeah! Should be there in 15 myself.

[Austin Letson]

I will be there at 3:20

[Austin Letson]

Are others around this weekend to meet up?

[Aaron Hill]

I'm available on Saturday

[Austin Letson]

Saturday works for me

[Austin Letson]

1pm?

[Julian Berman]

Good here.

[Matt Diamond]

What are you guys working on lately? I keep meaning to swing by one of these days

[Julian Berman]

Come! We generally decide when we're there honestly the past few weeks hah. If you have anything you think we could work on all together obviously feel free to suggest it, otherwise we've worked on a few different things the past few months (bit of Carleson project which Austin just finished, bit of Aaron's polynomial proof, bit of generating function stuff, ...).

[Julian Berman]

Ellie's sick :/ so think I won't be able to make today after all unfortunately.

[Austin Letson]

Oh no :( I hope she gets better soon!

[Austin Letson]

@Aaron Hill does 1pm at Sumptown still work for you?

[Tung-che Chang]

I'd like to join! I'm a phd student at Rutgers.

[Aaron Hill]

Austin Letson said:

Aaron Hill does 1pm at Sumptown still work for you?

Sounds good to me

[Aaron Hill]

Tung-che Chang said:

I'd like to join! I'm a phd student at Rutgers.

We're meeting at https://www.google.com/maps/place/Stumptown+Coffee+Roasters/@40.7457399,-73.9882272,587m/data=!3m2!1e3!4b1!4m6!3m5!1s0x89c259a61c75684f:0x79d31adb123348d2!8m2!3d40.7457399!4d-73.9882272!16s%2Fg%2F1hhw712x0?entry=ttu&g_ep=EgoyMDI0MTExOS4yIKXMDSoASAFQAw%3D%3D - looking forward to seeing you there

[Austin Letson]

I got a coffee and sat inside

[Austin Letson]

@Tung-che Chang we are in the hotel lobby that you can get to by the door at the back of sumptown

[Tung-che Chang]

Just getting my coffee

[Aaron Hill]

We're setting at a table in the back

[Tung-che Chang]

I'm inside the lobby but I don't know where you guys are

[Austin Letson]

Nice to meet you @Tung-che Chang. Hope to see you again soon!

[Tung-che Chang]

Likewise!

[Aaron Hill]

Anyone around this weekend?

[Julian Berman]

Yeah I should be up for the usual!

[Aaron Hill]

I can't make it at 1pm on saturday, but I'll be around later in the day

[Austin Letson]

I am out of town, but I will catch you guys next time

[Austin Letson]

Happy Thanksgiving :turkey:

[Julian Berman]

Happy Thanksgiving! Ok let's shoot for later tomorrow afternoon then for a non-Austin pair meetup.

[Dean Young]

I am going to be in NYC from the evening of the 4th to midday on the 6th. Are any of you all free to meet up then?

[Aaron Hill]

Julian Berman said:

Happy Thanksgiving! Ok let's shoot for later tomorrow afternoon then for a non-Austin pair meetup.

I'm available for the rest of the day

[Julian Berman]

Cool, should be good to go here too, could meet there at 3 if that works?

[Aaron Hill]

Sounds good

[Julian Berman]

I was declogging a sink, lucky me -- so I'll be a bit late, sorry, leaving now, so 3:15 should be there.

[Aaron Hill]

I have a table in the back

[Julian Berman]

Folks around for tomorrow?

[Austin Letson]

I am down. Could we do 12?

[Austin Letson]

E. Dean Young said:

I am going to be in NYC from the evening of the 4th to midday on the 6th. Are any of you all free to meet up then?

Sorry I missed you Dean. During the week is a bit harder for me

[Julian Berman]

Gonna leave here in 5, should be there at 12ish.

[Austin Letson]

I am transferring at 42. Will be there 12ish as well

[Julian Berman]

I know most of us are away, hopefully enjoying -- I'm back in town as of today, so if anyone actually is around this weekend either day and cares to meet up let me know. Otherwise happy holidays + new years NYC!

[Austin Letson]

Happy Holidays! :statue: I am getting ready to leave for Ireland otherwise I would be down.

[Aaron Hill]

Anyone around this weekend?

[Julian Berman]

Yeah think I can do a bit!

[Julian Berman]

@Aaron Hill were you thinking today? Or yesterday and I should have pinged you.

[Aaron Hill]

Later today would work for me

[Julian Berman]

Cool, let's do it!

[Aaron Hill]

What time would work for you?

[Julian Berman]

I should be good in an hour here.

[Aaron Hill]

Sounds good

[Aaron Hill]

I grabbed a table

[Julian Berman]

Leaving now, there in 10!

[Aaron Hill]

Anyone around tomorrow?

[Julian Berman]

I had terrible headaches the last two days , but long as those are a bit better in the morning I'm good for tomorrow yeah!

[Matej Penciak]

I'm finally back in town, so I'm able to make it this weekend

[Aaron Hill]

Does 1pm today sound good?

[Julian Berman]

Will be there more like 1:30 here, have a bit to do still at home before I can head over, but see y'all soon.

[Matej Penciak]

I am also going to be late, the A isn't running past 168th so I need to do some transfers

[Aaron Hill]

I'm also running late

[Austin Letson]

Is anyone around on Saturday to meet up?

[Julian Berman]

Yep I'm in.

[Austin Letson]

How does 1 work? @Julian Berman @Aaron Hill

[Aaron Hill]

Sounds good

[Austin Letson]

I have the high table in the back

[Julian Berman]

We around this weekend?

[Julian Berman]

Anyone have preference between later today or tomorrow?

[Aaron Hill]

Later today works for me

[Julian Berman]

Cool, shall we go for 1 again?

@Austin Letson @Matej Penciak y'all around (or anyone else of course)

[Julian Berman]

Will get there more like 130 again, just back from the :dog: :syringe:.

[Matej Penciak]

I've been feeling a little under the weather the last couple days, so I think I'm gonna stay in today

[Julian Berman]

Feel better!

[Aaron Hill]

I'll be there in a few minutes

[Julian Berman]

K see you in a sec

[Aaron Hill]

I got a table in the back

[Austin Letson]

I can't meet up today, but I will be around next weekend

[Aaron Hill]

Julian and I finished the polynomial span proof - I pushed it to the branch

[Austin Letson]

Are others around this weekend?

[Austin Letson]

I have a hard stop at 3 on Saturday so would be down to meet a little earlier at like 12?

[Julian Berman]

I'm in Italy till next week making delicious food disappear, will see y'all at the next one.

[Austin Letson]

Does 12 today at Sumptown still work for you @Matej Penciak and @Aaron Hill?

[Aaron Hill]

Sounds good

[Matej Penciak]

Yup! I'll see you guys there! (A is being funky again, so I might be a tad late as usual)

[Austin Letson]

My ETA is 12:15

[Matej Penciak]

Just got here! Haven't gotten a table yet, but I'm keeping my eyes peeled

[Aaron Hill]

#PrimeNumberTheorem+ > Outstanding Tasks V6

[Aaron Hill]

I managed to finish the PNT+ proof of pn_pn_plus_one (though it's pretty messy atm): https://github.com/Aaron1011/PrimeNumberTheoremAnd/tree/aaron/pn_pn_plus_one

[Aaron Hill]

I ended up repeating splitting up the limit (into lim(p_(n+1) / p_n) + lim(p_n / p_n), and then repeating with the asymptotic stuff), which ended up being much easier to work with

[Austin Letson]

Woo! That was quick

[Austin Letson]

Ah, that split makes sense

[Aaron Hill]

the o(1) constant was very difficult to deal with in the original way we tried to prove it, since you have 'k(n +1)' and 'k(n)' terms

[Aaron Hill]

splitting it into two limits made it much easier (and it was also easier to target the right things with rw and conv)

[Aaron Hill]

Unless anyone else wants to make changes, I'm going to clean it up and pr it sometime this week

[Austin Letson]

Aaron Hill said:

Unless anyone else wants to make changes, I'm going to clean it up and pr it sometime this week

Excellent! I could take a pass at golfing on Friday if there is still clean up to be done by then. No pressure to hold off on a PR though

[Austin Letson]

Are others around on Saturday?

[Austin Letson]

Aaron Hill said:

I managed to finish the PNT+ proof of pn_pn_plus_one (though it's pretty messy atm): https://github.com/Aaron1011/PrimeNumberTheoremAnd/tree/aaron/pn_pn_plus_one

I did some minor :golf: https://github.com/Aaron1011/PrimeNumberTheoremAnd/pull/1

Feel free to reject anything that seems less readable

[Julian Berman]

@Austin Letson @Aaron Hill just to mention it as an option -- I guess given we've had some issues finding spots with power and tables the last few weeks, happy to also offer up my apt (today or any time). I don't have a blackboard anymore but wifi and coffee come included as bribes for tolerating Ellie coming to disrupt our fun.

[Aaron Hill]

That sounds good to me - thanks for offering!

[Austin Letson]

That sounds good to me! I am excited to see Ellie again!

[Austin Letson]

Does 1 work for you two?

[Julian Berman]

OK cool just pull open https://leanprover-community.github.io/meet.html and follow the pin until you're staring through my window.

[Julian Berman]

(Will DM the address :)

[Julian Berman]

We on again?

[Matej Penciak]

I don't think I can make it to this weekend, but I'll catch you guys at the next one!

[Austin Letson]

I am down to meet up today

[Austin Letson]

Does 1 today work for others?

[Julian Berman]

Yep perf -- door's open here if you want to do it here again, otherwise cafe or wherever of course.

[Austin Letson]

I am down to come to your place

[Aaron Hill]

I'm ~15 minutes out

[Austin Letson]

I am around the corner

[Julian Berman]

Leonardo de Moura seems like he'll be in town next month on 2025-03-12T18:00:00-04:00 for a (free public) talk at the Simons Foundation. Details are here: https://www.eventbrite.com/e/verified-collaboration-lean-project-mathematics-programming-and-ai-tickets-1245242266139 just signed up myself so see any of you there hopefully.

[Austin Letson]

Ilena and I just signed up!

[Austin Letson]

Also are others around this weekend to meet up?

[Julian Berman]

Door's open here for today if y'all want.

[Austin Letson]

Excellent. Does 1 work for others?

[Matej Penciak]

I'll be like 30 minutes late, but that works for me

[Julian Berman]

I have a lot going on this weekend but would still like to set aside at least another hour or two tomorrow for mathing if you guys are around (and hopefully even a bit more if I manage to get everything done in the morning beforehand...). Lemme know if so!

[Austin Letson]

I am in NC this weekend so I will see you all next time.

[Matej Penciak]

I'm around!

[Aaron Hill]

Would some time later today work for everyone?

[Julian Berman]

Yeah I should be home/ready around 2:30-3 if that works.

[Matej Penciak]

I woke up feeling kind of sick this morning so I'm going to try to stay in this weekend

[Julian Berman]

Oy. Feel better!

[Aaron Hill]

I can head over now if you're still available

[Julian Berman]

Yep all ready here!

[Austin Letson]

Who else is going to the Simons Foundation talk tonight?

[Kristoffer Josefsson]

I had planned to go but am not able to (last minute changes). If it’s sold out and someone wants my spot let me know!

[Aaron Hill]

Anyone around today?

[Julian Berman]

I'm taking Ellie to the dog beach?! -- but then I should be back towards the late afternoon (330-4ish I'm sure) if that works -- obviously if others are around earlier happy to join wherever you head to, otherwise my place will be open

[Aaron Hill]

4pm works for me

[Julian Berman]

On the way home now so 5 is a bit better if that works!

[Aaron Hill]

Sounds good

[Julian Berman]

Who's in this weekend?

[Austin Letson]

I am down

[Austin Letson]

Does Saturday work for others?

[Julian Berman]

Yep here.

[Austin Letson]

Should we meet at 1?

[Julian Berman]

Works here!

[Austin Letson]

Where should we meet? I personally like working at your place Julian with Ellie for company :puppy: but I am also of course always happy to meet somewhere else given that it is your house :)

[Julian Berman]

Invite's open for here :) -- I do as well!

[Julian Berman]

Though I'm out of decaf coffee :D, will have to get a stash to keep on hand.

[Austin Letson]

Don't fret. I have some with me :coffee:

[Austin Letson]

I am around the corner

[Austin Letson]

Are there others around this weekend?

[Matej Penciak]

I'm back from Bulgaria, so I can make it this weekend!

[Julian Berman]

I'm around!

[Austin Letson]

Does 1 tomorrow work?

[Julian Berman]

Yep, and my place is open

[Julian Berman]

I'm at the noodle place just downstairs from my apt if anyone shows up early, will be done in a few minutes. EDIT: Home

[Austin Letson]

My ETA is 1:15

[Austin Letson]

Are others around on Saturday?

[Julian Berman]

How the hell is it Wednesday already...

[Julian Berman]

But yep for me!

[Aaron Hill]

I don't think I can make it on Saturday, but I'll be around on Sunday

[Matej Penciak]

I could do either day, but Sunday would be a bit better for my schedule if possible

[Julian Berman]

I can do Sunday I think too

[Austin Letson]

I am unable to do Sunday.

[Austin Letson]

I am still down to hack on rpylean for a few hours this afternoon for those that can make it, however if Sunday works better overall no worries.

[Julian Berman]

Well come on by :) I can do both.

[Austin Letson]

Sounds good. Does 1:30 work?

[Aaron Hill]

Anyone around this weekend?

[Julian Berman]

I'm away for passover this weekend but hope to see y'all next week

[Austin Letson]

@Aaron Hill Did you move yet?

[Aaron Hill]

I just signed a lease in Greenpoint, but I'm still in Manhattan for a little bit

[Austin Letson]

@Matej Penciak and @Aaron Hill want to meet at sumptown at 1?

[Aaron Hill]

I have a table in the back

[Austin Letson]

I am waiting for the N at times square. I will be there in 10 minutes

[Matej Penciak]

Austin Letson said:

I am waiting for the N at times square. I will be there in 10 minutes

Me too!

[Aaron Hill]

I finished the proof - the trick was to do everthing in ℤ_[p] (instead of in ℚ_[p] with Submodule.one), and then convert the statement about the relindex using AddSubgroup.relindex_comap

[Aaron Hill]

the proof is inline in distribHaarChar_padic_padicInt (the original smul_submodule_relindex is more general - it takes an arbitrary submodule rather than just Submodule.one)

[Aaron Hill]

and that lemma apparently needs to use compactness in some way: https://github.com/ImperialCollegeLondon/FLT/pull/407

[Aaron Hill]

I'll ask about it

[Yaël Dillies]

Aha! This is why people suddenly got interested in my blueprint item :smile: Keep up the good work!

[Aaron Hill]

Anyone around today or tomorrow?

[Matej Penciak]

Greta had a surgery yesterday so I'm going to be tending to her this weekend :( PXL_20250418_222817987.MP.jpg

[Austin Letson]

I am tied up this weekend. But I will see you all next time

[Julian Berman]

Same here I'm afraid... next weekend should hopefully be better. Ellie sends Greta cone sympathies, hope she's on the mend.

[Aaron Hill]

I cleaned up and submitted the PNT+ theorem we proved a while back: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/251

[Austin Letson]

Woo! Thanks Aaron

[Ruben Van de Velde]

I see "TODO - upstream to mathlib" - you going to do that as well? :)

[Julian Berman]

I was trying to generalize those and got stuck (and the branch has sat there since then) -- it's branch#count-more where I put just basically the proof there, along with a sorried out proof of the other direction (which is where I got stuck) and then a finset version

[Aaron Hill]

I think the converse direction of count_lt_count_iff_exists isn't actually true - if only p a holds, then the count doesn't increase going from a to b

[Kevin Buzzard]

Thanks a lot for the FLT work -- I just merged it!

[Julian Berman]

Shall we try for tomorrow? Anyone around?

[Julian Berman]

@Matej Penciak how's Greta?

[Aaron Hill]

I'm around the rest of today

[Julian Berman]

@Aaron Hill Cool, looks like it's gonna rain so indoors I guess -- invite's open here unless you have another pref on where to meet up!

[Aaron Hill]

Sounds good - I'll head over in about 20 minutes if that works for you

[Julian Berman]

Great! See you in a bit.

[Eric Wieser]

I'll be around in midtown for an hour or two this evening, if anyone wants to grab and recommend a place for a drink

[Yakov Pechersky]

:/ takes an hour to get to midtown for me...

[Yakov Pechersky]

But I'm a fan of The Perfect Pint on 46th. That might be too similar to a British pub for you, maybe you want something less familiar

[Julian Berman]

Oy, yeah I'd have loved to meet you in person but I'm on my way to the airport. If you want a random recc and like amaro my favorite bar is Amor y Amargo on 6th and A, which isn't midtown but is worth the trip.

[Matej Penciak]

I'm catching up on work after a week of tending to Greta, so I wouldn't be able to join... But I've had a decent time at Dolly Varden at 51st & 8th in the past (with the usual caveats that come with hanging out in midtown)

[Matej Penciak]

Julian Berman said:

Matej Penciak how's Greta?

She's doing a lot better! She wants to get back to playing as hard as she used to, but doctor's orders say she needs a bit more rest

[Eric Wieser]

I'll be around most of Saturday as well

[Matej Penciak]

Eric Wieser said:

I'll be around most of next Saturday as well

I'll be around Saturday as well!