Saarbrücken, DE

Stream: Geographic locality

[Laurent Bartholdi]

and currently visiting Berkeley CA, USA

[Laurent Bartholdi]

With @Cedric Holle and @Cuma Kökmen and @Roberto Alvarez and Simon

[Cedric Holle]

test123

[Cedric Holle]

works :D

[Cuma Kökmen]

hi

[Cuma Kökmen]

found it :D

[Simon Christoffel]

Hi

[Aaron Bies]

:wave:

[Alex Rogovskyy]

:wave:

[Roberto Alvarez]

@Laurent Bartholdi @Cedric Holle @Alex Rogovskyy I've made a discord server to better organize the seminar, let me know if you'd prefer another platform

[Arthur Correnson]

Hi

[Leon Pernak]

In Saarbrücken too :-)

[Bernhard Reinke]

hello

[Shreyas Srinivas]

Hi, I too am in Saarbrucken. Currently pursuing a PhD in computer science. I stumbled across lean a year ago and am excited to learn all the ways in which mathematics and more importantly, theoretical computer science can be expressed, taught,
and learned with lean as a prover.

[Aaron Bies]

Just found out there is a course on Lean next semester :eyes:
"Formalizing mathematics in LEAN" by Laurent Bartholdi

[Kevin Buzzard]

Oh nice! I love that there are formalising maths courses popping up here there and everywhere!

[Shreyas Srinivas]

Yep, I am planning to attend these sessions tomorrow

[Shreyas Srinivas]

Here in Saarbrucken, because of the very large CS contingent, there is a reasonable population of theorem prover users (and developers)

[Kevin Buzzard]

All over the world there are people running courses which use theorem provers in computer science departments. What I'm excited about is seeing them in mathematics departments, because 5 years ago I knew of 0 examples anywhere.

[Shreyas Srinivas]

Kevin Buzzard said:

All over the world there are people running courses which use theorem provers in computer science departments. What I'm excited about is seeing them in mathematics departments, because 5 years ago I knew of 0 examples anywhere.

Ah I see. As far as I know, Laurent is (also?) part of the CS dept here (source:https://saarland-informatics-campus.de/forschung-research/dozenten/). Even within CS and within formal methods, theorem proving is limited to a few niches, mostly Programming languages and Cyrptographic protocols

[Kevin Buzzard]

Theorem proving is kind of important throughout mathematics though ;-)

[Emilie (Shad Amethyst)]

I'm here in Saarbrücken this semester, following @Laurent Bartholdi's course :)