Leonardo de Moura: "Lean 4: Empowering the Formal Mathematics Revolution and Beyond"

Topos Institute Colloquium, 7th of September 2023.
---
This talk presents Lean 4, the latest version of the Lean proof assistant, and its impact on the mathematical community. We first introduce the project's design and objectives, followed by the mission of the newly established Lean Focused Research Organization (FRO).
The advent of Lean and similar proof assistants has sparked a transformation in mathematical practice, an era we refer to as the "Formal Mathematics Revolution". We'll explore how Lean 4 contributes to this revolution, with its tools and structures enabling mathematicians to formalize complex theories and proofs with unprecedented ease. A key aspect of our philosophy is facilitating decentralized innovation. We discuss the strategies employed to empower a diverse community of researchers, developers, and enthusiasts to contribute to formalized mathematics.
We will also delve into the usage of Lean as a functional programming language. With Lean 4, we have not only created an environment for formalizing mathematics but also an effective tool for writing software, enabling a smooth interaction between mathematical and computational aspects. Finally, we will look ahead, sharing our vision and planned steps for the future of Lean 4 and the Lean FRO. We'll discuss how we aim to further grow the user base, continue improving usability, and deepen the reach of formal methods into mathematics and computer science.

[@tarikozkanli788]

Lean4 is now a depedently typed Scheme

[@9s-l-s9]

In what way?

[@tarikozkanli788]

Because of the hygenic macros

[@replikvltyoutube3727]

can you show some examples comparing two?

[@9s-l-s9]

@@tarikozkanli788 Hmm. But just because its macro system is inspired by scheme? I mean is it not closer in everything else to the ml languages? :)

[@tarikozkanli788]

@@9s-l-s9 yes agree.