Zulip Chat Archive

Stream: Geographic locality

Topic: Berlin, DE

Tom Houlé (Jun 26 2020 at 11:19):

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 (Aug 20 2020 at 07:59):

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

David Blitz (Nov 22 2020 at 19:27):

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 (Feb 24 2021 at 12:24):

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 (Aug 13 2023 at 14:20):

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 (Mar 17 2024 at 21:34):

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 (Mar 17 2024 at 22:27):

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

Michael Rothgang (Mar 18 2024 at 10:14):

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 (Mar 18 2024 at 10:42):

We prefer small PRs anyway ;)

Michael Rothgang (Mar 18 2024 at 10:53):

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

Patrick Massot (Mar 18 2024 at 15:34):

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 (Mar 18 2024 at 23:00):

(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 (Apr 10 2024 at 17:07):

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

Michael Rothgang (Apr 12 2024 at 16:53):

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 (May 09 2024 at 21:50):

Hey, I work in Berlin :bear:

Adam Kurkiewicz (Oct 20 2024 at 14:42):

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 (Oct 21 2024 at 11:05):

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 (Oct 21 2024 at 12:24):

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

Adam Kurkiewicz (Oct 21 2024 at 14:22):

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 (Dec 04 2024 at 10:22):

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 (Dec 04 2024 at 11:11):

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

Michael Rothgang (Dec 04 2024 at 11:16):

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 (Dec 05 2024 at 09:15):

I'd be interested :+1:

Yves Jäckle (Dec 05 2024 at 09:18):

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 (Dec 05 2024 at 15:27):

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 (Dec 06 2024 at 09:39):

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 (Dec 18 2024 at 15:16):

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 (Dec 18 2024 at 16:17):

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 (Dec 31 2024 at 06:52):

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 (Jan 03 2025 at 05:39):

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.