Karlsruhe, DE

Stream: Geographic locality

[Marc Huisinga]

@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]

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]

But what is the idea of this stream?

[Kevin Buzzard]

To enable people who are geographically close and share common interests to find each other?

[Shekhinah Memmel]

I'm from Hadiko.

[Shekhinah Memmel]

I'm from Hadiko.

[Darij Grinberg]

first time I'm seeing a Karlsruhe group in a math community. hi from Waldstadt

[Johan Commelin]

Karlsruhe is super critical for Lean's existence (-;

[Darij Grinberg]

just by numbers or is there a working group at the KIT?

[Johan Commelin]

One of the two core developers is at KIT

[Johan Commelin]

so, maybe not by numbers, but if you do a weighted count, then....

[Sebastian Ullrich]

@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]

ah, a nontrivial group :)

[Darij Grinberg]

i have no KIT connection (i "work" in Philadelphia); i'm just here for the pandemic

[Sebastian Ullrich]

Oh I'm sure other cities have pandemics as least as nice as ours

[Sebastian Reichelt]

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]

I have done even less Lean so far... (just Kevin's integer game)

[Darij Grinberg]

but I like to be in the loop about formalization efforts, particularly in algebraic combiantorics

[Max]

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]

Wait, who's doing Isabelle in Karlsruhe? I thought I had supplanted them!

[Max]

The Institute of Theoretical Informatics, ITI at KIT :).

[Sebastian Reichelt]

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]

Shall we open a chat with all the :beers: people to try and find a time and location?

[Johan Commelin]

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]

surely you don't want to miss out on our beautiful construction sites? :grinning_face_with_smiling_eyes:

[Johan Commelin]

Ooh, I'm sure the construction sites in Karslruhe can't beat the mess that is the math dept in Freiburg.

[Sebastian Reichelt]

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.

[Christian Pehle]

if there is another meet-up in Karlsruhe at some point, I might make it as well :)

[Sebastian Ullrich]

Yeah, we should do another one some time. And bully @Johan Commelin into attending as well :) .

[Sebastian Reichelt]

Was thinking about this as well. Hopefully the beginning of the semester is not too packed with other obligations?

[Sebastian Ullrich]

Nah, we have student TAs for that

[Sebastian Reichelt]

I've created a doodle with the dates where I'm personally available: https://doodle.com/poll/9pi223m8wxf3bqmt?utm_source=poll&utm_medium=link
I suggest we continue in the private stream again, and invite everyone who participated in the doodle.
Looking forward to seeing you again, and hopefully also Johan, Christian, and Jakob, who couldn't make it last time.

[Sebastian Reichelt]

I'll continue here instead as I don't have the Zulip name of everyone in the Doodle. Let's meet on Wednesday, October 27, as that seems to be ok for everyone so far.
Shall I reserve a table at Oxford again? (Inside this time...)

[Johan Commelin]

Unfortunately I can't make it this time either

[Sebastian Ullrich]

@Sebastian Reichelt I'm open to other locations, but otherwise I'd say: go ahead!

[Sebastian Reichelt]

The reservation has just been confirmed: October 27, 7 pm at Oxford Ost.

[Markus Himmel]

My employer is offering an MSc thesis in industry, partly supervised by me, about using Lean to verify a piece of real-world software: https://www.cas-mitgestalter.de/jobs/abschlussarbeit-informatik-formale-verifikation/

[Alex J. Best]

You could post this in #job postings too

[Markus Himmel]

I considered this, but since the offer is limited to German-speaking students who are willing to live in Karlsruhe for the duration of the thesis, I think it makes more sense here.

[Johan Commelin]

I think you should just point out that condition, but cross-post nonetheless. Not sure all German-speaking-students-willing-to-live-in-Karlsruhe follow this thread.

[Markus Himmel]

Fair enough. I'll cross-post.

[Sebastian Reichelt]

As @Sebastian Ullrich already mentioned in the Freiburg thread, a new instance of K∀-B∃∃R is overdue. The weather report for next week looks all right, so here is a doodle: https://doodle.com/meeting/participate/id/dNkRl1ze

[Henrik Böving]

(question from the uninitiated, what is K∀-B∃∃R?)

[Sebastian Reichelt]

Just an informal Lean meeting in Karlsruhe, which happened twice last year at Oxford Ost.

[Sebastian Reichelt]

Looks like there are a lot of possible dates, so let's just pick Tuesday May 10.
Shall we try another location this time? Unless more people join, we are pretty flexible, it should just be somewhere with a reasonably quiet area outside, preferably with good food. If we're looking for something in Oststadt again, maybe Henderson's? Hoepfner is nice, too, but (a few years ago) I wasn't too happy with the food served in their Biergarten. Alter Schlachthof would be a good option but is closed on Mondays and Tuesdays now, so we'd just have to pick Wednesday then. Or just Oxford again? Any preferences?

[Sebastian Ullrich]

Hmm, looks like we may as well choose my office given the audience... :) . But Henderson's sounds good to me, even without Campus-Ale.

[Markus Himmel]

Unfortunately I missed the doodle and would love to join but I don't have time on Tuesdays. @Sebastian Reichelt, since you mentioned that there were other good dates, maybe one of them is on a different weekday?

[Sebastian Ullrich]

Let's notify some previous participants as well @Jakob von Raumer @Max Nowak @Sebastian Graf @Max Wagner

[Max Nowak]

I forgot to submit the doodle, whoops. I'm 60% likely to show up, sadly have a lot of stuff going on :(.

[Sebastian Reichelt]

I didn't quite realize that picking a date closed the poll. @Markus Himmel, @Max Nowak, I've reopened it.
Currently, Tuesday and Wednesday next week or the week after are all equally good.

[Sebastian Reichelt]

So Wednesday, May 11 it is.

[Jakob von Raumer]

I'm in, rather later than early in the evening, as soon as viva celebrations of a friend of mine end

[Sebastian Ullrich]

@Sebastian Graf will likely join us as well

[Sebastian Ullrich]

We should probably make a reservation soon, if we're not already too late :)

[Sebastian Reichelt]

Cool, but looks like we need a bit more space.
On the website of Henderson's, it said that reservations are possible only during opening hours, so I couldn't book anything on Sunday or yesterday but will call them as soon as they open today.

[Sebastian Reichelt]

I've reserved a table at Henderson's tomorrow at 7 pm, outside. Looking forward to seeing you all.

[Sebastian Ullrich]

After the pleasant hackathon in Freiburg, @Jakob von Raumer and I thought we should reciprocate and invite people (from anywhere) to a day of hacking and general Leaning at KIT. I assume Fridays are good for people that need to travel back the same day, and also our seminar room is still available on the following days:

[Sebastian Ullrich]

/poll When would you prefer to attend a Lean hackathon?
Fri Mar 10
Fri Mar 17
Fri Mar 24

[Sebastian Ullrich]

@Johan Commelin @Joachim Breitner @Reid Barton @Tomas Skrivan (if still nearby!)

[Sebastian Ullrich]

Students are welcome as well of course!

[Johan Commelin]

Unfortunately I'm blocked on all these Fridays :scream: :see_no_evil:
The week of 13-17, Reid and I are giving a lecture course, and the 10th there are preliminary lectures. On 24, there is a seminar in Strasbourg...

[Sebastian Ullrich]

Oops... Thursday would be the one other day where the room is still fully available

[Johan Commelin]

Sorry! Strasbourg is on Thu 23!

[Sebastian Ullrich]

Then I guess we already have a favorite date :)

[Reid Barton]

The morning of the 24th I pick up my Aufenthaltstitel (at last...)

[Reid Barton]

But if we leave at 10 or so, it should work.

[Reid Barton]

I think Tomas is already in Pittsburgh.

[Joachim Breitner]

I don’t see the poll anymore. So March 24th is left? That day is unclear here, we have vague plans to travel that weekend.

[Henrik Böving]

image.png
THis is the poll

[Sebastian Ullrich]

Btw, I changed the poll title from "prefer" to "available". This thing is incredibly buggy. I hope people can still see the poll?

[Henrik Böving]

I can see it

[Henrik Böving]

Sebastian Ullrich said:

/poll When would you prefer to attend a Lean hackathon?
Fri Mar 10
Fri Mar 17
Fri Mar 24

so looking at the poll now will it be this Friday? Just asking so I know if I need to keep that date free^^

[Johan Commelin]

Hmm, Reid and I had scheduled 24th already.

[Sebastian Ullrich]

I'm also not sure yet whether I can make it this week, so the 24th would probably be safer. Looks like we'll just have to repeat this in a few months to gather more people.

[Joachim Breitner]

So March 24th is left? That day is unclear here, we have vague plans to travel that weekend.

The travel plans have concretized, and I won’t be able to come. Next time!

[Johan Commelin]

Enjoy your other trip!

[Sebastian Ullrich]

We have booked Room 010 in Building 50.34 for the entire Friday. From the main station, you can take the tram to Durlacher Tor / KIT-Campus Süd, then walk another ~7min. When you enter the building (using the left entrance when viewed from the street), continue straight on through the door with a drawing of the ISS (ignore the scary German signage in red) until you see the sign for 010 on the left-hand side; you have to cross the little kitchen to get to the door.

[Markus Himmel]

What time does it start?

[Sebastian Ullrich]

It sounds like the Freiburg group will not arrive before ~11:30, but Jakob and I will certainly be around from 10:00 on at the latest

[Max Nowak 🐉]

@Markus Himmel we are going to Oxford OST :) join us there