Berlin, DE

Stream: Geographic locality

[Tom Houlé]

Hello there! I'm a software engineer who started using Lean mostly as a tool for exploring more mathematics, but also interested in other applications long term. Anyone else in Berlin?

[Paul Boes]

Hey, I'm a recently graduated PhD in quantum information theory based in Berlin.

[David Blitz]

Hello, I'm based in Berlin and I work in an AI startup as a researcher. I'm currently working through the 'lost levels' of the natural number game.

[Gagan Bhatia]

Hello, I'm a software engineer who started using Lean to explore proofs. I have a background in Physics and Chemical Engineering. I'm based in Berlin.

[Adam Kurkiewicz]

Hi all,

I'm a small business owner and a bioinformatician, with a recent interest in the F2F IMO grand challenge. I'm currently learning lean, and based in Charlottenburg, in Berlin.

[Michael Rothgang]

Hello everybody. I'm finishing my PhD in symplectic geometry (working with Chris Wendl at HU, on equivariant pseudo-holomorphic curves). I started really working with Lean last autumn, got hooked pretty quickly and stuck around because I like this community.

My eventual vision is to formalise symplectic geometry. As that field has pretty broad foundations, I'm interested in formalising many things. So far, I worked on formalising Sard's theorem, some differential geometry and the inverse function theorem (for Banach manifolds). Recently, I started cleaning and helping to upstream results from the sphere eversion project: it would be a shame for this to rot outside of mathlib. I guess I like cleaning up and polishing.

[Kim Morrison]

These are great topics! Looking forward to seeing lots of PRs. :-) And getting sphere eversion material in is super helpful.

[Michael Rothgang]

New large PRs will have to wait a bit until my thesis is done. If you reading this want to help, feel free to review some of my pending PRs :-)

You can also help me working on #8738, #11185 or #10303: all of them require some work; I'll get to them eventually, but not necessarily soon. (Feel free to ping me if something is unclear from the thread.)

[Ruben Van de Velde]

We prefer small PRs anyway ;)

[Michael Rothgang]

I meant "large" as in "new conceptual work" - but I agree with you :-)

[Patrick Massot]

The work that you are doing is super useful. I am really sorry I don’t have more time to work with you, I hope that will change. I’m not reviewing the PRs coming from the sphere eversion since they are mostly PRing my code, but I’m very grateful that you do this.

[Kim Morrison]

(Maybe this is a discussion for another thread, but if reviewing these PRs is the bottleneck I would not object to Patrick merging Michael's PRs from sphere eversion.)

[Ralf Stephan]

Bioinfo here, as well, part-time biocurating for Reactome, but that's the job, math is the hobby.

[Michael Rothgang]

Cross-linking for visibility: there will be an informal Lean workshop at the HU math department in Adlershof on May 10. The main target group are university people, but that's not a hard requirement.

[Yves Jäckle]

Hey, I work in Berlin :bear:

[Adam Kurkiewicz]

Hey all,

I've been thinking to start some kind of informal in-person Lean meetup here in Berlin (maybe once a month for a good start?). Anybody would be interested?

Curious to hear what you've all been studying from or formalising! Personally I've been using Lean to formalise IMO number theory problems and their solutions and contribute them to Compfiles (e.g. https://github.com/dwrensha/compfiles/pull/44).

The meetup format could be just a chat over beers for a good start, but we could evolve into a more formal setting with talks, workshops, etc... later on.

[Vlad Tsyrklevich]

I'd be interested. I'm fairly new to lean, but slowly learning it as I participate in #Equational and work my way through #fpil. It would be nice to meet others with similar interests.

[Michael Rothgang]

I have moved to Bonn now - but reading about this makes me happy :-)

[Adam Kurkiewicz]

Hey Vlad, I think this will be a very tiny meetup (just you and me it looks like for now!), but I'm keen to do this nonetheless :). I'm near Charlottenburg Schloss, and we do have a very good local brewery. Which part of town are you in?

Equational looks like an interesting project, I've been lurking and reading the chat, but haven't made any contributions yet.

[Jesse Alama]

Anyone interested in a Lean meetup in Berlin, Germany on Saturday, March 15th, 2025? There will be a good number of functional programmers in town for BOBKonf 2025, which takes place on the 14th. (Lean was the topic of a tutorial earlier this year, led by @Joachim Breitner and @David Thrane Christiansen .) If there's enough interest I can try booking a little coworking spot for us.

[Michael Rothgang]

I'm not in Berlin any more, but really happy to see this question!

[Michael Rothgang]

There was also a one-day Lean intro last May, more focused on theorem proving. Perhaps somebody from then is interested? Pinging some people who I know were there: @Nicolas Alexander Weiss @Yves Jäckle @Tobias Bucher @Ben Eltschig @Tom Kranz

[Yves Jäckle]

I'd be interested :+1:

[Yves Jäckle]

Btw, this comes a little late, and I don't know if this has been advertised on zulip already, but there's a workshop today and tomorrow here in Berlin.
Even if you don't partake, I think it would be fine if anyone interested in Lean joins for lunsh or dinner @Nicolas Alexander Weiss @Tobias Bucher @Ben Eltschig @Tom Kranz @Vlad Tsyrklevich @Adam Kurkiewicz

[Nicolas Alexander Weiss]

Yves Jäckle said:

Btw, this comes a little late, and I don't know if this has been advertised on zulip already, but there's a workshop today and tomorrow here in Berlin.
Even if you don't partake, I think it would be fine if anyone interested in Lean joins for lunsh or dinner Nicolas Alexander Weiss Tobias Bucher Ben Eltschig Tom Kranz Vlad Tsyrklevich Adam Kurkiewicz

Hey, thanks for the update! I'm moving to Leipzig soon to start working on my PhD in algebraic analysis However, not from a formalisation perspective yet. Perhaps thats a nice project for the future.

[Jesse Alama]

Another counterproposal to Saturday, March 15th would be Thursday, March 13th. I'm in touch with a Berlin coworking space and find that they're not exactly enthused about hosting a small event on a Saturday, when they're normally closed.

[Adam Kurkiewicz]

Thanks @Jesse Alama and @Yves Jäckle for advertising both opportunities. I was unfortunately travelling in Scotland, and now back in town but travelling again soon. @Vlad Tsyrklevich and I have been planning to meet up for a lean proto-meetup/coffee for a couple weeks now, maybe we can make it happen in the new year.

@Jesse Alama , would you like me to ask at 42 Berlin? I've seen them host these kind of events on a Saturday (and they are open on Saturdays anyway). The "price" of them hosting the event might be that we engage the students in some way (42 Berlin is a private university/ coding school)

[Adam Kurkiewicz]

I and @Vlad Tsyrklevich just arranged to meet in World Chess Club at 6pm on Monday the 6th of January:

https://maps.app.goo.gl/AUosFLasrKQE1Uz1A

All feel free to join us, but if there's lots of you we should maybe let the venue know :sweat_smile:

[Jesse Alama]

Adam Kurkiewicz said:

Thanks Jesse Alama and Yves Jäckle for advertising both opportunities. I was unfortunately travelling in Scotland, and now back in town but travelling again soon. Vlad Tsyrklevich and I have been planning to meet up for a lean proto-meetup/coffee for a couple weeks now, maybe we can make it happen in the new year.

Jesse Alama , would you like me to ask at 42 Berlin? I've seen them host these kind of events on a Saturday (and they are open on Saturdays anyway). The "price" of them hosting the event might be that we engage the students in some way (42 Berlin is a private university/ coding school)

I'm happy to announce that I've found a space at a coworking venue (one that I've used in the past for other conferences). Come join us at Leaning In! 2025 on Thursday, March 13th, 2025. More information on the web page.

[Jesse Alama]

Is there any chance we could set up a channel for Leaning In! in Zulip, similar to how other events (e.g. Lean Together) have their own channel? I'm not sure who to ask about this.

[Kevin Buzzard]

Is this any different to #new members ?

[Joachim Breitner]

Yes, on new members you wouldn't expect discussion on what restaurant to go to in Berlin after the workshop, I assume :-)

[Kevin Buzzard]

Oh apologies, I misread as "Learning Lean in Zulip" :-) Yes definitely make a channel!

[Johan Commelin]

I've contacted Jesse via DM to create a channel.

[Yves Jäckle]

Is #Geographic locality > Berlin, DE @ 💬 still planned ?
If so, here is what I look like, and I'll be wearing blue

[Vlad Tsyrklevich]

It is still planned! See you at World Chess Club. I'll be in a greenish plaid shirt.

[Adam Kurkiewicz]

Hmm, if Google can be trusted, it looks like World Chess Club is closed today:

https://maps.app.goo.gl/Fib2oFD2LuSW3pwM8

[Vlad Tsyrklevich]

Oops, that's a silly oversight on my part.

[Adam Kurkiewicz]

Their websites says it too:

Screenshot 2025-01-06 at 16.42.42.png

[Adam Kurkiewicz]

It's Mitte though, there should be another place

[Adam Kurkiewicz]

Maybe an Irish pub?

https://maps.app.goo.gl/44toADNtrwPar8RW9

[Vlad Tsyrklevich]

They serve food which means they're non-smoking, so that sounds great to me.

[Vlad Tsyrklevich]

I'll explicitly cc @Yves Jäckle to make sure he sees the above

[Vlad Tsyrklevich]

Arrived a few minutes early, got a table against the window

[Yves Jäckle]

On my way to #Geographic locality > Berlin, DE @ 💬 now

[Yves Jäckle]

@Kelly Davis
If you want to meet people doing Lean, we can go for lunsh/coffee/dinner ?
Could do another semi-casual meetup with @Vlad Tsyrklevich and @Adam Kurkiewicz .
Perhaps also with @Ben Eltschig , @Christoph Stephan , @ooovi ?

[Kelly Davis]

Yves Jäckle said:

Kelly Davis
If you want to meet people doing Lean, we can go for lunsh/coffee/dinner ?
Could do another semi-casual meetup with Vlad Tsyrklevich and Adam Kurkiewicz .
Perhaps also with Ben Eltschig , Christoph Stephan , ooovi ?

I'd be up for it!

[Théo Tyburn]

I would also be in!

[Yves Jäckle]

(waiting for tagged-people's responses before setting a date)

[Christoph Stephan]

I would also be in! Preferably for dinner since I have to teach most of the week in Potsdam

[Ben Eltschig]

I would certainly also be interested :)

[Vlad Tsyrklevich]

I’m in, pretty flexible time wise

[ooovi]

yes lets!

[Yves Jäckle]

/poll Which evening would you be available ?
Monday 12.05
Tuesday 13.05
Wensday 14.05
Thursady 15.05
Friday 16.05
Monday 19.05
Tuesday 20.05
Wensday 21.05
Thursday 22.05
Friday 23.05
Later

[Yves Jäckle]

(waiting for two more votes)

[Yves Jäckle]

Ok, let's meet Monday the 19th :+1:
Does anyone know a nice coworking-ish place ?
I found Blumental, which has a coworking café that doesn't require booking. It's only open until 6pm though. So We could meet there at 5pm, and go for dinner somewhere in the area at 6pm ?

[Kelly Davis]

Never been there, but Blumental seems like a great choice other than the closing time.

There are a quite a few restaurants within walking distance: Home of Dumplings, Mon Eatery & Bar, Caphe HOA, AMRIT... If anyone has a recommendation, let us know.

[Ben Eltschig]

If I'm reading correctly, Blumental seems to be closed entirely on mondays and tuesdays? so it wouldn't work for the 19th

[Kelly Davis]

Ben Eltschig said:

If I'm reading correctly, Blumental seems to be closed entirely on mondays and tuesdays? so it wouldn't work for the 19th

I concur; Blumental is closed on Monday and Tuesday. Mon Eatery & Bar is open on Mondays from 12:00 until 22:00. So we could meet there at, say, 17:00.

[Vlad Tsyrklevich]

I'm happy to join after ~1815

[Kelly Davis]

Vlad Tsyrklevich said:

I'm happy to join after ~1815

We could all simply meet at 18:00, and you join at 18:15. I think 17:00 might be a bit early for some to make it there.

[Yves Jäckle]

Ok for Monday the 19th at 18:00 at Mon Eatery & Bar ?
We can sit down so that new users are next to experienced ones. I'm sure if we bring out the laptops for desert, the staff won't mind.
The alternative would be Blumental on Wensday the 21.

[Kelly Davis]

Yves Jäckle said:

The alternative would be Blumental on Wensday the 21.

Blumental on Wensday the 21 is only open until 18:00.

[Yves Jäckle]

So let's definitely settle for Monday the 19th at 18:00 at Mon Eatery & Bar.

[Paul Lezeau]

A bit last minute, but I’ll be around in Berlin from this evening to Sunday if anyone wants to grab a coffee:)

[Yves Jäckle]

Damn, I had visitors this weekend :smiling_face_with_tear: Next time though :+1:

[Vlad Tsyrklevich]

Sitting inside if anyone is coming late

[Adam Kurkiewicz]

Sorry guys, I actually moved to London so no longer around for those in Berlin. Hope you all had a great time!!!

[Moritz Firsching]

I'll be in Berlin on Thursday , 2025-09-18 and plan to have lunch in Dahlem somewhere, possibly the FU mensa, anybody up for it?!

[ooovi]

(deleted)

[Moritz Firsching]

we are planning to meet at 2025-09-18T12:30:00+02:00 at the Pi-Building (Arnimallee 6), go for lunch and perhaps do some lean afterwards, everybody welcome!

[Shreyas Srinivas]

I am in Berlin this week till Friday. Are there any lean related meetings happening?

[Yves Jäckle]

Hey!
Shreyas Srinivas said:

Are there any lean related meetings happening

None that know of...
But we can do a spontaneous informal meeting :smile:

[Yves Jäckle]

I don't have the permission to use @**topic** here on zulip, so I guess we have to wait til people read this.

[Yves Jäckle]

/poll When are you available ?
Wensday afternoom
Wensday evening
Thursday afternoom
Thursday evening
Friday afternoon
Friday evening

[Michael Rothgang]

@topic for the above poll

[Michael Rothgang]

Seems I have the permissions :-)

[Michael Rothgang]

I'm not in Berlin this week, but have fun!

[Yves Jäckle]

How about Thursday, 18h (6 pm), at this location ? This is just as a meeting spot, we can decide where to go from there.

[Klaus Gy]

can i join, although i dont know any of you? just as a lean-interested programmer :)

[Shreyas Srinivas]

The place sounds good to me. It seems I can reach it by taking the U3

[Shreyas Srinivas]

The time might be a bit inconvenient. 19:00 or later would be much better since I am at a conference

[Shreyas Srinivas]

Klaus Gy said:

can i join, although i dont know any of you? just as a lean-interested programmer :)

I am meeting everybody here for the first time.

[Vlad Tsyrklevich]

7 works for me. Shall we eat beforehand then? I could also wait, not sure how that area is for falafel/döner spots but something quick might make planning easy last minute

[Shreyas Srinivas]

I wouldn’t get a chance to eat before that

[Shreyas Srinivas]

Basically I’d catch the first train from from Freie universität

[Vlad Tsyrklevich]

What’s the conference at FU? That’s where I and I also assume Yves will be traveling from as well

[Shreyas Srinivas]

It’s DISC at Harnack haus.

[Yves Jäckle]

If we're all at FU we could meet there ?
So shall we switch to meeting in front of U Dahlem Dorf (main entrance to the subway station) at 6 pm ?
Wrt:
Vlad Tsyrklevich said:

Shall we eat beforehand

I thought we could go eat together :face_holding_back_tears:
@Klaus Gy are you near Dahlem ?

[Klaus Gy]

No, I'll be probably around Ernst-Reuter-Platz or Zoo

[Yves Jäckle]

Food options aren't great in Dahlem, so we'll have to move someplace better anyway

[Yves Jäckle]

/poll Organization
Meet at Dahlem, talk Lean at Dahlem, eat somewhere
Meet at Dahlem, meet Klaus at Zoo, eat and talk Lean somewhere

[Yves Jäckle]

Shreyas Srinivas said:

19:00 or later would be much better

Forgot about this. Of course, we can meet at 19:00 :+1:

[Klaus Gy]

i can also come to dahlem :) just whatever suits you best!

[Shreyas Srinivas]

Either works for me.

[Yves Jäckle]

@Vlad Tsyrklevich
Looks like your vote is the only one that can settle this :sweat_smile:

[Vlad Tsyrklevich]

I gotta head east anyway to go home so let’s go to Zoo

[Shreyas Srinivas]

What’s the exact place (I am new here and need to use the apps to find my way)

[Yves Jäckle]

Ok so @Shreyas Srinivas @Vlad Tsyrklevich and I are meeting at 19:00 at the entrance to U Dahlem Dorf
We'll take the U3 and then the U9 to go to Zoo and meet @Klaus Gy at this location at Kudamm at around 19:25 to 19:35.
See you tomorow :+1:

[Shreyas Srinivas]

I invited @Henrik Lievonen who is also at DISC. He might join us.

[Shreyas Srinivas]

I forgot to mention this, we have two vegetarians in the group. So ideally we should find a place whose veggie options go beyond salad and potatoes.

[Vlad Tsyrklevich]

In Berlin vegan options abound

[Klaus Gy]

i stand now btw this hectagon and gedächtniskirche

[Klaus Gy]

is that the meeting point you planned?

[Shreyas Srinivas]

I am at the dahlem dorf u Bahn station entrance

[Shreyas Srinivas]

Wearing a white full sleeve shirt

[Klaus Gy]

aah sorry so we meet at dahlem? i didnt get this. can you tell me where you are heading? will catch the next train to dahlem

[Klaus Gy]

at dahlem-dorf in 5 mins

[Shreyas Srinivas]

Uh

[Shreyas Srinivas]

We just reached the zoo ubahn

[Klaus Gy]

aah ok im heading back now just tell me where you go!

[Shreyas Srinivas]

https://maps.app.goo.gl/A5Vmw6XuCgk53aqL7?g_st=ic

[Shreyas Srinivas]

This is the restaurant I mentioned https://en.wikipedia.org/wiki/Hindoostane_Coffee_House?wprov=sfti1

[Shreyas Srinivas]

image_3351FC3A-CCC8-49F8-9A42-A6E9475EB0E3_1761865869.heic

[Jesse Alama]

Leaning In! 2026 wlll be on March 12th in Berlin!

[Aaron Elligsen]

Hello Berliners,
I’m hosting an online meetup called “Advent of Code Verified!”, where we’ll work through an Advent of Code puzzle and try to formally verify our solutions using Dafny (and anyone is welcome to bring Lean or other tools as well).

If you’re interested in a collaborative session mixing AoC with formal methods, you’re warmly invited to join:
https://www.meetup.com/berlin-software-verification-meetup/events/312095241/

[Christoph Stephan]

Hi everyone in Berlin and surroundings,

on 17 December Michael Rothgang and María Inés de Frutos Fernández will speak in the colloquium at our institute (Mathematics, Uni Potsdam in Golm):

https://www.math.uni-potsdam.de/institut/veranstaltungen/details-1/veranstaltungsdetails/formalising-mathematics-differential-geometry-and-number-theory-in-the-lean-proof-assistant

If you are interested, come around to Golm!

Best, Christoph