# Leonardo de Moura on Lean, Formal Verification, and the Future of Mathematics

DevFeed: [Leonardo de Moura on Lean, Formal Verification, and the Future of Mathematics](<https://devfeed.tech/articles/creator-of-lean-handwritten-math-will-change-dramatically-leonardo-de-moura-18086.md>)

Original publisher: [Read original article](<https://www.developing.dev/p/creator-of-lean-the-end-of-handwritten>)

Author: Ryan Peterman

Published: 2026-08-10T13:03:04Z

Content type: article

Language: en

Sources: [The Developing Dev](<https://devfeed.tech/sources/the-developing-dev.md>)

Topics: [Lean](<https://devfeed.tech/topics/lean.md>), [Formal verification](<https://devfeed.tech/topics/formal-verification.md>), [math](<https://devfeed.tech/topics/math.md>), [Large Language Model](<https://devfeed.tech/topics/llm.md>)

Tags: [code](<https://devfeed.tech/tags/code.md>), [formal-verification](<https://devfeed.tech/tags/formal-verification.md>), [google](<https://devfeed.tech/tags/google.md>), [language](<https://devfeed.tech/tags/language.md>), [llms](<https://devfeed.tech/tags/llms.md>), [math](<https://devfeed.tech/tags/math.md>), [podcasts](<https://devfeed.tech/tags/podcasts.md>), [programming](<https://devfeed.tech/tags/programming.md>), [programming-language](<https://devfeed.tech/tags/programming-language.md>), [software](<https://devfeed.tech/tags/software.md>), [verification](<https://devfeed.tech/tags/verification.md>)

## AI overview

An interview with Leonardo de Moura, creator of Lean, about using the programming language for machine-checkable proofs, software verification, and mathematical reasoning. The discussion also covers how LLMs can work with Lean to generate and verify proofs.

## Source excerpt

In 2024, AlphaProof from Google Deepmind broke through in competition math achieving a silver-medal in Interational Mathematical Olympiad (IMO).