Lean community members Yaël Dillies and Paul Lezeau have published the first in a new series of blog posts about #LeanLang simprocs, or "custom simplification procedures".
The first post introduces simproc (via simp) and outlines three use cases. More practical guidance on writing simprocs to come in future posts!
Read the first post on the Leanprover-Community site here: https://leanprover-community.github.io/blog/posts/simprocs-for-the-working-mathematician/
A Lean proof of Fermat’s Last Theorem
Kevin Buzzard, Richard Taylor
May 18, 2025
https://bit.ly/43qH832
"Lean is my favorite computer game"
#LeanLang #LeanProver
https://www.youtube.com/shorts/XNWldXVJGbY
"The original motivation for (creating) Lean was software verification."
Leonardo de Moura
#LeanLang
https://www.youtube.com/shorts/yk5T-sZDPkc
Kevin Buzzard: Will Computers prove theorems?
#LeanLang #LeanProver
https://podcasts.ox.ac.uk/will-computers-prove-theorems
Leo De Moura: Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI
#LeanLang #LeanProver
https://podcasts.ox.ac.uk/formalizing-future-leans-impact-mathematics-programming-and-ai?video=1
The Department of Computer Science, University of Oxford has released recordings of the recent Strachey Series Lectures featuring Leo de Moura and Kevin Buzzard:
1️⃣ "Formalizing the Future: Lean's Impact on Mathematics, Programming, and AI" - Leo de Moura, Chief Architect of Lean
Leo discusses how Lean provides a framework for machine-checkable mathematical proofs and code verification, enabling collaboration between mathematicians, software developers, and AI systems. He also outlines the work the Lean Focused Research Organization does to expand Lean’s capabilities and support the community.
➡️ Watch Leo's lecture here: https://podcasts.ox.ac.uk/formalizing-future-leans-impact-mathematics-programming-and-ai
2️⃣ "Will Computers Prove Theorems?" with Kevin Buzzard, Professor of Mathematics, Imperial College
Kevin examines the potential for AI systems and theorem provers to assist in mathematical discovery, addressing whether computers might someday find patterns in mathematics that humans have missed, and discusses the integration of language models with formal verification systems.
➡️ Watch Kevin's lecture here: https://podcasts.ox.ac.uk/will-computers-prove-theorems
#LeanLang #LeanProver #FormalVerification #Mathematics #AI #TheoremProving #OxfordCS
The Lean FRO team met synchronously in Amsterdam last week for our annual team retreat, and to discuss upcoming work and our Year 3 roadmap! 🇳🇱✨
We had very productive discussions around Lean's future in mathematics, software and hardware verification, and AI for math. It was energizing to see our team's commitment to Lean's continued growth in each of these domains.
We're cooking up many exciting developments that will support both our mathematical community and our growing base of software verification users. Stay tuned for our full Y3 roadmap publication at the end of July!
#LeanLang #LeanProver #Lean4 #FormalVerification #Programming #Mathematics #TheoremProving
Functional Programming and Theorem Proving in Lean
#LeanLang #LeanProver
Stanford University
https://bit.ly/4deed6J
Learning Lean in the Age of Artificial Intelligence
#LeanLang
Three talks at the recent #ZKProof 7 conference in Sofia caught our attention:
🔹 Alexander Hicks from Ethereum Foundation had some really nice things to say about #LeanLang, calling it "quite a nice functional programming language". 😍 He showed off zkLib, which ties executable implementations of proof systems directly to security proofs.
https://www.youtube.com/live/L_uz5rH50Sw
🔹 James Parker from Galois introduced zkLean - a DSL for specifying ZK statements in Lean. Definitely worth checking out if you're interested in this space!
https://www.youtube.com/live/O_bT89JK6_c
🔹 Jonathan Rouach from QEDIT discussed the motivation behind the development of a Lean end-to-end proof of the PLONK verifier.
https://www.youtube.com/live/dNLa5B2ER74
Feline, a cat clone in Lean
#LeanLang
https://github.com/adolfont/learning-lean/tree/main/fpinlean/2.4.cat/feline
Introducing clean, a formal verification DSL for zk circuits in Lean4
#LeanLang https://blog.zksecurity.xyz/posts/clean/
Learning Lean
#LeanLang
https://github.com/adolfont/learning-lean
Will you be in Oxford on May 6?
You can attend Leonardo de Moura's lecture on Lean!
#LeanLang #LeanProver #Lean4
Verified Collaboration: How the Lean Project is Transforming Mathematics, Programming, and AI
Leonardo de Moura
#LeanLang
https://bit.ly/4hNDfKq
We were super excited to hear from 14-year-old Daniel Carpenter, enthusiastic #LeanLang user and Spanish IMO team qualifier, a few weeks ago in the run up to the Exporecerca Jove Science Fair in Barcelona. Daniel's project, "Putting the Computer to the Test in the Mathematical Olympiad", which formalizes Catalan Math Olympiad problems in Lean had been accepted to the fair and he reached out to let us know!
In a happy coincidence, Lean FRO research engineer Anne Baanen happens to live in Barcelona and was able to meet with Daniel in person at the Exporecerca. They had a great conversation about Lean and Daniel's
future plans for formalization projects.
The Royal Society for Sciences and Arts in Barcelona also recognized Daniel's project with an award - so huge congrats from all of us at @leanprover to Daniel!
Would creating a podcast focused on the Lean programming language and proof assistant be a meaningful or viable idea?
#LeanLang
📣 #LeanLang version 4.17 has been released! This release includes 168 feature additions and 57 fixes to the core language! This also includes a first draft of the new try? tactic!
➡️ 𝗥𝗲𝗮𝗱 𝘁𝗵𝗲 𝗳𝘂𝗹𝗹 𝗿𝗲𝗹𝗲𝗮𝘀𝗲 𝗻𝗼𝘁𝗲𝘀 𝗵𝗲𝗿𝗲: https://github.com/leanprover/lean4/releases/tag/v4.17.0
