Zulip Chat Archive

Stream: general

Topic: propaganda

Patrick Massot (Apr 05 2018 at 20:39):

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 (Apr 05 2018 at 20:39):

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

Johannes Hölzl (Apr 08 2018 at 19:21):

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 (Apr 08 2018 at 20:24):

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.

Last updated: Dec 20 2023 at 11:08 UTC