Stream: Geographic locality
Topic: Karlsruhe, DE
Marc Huisinga (Feb 28 2020 at 10:46):
@Sebastian Ullrich , @Markus Himmel and myself are at KIT in Karlsruhe. Sebastian supervised my CS BSc thesis and is now co-supervising Markus' math+CS BSc thesis.
Jakob von Raumer (Apr 12 2020 at 12:31):
In Karlsruhe, Germany right now, being stuck at my parents place after Covid-19 destroyed my travel plans for the early summer. Spending the time looking for jobs :point_left: :bangbang: :upside_down:
Alexandre Rademaker (Apr 12 2020 at 12:44):
But what is the idea of this stream?
Kevin Buzzard (May 03 2020 at 14:53):
To enable people who are geographically close and share common interests to find each other?
Shekhinah Memmel (Dec 27 2020 at 10:59):
I'm from Hadiko.
Shekhinah Memmel (Dec 27 2020 at 11:02):
I'm from Hadiko.
Darij Grinberg (Jan 26 2021 at 15:22):
first time I'm seeing a Karlsruhe group in a math community. hi from Waldstadt
Johan Commelin (Jan 26 2021 at 15:22):
Karlsruhe is super critical for Lean's existence (-;
Darij Grinberg (Jan 26 2021 at 15:24):
just by numbers or is there a working group at the KIT?
Johan Commelin (Jan 26 2021 at 15:24):
One of the two core developers is at KIT
Johan Commelin (Jan 26 2021 at 15:25):
so, maybe not by numbers, but if you do a weighted count, then....
Sebastian Ullrich (Jan 26 2021 at 15:30):
@Jakob von Raumer did find a job here as a postdoc, so I guess two people now makes us an actual Lean group!
Darij Grinberg (Jan 26 2021 at 15:30):
ah, a nontrivial group :)
Darij Grinberg (Jan 26 2021 at 15:31):
i have no KIT connection (i "work" in Philadelphia); i'm just here for the pandemic
Sebastian Ullrich (Jan 26 2021 at 15:32):
Oh I'm sure other cities have pandemics as least as nice as ours
Sebastian Reichelt (Jan 26 2021 at 19:47):
Hi to all fellow Karlsruhers! Although I haven't done enough Lean to be in any group yet, I'd love to get to know you and maybe even meet you when that becomes possible again.
Darij Grinberg (Jan 26 2021 at 21:57):
I have done even less Lean so far... (just Kevin's integer game)
Darij Grinberg (Jan 26 2021 at 21:58):
but I like to be in the loop about formalization efforts, particularly in algebraic combiantorics
I'm in Karlsruhe as well! Doing my humble BSc thesis, but with Isabelle/HOL instead of lean (I wasn't aware of lean when I started)
Sebastian Ullrich (May 30 2021 at 22:02):
Wait, who's doing Isabelle in Karlsruhe? I thought I had supplanted them!
The Institute of Theoretical Informatics, ITI at KIT :).
Sebastian Reichelt (Jun 06 2021 at 18:42):
Now that it's become reasonably safe to meet others in Karlsruhe, would any of you be interested in, say, going to a Biergarten to get to know each other?
Sebastian Ullrich (Jun 11 2021 at 15:16):
Shall we open a chat with all the :beers: people to try and find a time and location?
Johan Commelin (Jun 11 2021 at 15:36):
I'm not sure I will be able to travel from Freiburg to Karlsruhe soon. But if at some point I'm travelling up north, I'll let you know and if it fits I can make a stop in Karlsruhe.
Marc Huisinga (Jun 11 2021 at 16:17):
surely you don't want to miss out on our beautiful construction sites? :grinning_face_with_smiling_eyes:
Johan Commelin (Jun 11 2021 at 16:32):
Ooh, I'm sure the construction sites in Karslruhe can't beat the mess that is the math dept in Freiburg.
Sebastian Reichelt (Jun 11 2021 at 18:24):
Oops, I hadn't noticed the :beers:. Nice!
Given my obvious lack of Zulip skills, I may not be the best person to start a chat, but I'll try.
Last updated: Jul 29 2021 at 22:11 UTC