The paper "The Lean theorem prover (system description)", published in the CADE-25 proceedings in 2015, is recognized for "being the first description of the Lean theorem prover, which meanwhile has made spectacular progress and has a tremendous impact in interactive and automated reasoning, with numerous applications, in particular to formalized mathematics and software verification", as can be read in the official laudation. The paper describes the (then) new proof assistant Lean, that over the last 10 years has grown to become the most prominent proof assistant for formalized mathematics, and which has made the possibility of formalization more widely known among mathematicians. Notable formalization projects that have been formalized in Lean since then are the Liquid Tensor Experiment and the Sphere Eversion project, and there are ongoing projects including the Carleson project and the Fermat's Last Theorem project.
The authors of the paper are Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer, which at that time were the only developers and users of Lean. Since then, Lean has been developed much further from a prototype to a performant proof assistant and programming language with 20 developers, and includes a large mathematical library with over 500 contributors.
Floris van Doorn received his PhD in 2018 at Carnegie Mellon University under the supervision of Jeremy Avigad and Steve Awodey. He then worked as a postdoc at the mathematics department of the University of Pittsburgh with Tom Hales and at the mathematics department of the University of Paris-Saclay with Patrick Massot. Since 2023, he has been a professor at the Mathematical Institute of the University of Bonn and research leader of the new Interdisciplinary Research Unit (IRU) "Formalized mathematics and computer-assisted proofs". This IRU wants to formalize brand-new research results, develop new computational tools and contribute to libraries for the rigorous formalization of mathematics and will serve as a bridge between the departments of mathematics and computer science.