Gothenburg, Sweden

Stream: Geographic locality

[Victor Ahlquist]

Studying for a B.sc in maths at the University of Gothenburg. Trying to learn Lean in my spare time, hopefully I'll be good enough to contribute to mathlib in time.

[Jannis Limperg]

Hej! If you're interested in type theory more broadly, check out the Initial Types Club at Chalmers. It's a weekly-ish undergrad-friendly seminar on type theory and adjacent topics (or at least it was when I was there).

[Victor Ahlquist]

Thanks for the link. Unfortunately I'm more interested in the mathematical side of Lean rather than the type-theoretic, but I might check it out in the future if my tastes have changed :)

[Jannis Limperg]

I'll allow it. But be aware that this is all an elaborate scheme for generating type theory PhDs. :octopus:

[Kevin Buzzard]

It's supposed to be an elaborate scheme for getting mathematicians interested in theorem provers!

[Mario Carneiro]

Starting today, I am now officially starting my new postdoc at Chalmers University under Magnus Myreen, after finishing my postdoc at CMU under Jeremy Avigad. I don't have any specific projects I've come here to do, but expect some Lean/CakeML crossovers soon!

[Shreyas Srinivas]

Nice!! Will we see a deep embedding of cake ML in lean soon?

[Mario Carneiro]

actually yes, that's one of the near term projects we talked about today, Magnus was already planning on doing something like that for Coq and doing it for lean instead or in addition should be not hard

[Shreyas Srinivas]

Is the plan to implement the proof producing front end alone? I toyed with the idea during my vacation and put it aside because I didn't know how to represent non-terminating programs

[Shreyas Srinivas]

(deleted)

[Mario Carneiro]

not proofs, just the semantics of CakeML

[Mario Carneiro]

the idea is so that you can prove the correctness of CakeML programs in lean

[Mario Carneiro]

so kinda like using VST and then trusting CompCert

[David Thrane Christiansen]

@Mario Carneiro You're not that far away - if you ever pass through CPH, drop me a line

[Rishi Sreedhar]

Heyy I've been curious about LEAN for some time now and was wondering if there is an active LEAN community in Gothenburg. If so, please DM? Thank you!

[Mario Carneiro]

Well there is me, and a small community of others at Chalmers who have done some stuff with lean and/or took my lean class last year, but we don't have regular meetings or anything like that. But I'm happy to reach out and maybe get something going

[Yaël Dillies]

I'm in Stockholm, so not exactly nextdoor, but I could come on some occasions

[Rishi Sreedhar]

Hi Mario, Yaël, thank you for your responses! I often work from the Chalmers Library. Would you like to meet for a fika sometime?

[Mario Carneiro]

the logic and types group has group lunches almost every day, I'll DM you details around noon and you can drop by

[Mario Carneiro]

Reid Barton is also starting here as of last week