Seminar: Introduction to the Lean 4 theorem prover and programming language by Leonardo de Moura

Lean 4 is an implementation of the Lean interactive theorem prover (ITP) in Lean itself. It addresses many shortcomings of the previous versions and contains many new features. Lean 4 is fully extensible: users can modify and extend the parser, elaborator, tactics, decision procedures, pretty printer, and code generator. The new system has a hygienic macro system custom-built for ITPs. It contains a new typeclass resolution procedure based on tabled resolution, addressing significant performance problems reported by the growing user base. Lean 4 is also an efficient functional programming language based on a novel programming paradigm called functional but in-place. Efficient code generation is crucial for Lean users because many write custom-proof automation procedures in Lean itself. In this tutorial, we introduce the Lean theorem prover with examples and describe some of its applications.

[@bernardoborges8598]

Great video! Very well explained and motivated!

[@LoveTalesBook]

Hi bro I want to learn Move programming language Where to start and which is the beginner video to watch in your videos