Lean FRO

"I think the other thing that's got real potential is moving away from using English as the main language that you communicate with... There are people who have used mathematical language, Lean is the sort of... mathematical language that allows for processing of mathematical proofs. I think there's some real potential in that because what Lean has that English doesn't is precision." Mathematician and broadcaster Hannah Fry shared this when New Scientist asked her about AI approaches that go beyond transformer-based models. Hannah Fry's full conversation with New Scientist is linked below. 📺️ Interview: https://lnkd.in/gwywpZsA ➡️ See the Lean Y3 roadmap: https://lnkd.in/geUJXM_K #LeanLang #LeanProver #Mathematics #AI

I had a great time (virtually) visiting Topos Institute today. Watch my talk: Autoformalization and the Future of Mathematics and Science (how far will we go? how fast?) https://lnkd.in/evCNtnaa

𝐋𝐞𝐚𝐧 𝟒.𝟐𝟖.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! This release brings module system fixes, performance improvements in 𝚋𝚟_𝚍𝚎𝚌𝚒𝚍𝚎, and continued expansion of 𝚐𝚛𝚒𝚗𝚍 annotations across the standard library. Notable improvements include: 🤖 New lightweight symbolic simulation framework integrating with 𝚐𝚛𝚒𝚗𝚍, enabling verification condition generators and symbolic execution engines 🎛️ User-defined 𝚐𝚛𝚒𝚗𝚍 attributes useful for implementing tactics using the 𝚐𝚛𝚒𝚗𝚍 infrastructure 🔧 New 𝚜𝚘𝚕𝚟𝚎𝚛𝙼𝚘𝚍𝚎 field in 𝚋𝚟_𝚍𝚎𝚌𝚒𝚍𝚎 to configure the SAT solver for proof search, counterexample search, or default behavior 🔍 lean4checker available out-of-the-box as 𝚕𝚎𝚊𝚗𝚌𝚑𝚎𝚌𝚔𝚎𝚛 via elan 𝐅𝐮𝐥𝐥 𝐫𝐞𝐥𝐞𝐚𝐬𝐞 𝐧𝐨𝐭𝐞𝐬: https://lnkd.in/gW48gpq3 #LeanLang #LeanProver #ProofAssistant #OpenSource #FormalVerification

Lovely sharing the mission of Axiom with Valérie Pécresse, President of the Île-de-France region, and Amaury Hayat, AI for math researcher extraordinaire. The future of AI should be built on an incomparable mathematical foundation, something like the French rigor of Bourbaki and the genius of Grothendieck to the lasting influence of Andre Weil and Jean-Pierre Serre. We discussed the intersection of AI and Mathematics, and the critical role of formalization in the pursuit of truth. As we look to the future, tools like Lean FRO are bridging that storied history with the future of automated formalized and verified reasoning. 🇫🇷

Remarkable work from the RoboSurge team at TreeHacks 2026 🎉 2nd place overall out of 378 submissions at the largest collegiate hackathon, and tucked into their technical stack: we were super excited to see 𝐟𝐨𝐫𝐦𝐚𝐥𝐥𝐲 𝐯𝐞𝐫𝐢𝐟𝐢𝐞𝐝 𝐭𝐫𝐚𝐣𝐞𝐜𝐭𝐨𝐫𝐢𝐞𝐬 𝐮𝐬𝐢𝐧𝐠 𝐋𝐞𝐚𝐧'𝐬 𝐝𝐞𝐩𝐞𝐧𝐝𝐞𝐧𝐭 𝐭𝐲𝐩𝐞 𝐭𝐡𝐞𝐨𝐫𝐲, with, as the team describes it, "NO AI". And all this in only 36-hours! Congratulations to Justin Peng and the rest of the team! #LeanLang #LeanProver #TreeHacks #FormalVerification

There is a quiet revolution happening in math, driven by computing and AI: If you open an advanced math textbook, you will encounter a wall of symbols and a dry definition/theorem/proof presentation. To fully understand such a book requires years of background in number theory, abstract algebra, group theory, etc. By contrast, if you read a book on a new programming language, such as Rust, you can probably write simple programs in an afternoon without the need to learn predicate logic, automata theory, complexity, etc. What if it was possible to do advanced math as easily as a programming? One reason math is harder to learn that programming is the bottom-up presentation, where many prerequisite theorems and proofs are needed before getting to the main topic.  Mathematicians will argue this is simply the nature of the subject and is necessary to ensure rigor and accuracy.  However, this is slowly changing due to the use of automated proof assistants. Programming languages, such as Java and Haskell, have static “type systems” that prevent you from making certain programming errors.  The type system warns you if you use the wrong type, e.g. attempting to apply a method to an Integer instead of a Boolean.  There are also more advanced “dependent” type systems that can express richer types and avoid a much larger set of programming errors. With an advanced type system, the type is viewed as a “theorem”, and the corresponding program that matches the type is the “proof”.  This approach can be generalized beyond computer programming, and type systems can express math theorems, e.g. theorems about prime numbers. The theorems can then be proven by writing programs consisting of proof tactics.  This is how automated proof assistants work, such as Lean, Agda, and Rocq.   Proof assistants now have large libraries of math fundamentals, e.g. Lean mathlib4 has proofs of over 250K theorems!   These libraries can be used to prove further theorems, just like a Java class library. More advanced type systems, e.g. HoTT, will enable far more math theorems to be proven. However, using these systems still requires a lot of math expertise.  This is where AI comes in, which is now providing copilots to further automate theorem proving, making math more accessible while also improving rigor.  This is not just of theoretical interest, as the new theorems will be applied to develop better AI algorithms, and improve code quality and security.  I am excited to see what new applications this will unlock! [Note that the above is entirely my own opinion, and in no way represents the views of Amazon]

I just merged my latest contribution to PhysLean — a growing open-source library that formalizes physics in Lean 4, the same proof assistant used by the mathematics community to build Mathlib. PR #876 tackles the classical harmonic oscillator's configuration space. What does that mean concretely? In physics we usually treat configuration space as "just ℝ" and move on. But when you formalize things in a theorem prover, you're forced to be precise about every layer of structure: algebraic operations, topology, metric, norm, inner product, smooth manifold charts — all the way up to the map that sends an abstract configuration to a position in physical space. So this PR: → Introduces a dedicated ConfigurationSpace type with all the necessary mathematical structure → Equips it with a smooth manifold instance (ChartedSpace + IsManifold, modeled on ℝ) → Provides the explicit embedding into 1D physical Space → Refactors the harmonic oscillator API so that trajectories, equations of motion, Hamiltonian/Lagrangian identities, and solution lemmas all live over this new type Why does this matter beyond the harmonic oscillator? Because the pattern generalizes. Once you have a clean, formally verified configuration-space API for the simplest mechanical system, you have a template for N-particle systems, constrained systems, field theories — anywhere the distinction between "abstract coordinates" and "physical space" actually matters. It's a small step, but it's the kind of foundational infrastructure that makes future formalization work dramatically easier. If you're curious about the intersection of formal mathematics, physics, and software engineering, PhysLean is a fascinating project to follow: https://lnkd.in/dg8S9TUz #PhysLean #Lean4 #FormalVerification #MathematicalPhysics #OpenSource

Opus 4.6 can construct substantial, mechanically verified Lean 4 formalizations of advanced category theory with effective tool support. Over two short sessions, the model helped build a 900 line library covering categories, functors, natural transformations, monoidal structures, monads as monoid objects, and the Yoneda lemma, translating standard textbook material directly into type checked code. It handled routine structural proofs easily and managed more intricate obligations such as pentagon and triangle coherence conditions, though it produced verbose and poorly factored proofs that required human refactoring for clarity. In proving that a monad forms a monoid object in the endofunctor category, it captured the correct abstraction but needed guidance to structure auxiliary lemmas and improve readability. Direct integration with the Lean language server, including goal inspection and tactic experimentation, proved decisive by enabling iterative correction. Limitations remain in multi step planning and tactic selection, yet recent progress suggests rapid improvement in automating formal reasoning workflows. https://lnkd.in/gs-7MVGM

Most existing #lean4 datasets contain only correct proofs. Models learn error correction with RL, that's expensive. With UW Math AI lab we release a dataset of 260k erroneous Lean proofs with - compiler feedback - reasoning trace - corrected proof Improvements in Error Correction: - Goedel 8B: 2x - Kimina 8B: 3x Paper: https://lnkd.in/gaybt4bd

Here is an interesting new paper: "Accelerating Scientific Research with Gemini: Case Studies and Common Techniques" https://lnkd.in/d2KQd8U3 What caught my attention is that they mention formalization as a "future direction" in Section 9.2, and write: > "Future research must focus on building autoformalization pipelines that automatically translate LLM-generated informal mathematics into formal verification languages (such as Lean, Coq, or Isabelle)." Actually, such "autoformalization pipelines" already exist today. All that you need to do is to type "formalize this in Lean 4" in Codex/GPT-5.3. :)