Informal introduction to formal proofs in Lean 4

par Dr Mykola Iorgov (Bogolyubov Institute for Theoretical Physics, Kyiv, Ukraine)

mardi 20 oct. 2026, 11:00 → 12:00 Europe/Paris

Salle 1180, bâtiment E2 (Salle des séminaires )

I will give an introduction to Lean 4, a modern functional programming language with a powerful type system. One of its key features is the ability to state mathematical claims and write their proofs in Lean itself. This approach is based on the idea of “programs as proofs” (the Curry–Howard correspondence): a mathematical statement is treated as a type, and its proof as an element of that type. So when Lean checks a program, it is in effect verifying the correctness of the corresponding mathematical proof. If the code is accepted by Lean's kernel, we obtain a formally verified mathematical proof. This approach is especially significant in modern research involving large language models. LLMs can generate mathematical proofs, and writing a proof in Lean makes it possible to formally verify that it is correct.