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 :)

[Klaus Wiegmann]

I'm also here in Saarbrücken, from the Universität des Saarlandes, following @Laurent Bartholdi 's proseminar course :+1:

[Shreyas Srinivas]

Welcome to SB. We should have a lean meetup beyond the proseminar sometime.

[Simon Kirchner]

I'm here in Saarbrücken (Universität des Saarlandes), following @Laurent Bartholdi 's seminar this year.

[Philipp Radder]

Hi, I am following @Laurent Bartholdi 's Seminar as well at Saarland University

[Sebastian Volz]

Hello everyone! I am also following @Laurent Bartholdi 's Seminar at Saarland University.

[Oliver lang]

im following @Laurent Bartholdi s lean course at saarland university

[Bashar Hamade]

Hello everyone,I'm taking @Laurent Bartholdi's seminar "Computer-assisted proofs in Lean" at Saarland University

[Kevin Buzzard]

You guys should find a project to work on together :-)

[Shreyas Srinivas]

We should have some kind of a monthly lean meeting here with interesting talks, beyond the seminar.

[Shreyas Srinivas]

There's already a rust saar group. There could be a lean saar group too

[Bashar Hamade]

Kevin Buzzard said:

You guys should find a project to work on together :-)

That sounds great!
most of us in the seminar right now though are complete lean beginners,and mainly we are computer science bachelor students who haven't dived very deeply into the world of formal proofs , computational logic...
But this seminar (and our Computational Logic course ) seems like a perfect launching pad for one to go deeper into these topics,so hopefully we could work on some good projects as the time progresses :).

[Yun-Jhu]

Hi, I am also following @Laurent Bartholdi 's prosemanir at Saarland University.

[Maximan]

Hey guys, I too am following @Laurent Bartholdi 's prosemanir at Saarland University.

[Min Htut Win]

Hello, I am following @Laurent Bartholdi 's seminar at Saarland University.

[Julian Blaes]

Hi! I'm also in @Laurent Bartholdi 's seminar :-)

[Fabian Brenner]

Hey, I too am attending @Laurent Bartholdi 's seminar at Saarland Univerity.

[FabioR]

Hey guys, I also am following @Laurent Bartholdi 's prosemanir at Saarland University.

[Kasun Gallage]

Hi all, I am also following professor @Laurent Bartholdi 's seminar of "Computer-Assisted Proofs" at Saarland University.

[Shreyas Srinivas]

Hello :wave: and welcome. What topics are up for presentation this semester?

[Anshul Birwal]

Hi all, I am also following @Laurent Bartholdi 's proseminar in Computer Assisted proof's using Lean. We will be focusing on inverse semigroups this time.

[Atharva Kore]

Hello, I am student of @Laurent Bartholdi 's proseminar in Computer Assisted proof's using Lean. The journey would be interesting.

[Kris]

G'Day everyone

[Sude Ergün]

Hey, I am also attending @Laurent Bartholdi 's seminar about Lean at Saarland University.

[Audric CK]

hello, im also attending @Laurent Bartholdi seminar.

[Nicolas Löw]

Hello, i also attend @Laurent Bartholdi's seminar at Saarland University.

[Harald Neumann]

Hi, I'm attending @Laurent Bartholdi's seminar.

[Mahmoud Alali]

Hi, I'm attending @Laurent Bartholdi's seminar

[Robert]

Also attending @Laurent Bartholdi 's course!

[Joachim Breitner]

Just curious: Is “saying hi on Zulip” part of the first exercise sheet? :-)

[Shreyas Srinivas]

Maybe...