Gaëtan Serré

Stream: new members

[Gaëtan Serré]

Hi everyone,
I am a PhD candidate at the École Normale Supérieure of Paris-Saclay. I will start my PhD in applied mathematics (in the Centre Borelli lab) in October. I work on stochastic methods for global optimization and sampling methods. I am currently trying to adapt proofs I wrote concerning the convergence of a such method in Lean 4 (and Mathlib obviously). I was introduced to Lean by @Patrick Massot 5 years ago in a course, and I'm starting to get back into it. I'm looking forward to being part of the Lean community, as I find very important the problem of formalization and reproducibility of mathematical proofs.
By the way, is there a tool to render Lean 4 projects in HTML (as format-lean)? Thank you very much!

[Riccardo Brasca]

Bienvenu !

[Yaël Dillies]

Salut !

[Anatole Dedecker]

Salut !

[Patrick Massot]

Oh, that was the very first year I used Lean for teaching! I'm really happy to read you are still interested in Lean after attending that very experimental course. Since then it became a much more polished and much easier course.

[Patrick Massot]

format_lean itself has not been ported to Lean 4 but there is LeanInk with slightly overlapping goals, and there will be informal Lean at some point (see https://www.youtube.com/watch?v=tp_h3vzkObo).

[Gaëtan Serré]

Patrick Massot said:

Oh, that was the very first year I used Lean for teaching! I'm really happy to read you are still interested in Lean after attending that very experimental course. Since then it became a much more polished and much easier course.

It was a hard course but one of the most interesting one! I am glad it became better

[Gaëtan Serré]

Patrick Massot said:

format_lean itself has not been ported to Lean 4 but there is LeanInk with slightly overlapping goals, and there will be informal Lean at some point (see https://www.youtube.com/watch?v=tp_h3vzkObo).

The lake build dir.file:print_proofs command is exactly what I am looking for! This is not available yet?