Das Paper „The Lean theorem prover (system description)“, das 2015 in den CADE-25 Proceedings veröffentlicht wurde, wird dafür gewürdigt, dass es „die erste Beschreibung des Lean Beweisassistenten ist, der inzwischen spektakuläre Fortschritte gemacht hat und einen enormen Einfluss auf interaktives und automatisiertes Beweisen hat, mit zahlreichen Anwendungen, insbesondere in der formalisierten Mathematik und der Software-Verifikation“, wie es in der (übersetzten) offiziellen Laudatio heißt. Das Paper beschreibt den (damals) neuen Beweisassistenten Lean, der sich in den letzten 10 Jahren zum bekanntesten Beweisassistenten für formalisierte Mathematik entwickelt hat und die Möglichkeit der Formalisierung unter Mathematiker*innen bekannter gemacht hat. Bemerkenswerte Formalisierungsprojekte, die seither in Lean realisiert wurden, sind das Liquid Tensor Experiment und das Sphere Eversion project. Zahlreiche Projekte wie das Carleson project und das Fermat's Last Theorem project laufen derzeit auf Hochtouren.
Die Autoren des Papiers sind Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn und Jakob von Raumer, die zu diesem Zeitpunkt die einzigen Entwickler und Benutzer von Lean waren. Seitdem hat sich Lean von einem Prototypen zu einem leistungsfähigen Beweisassistenten und einer Programmiersprache mit 20 Entwickler*innen weiterentwickelt und umfasst eine große mathematische Blbliothek mit über 500 Mitwirkenden.
Floris van Doorn promovierte 2018 an der Carnegie Mellon University unter der Leitung von Jeremy Avigad und Steve Awodey. Anschließend arbeitete er als Postdoktorand am Fachbereich Mathematik der University of Pittsburgh bei Tom Haless und am Fachbereich Mathematik der Universität Paris-Saclay bei Patrick Massot. Seit 2023 ist er Professor am Mathematischen Institut der Universität Bonn und Leiter der neuen Interdisciplinary Research Unit (IRU) "Formalized mathematics and computer-assisted proofs". Diese IRU will brandneue Forschungsergebnisse formalisieren, neue computergestützte Werkzeuge entwickeln und zu Bibliotheken für die rigorose Formalisierung der Mathematik beitragen. Sie dient als Brücke zwischen den Fachbereichen Mathematik und Informatik.