3 juillet 2026 à 14h30
Rémy Degenne, Chercheur de l’équipe SCOOL
Titre : Proving theorems with Lean and Artificial Intelligence
Abstract:
AI agents can now write mathematics, but we can’t trust them yet. Subtle errors might be hidden deep in the reasoning steps, and rigorously checking the proofs manually takes a lot of time and expertise. The Lean theorem prover provides a way to write formal, machine-checkable proofs, giving us high confidence in their correctness. AI systems have managed to reach gold medal level at the International Mathematical Olympiad while producing Lean-checked proofs. Could we get them to write research-level, verified mathematics? I will introduce Lean and its mathematical library Mathlib, and explain how they can be used to write trusted proofs, in particular machine learning theory proofs. I will also present recent advances in AI-assisted formalization.
Inria, Amphi du bâtiment B
français
English