propaganda

Stream: general

[Patrick Massot]

Today I attended a talk by Warwick Tucker, the Lorenz attractor guy. I told him about Lean and he seemed to be very interested (he does computer assisted proofs and would like to use proof assistants)

[Patrick Massot]

@Sebastien Gouezel: recently I also got Samuel Lelièvre very interested in trying Lean

[Johannes Hölzl]

Fabian Immler (who formalized a lot of theory of differential equations in Isabelle/HOL) was last year in Sweden and worked together with Warwik. Fabian's PhD thesis was to implement most of the computational part (and its correctness) of the Lorenz attractor proof in Isabelle. The next step is to work on the analysis part.

[Patrick Massot]

Yep, Warwick mentioned this. But he was not aware of the existence of Lean, and he seemed very interested, especially by the fact that it has some documentation targeting mathematicians (TPIL) and a more friendly interface than Coq.