Zulip Chat Archive

Hallo Henrik Böving , Gruesse von Franz.Kronseder (jg 1960, TUM-Inf 1987) aus Muenchen-Moosach :)
Ich bin seit ca einem Jahr LeanProver-Fan und habe jetzt im Vor-Ruhestand viel mehr Zeit fuer sowas wie vorher on-th-job.

Ich will mich in Lean4-Programming/Proving einarbeiten und verfolge deswegen auch Dein doc-gen4 Projekt: Henrik Böving:
I just ported the doc-gen search over to doc-gen4 (https://leanprover-community.github.io/mathlib4_docs/) ...

Weil's sich im Ruhestand nach zwei Jahren Covid19-HomeOffice fachlich deutlich einsame lebt als vorher,
wuerd Ich gerne ein paar neuer persoenliche Kontakte in den ProofChecking-Communities finden.

Moosach Bahnhof https://www.openstreetmap.org/node/3986273653
Hochschule München https://www.openstreetmap.org/node/9146420825

Q: kommst Du gelegentlich auf den HM-Campus in der LothStr. dann waer mal ein Kaffee-Ratsch nett. lg Franz.Kronseder

Henrik Böving (Feb 20 2022 at 21:49):

Im Moment nicht da Semesterferien sind und ich in ein bisschen oestlich von Muenchen wohne und arbeite (ich bin dualer Student) und deswegen eine Fahrt an den Campus ca 1h fuer mich dauert :/ Aber im naechsten Semester soll es zumindest laut Plan einige Praesenz Veranstaltungen geben zu denen ich dann auf jeden Fall an den LothStr. Campus fahren werde, das waere ab Mitte Maerz.

Franz Kronseder (Feb 20 2022 at 22:05):

:) danke-fuer-antwort, eilt-ja-nicht , freu-mich-drauf , inzwischen will ich meine insights vertiefenin c++,lean3/lean4-sources , mathport, tactics , other-tools ... Gute Nacht ...

Jannis Limperg (Mar 15 2023 at 17:12):

@Jasmin Blanchette and I are now in Munich!

Henrik Böving (Mar 15 2023 at 20:22):

Oh cool! Do we wanna meet up some time?

Jannis Limperg (Mar 16 2023 at 00:19):

Yes, absolutely! I'm a bit under the weather this week, but from next week I'll hopefully be at the LMU (Oettingenstraße 67) on a daily basis.

Henrik Böving (Mar 16 2023 at 07:00):

Cool, let's talk again next week then.

Alex Keizer (Mar 17 2023 at 12:57):

I'll be visiting Munich for a few days somewhere between now and mid-April, and giving a presentation about my Msc Thesis ("Implementing a definitional (co)datatype package in Lean 4, based on quotients of polynomial functors"). @Henrik Böving you're welcome to join, too, if you want!

Henrik Böving (Mar 17 2023 at 13:16):

Oh I'd love to listen to that. Just tell me when exactly once you know.

Franz Kronseder (Mar 17 2023 at 14:34):

https://www.openstreetmap.org/node/4472669396
LMU : Library Fachbibliothek Englischer Garten, 67, Oettingenstraße
, Englischer Garten Süd, Altstadt-Lehel, Schwabing-Freimann, Munich, Bavaria, 80538, Germany

https://www.ub.tum.de/teilbibliothek-mathematik-informatik Boltzmannstrasse 3
85748 Garching :Fakultätsgebäude Mathematik & Informatik :Gebäudeteil 03

Hello Jasmin, Jannis,Alex,Henrik .. I would love to attend any of your meetings/presentations as a retired amateur listener.
rgds Franz

Alex Keizer (Apr 02 2023 at 11:29):

@Henrik Böving @Franz Kronseder My presentation will be coming Thursday (the 6th) afternoon, at LMU (Oetingenstrasse 67). @Jasmin Blanchette is in charge of booking the room; he'll have more details as to the exact time and room.

Jasmin Blanchette (Apr 03 2023 at 07:43):

14:00 in room 157.

Franz Kronseder (Apr 03 2023 at 07:48):

Hello/Hallo Alex.Keizer , I thank you for the invite ! , looking forward to meet this group coming Thursday afternoon, rgds Franz.

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib