Strasbourg, France

Stream: Geographic locality

[Pierre Guillot]

Hi everyone! I'm just getting started with Lean, still in the process of reading docs and tutorials. I'd be interested to know if there are people in my area with an interest in formalizing maths. (Well, there are people in Paris and Lyon for sure!)

Pierre

[Johan Commelin]

Across the border, there's Karlsruhe and Freiburg. I'm not aware of other Lean users in Alsace at the moment.

[Patrick Massot]

Bienvenue !

[Marc Huisinga]

See also the Karlsruhe thread :)

[Filippo A. E. Nuccio]

Hi Pierre, bienvenu!

[Xavier Roblot]

Bonjour !

[Adam Topaz]

Hi @Pierre Guillot !

[Pierre Guillot]

Hi Adam! it's been a while hasn't it? how are you?

[Adam Topaz]

I'm well, and you? What got you interested in lean?

[Pierre Guillot]

I'm doing great, and my life has changed entirely: I have a 2-year-old daughter :-)

Where do you live now?

I got interested in Lean very gradually. For one thing I've loved coding for a while (starting with assembly when I was a teenager!), and in recent years I've been using Sage very frequently. Then I learned some Haskell just for kicks. Then I had some discussions with a CS friend here and we had this attempt at teaching some Coq to our students-- well, it was Edukera, some graphical interface over Coq, and it was disappointing in almost all respects, but whatever. (I'm speaking in the past but I'll have to teach it again in the fall.) Then Voevodsky created some buzz over HoTT.

And then eventually I became aware, reading Quanta I think, that Lean was already being used by a lot of mathematicians, I discovered that it had plenty of documentation (unlike Coq or Isabelle, if you mean "documentation for mathematicians"), I started digging a little... I also spoke with Filippo Nuccio, that I've known for a number of years. It helps talking to someone you know, who's crossed the rubicon and moved to formalized maths (I didn't know you were part of the adventure, although Filippo quickly told me).

Now I'm learning! It doesn't seem too difficult in itself, but some aspects are tricky to me -- I'm hoping that what I find relatively easy is the important stuff and what I find hard is anecdotal, but time will tell! Generally I just find it confusing to jump inside a very large project on which tons of other people have thought hard for a while. (And I haven't got to the point where I need to use GIT, which I know already puzzles me completely.)