Lean FRO

770 days from the day I wrote the first word to this stack of books arriving at my front door. I can't wait to share The Proof in the Code (Quanta Books) with everyone when it comes out on June 9. https://lnkd.in/gDSCesMh

Finalmente Lean e Leonardo de Moura foram mencionados no IA Sob Controle, episódio 255 ( https://lnkd.in/deuA-8Tv ), no capítulo sobre Google Para quem quiser saber mais sobre Lean, recomendo seguir Lean FRO e três entrevistas com Leonardo: Lean e Verificação de Software, com Leonardo de Moura (AWS) https://lnkd.in/dQf2mF7j Raciocínio Automatizado, com Leonardo de Moura (criador de Lean e Z3) https://lnkd.in/dwYZ2WAk Z3 and Lean, the Spiritual Journey - Leo de Moura https://lnkd.in/dBtSJ9Ki

𝐇𝐢𝐠𝐡𝐥𝐢𝐠𝐡𝐭𝐢𝐧𝐠 𝐭𝐡𝐞 𝐫𝐞𝐜𝐞𝐧𝐭𝐥𝐲 𝐟𝐢𝐧𝐚𝐥𝐢𝐳𝐞𝐝 𝚌𝚋𝚟 𝐭𝐚𝐜𝐭𝐢𝐜, 𝐧𝐨𝐰 𝐚𝐯𝐚𝐢𝐥𝐚𝐛𝐥𝐞 𝐢𝐧 𝐋𝐞𝐚𝐧 𝟒.𝟑𝟎.𝟎. "Call-by-value evaluation" is how most software actually runs: arguments get computed before being passed to a function. 𝚌𝚋𝚟 brings that same execution model into the proof layer. This matters for: ⚡ Software verification: proofs about functions, including those defined via well-founded recursion, can now be closed by simply running the function — no need to trust the compiler. 🧠 Mathematicians: goals that boil down to a concrete calculation can be settled by evaluation. 𝚌𝚋𝚟 computes the term to its final value instead of leaving you to work through the reduction by hand. 🔧 Teams building on Lean: 𝚌𝚋𝚟 exposes extensibility hooks, custom simplification procedures and attributes, so verification workflows can be tuned to specific domains. 𝐓𝐚𝐜𝐭𝐢𝐜 𝐫𝐞𝐟𝐞𝐫𝐞𝐧𝐜𝐞: https://lnkd.in/edC3sqvd #LeanLang #LeanProver #ProofAssistant #OpenSource #FormalVerification

The programming language and math proof assistant Lean is the latest tool in a millennia-long search to discover and verify the truth. In the fourth and third century BCE, early proofs by Aristotle and Euclid laid the groundwork for rigorously verifying mathematics. Later, Gottfried Leibniz, Bertrand Russell, Alfred North Whitehead, and Kurt Gödel sought the truth by representing math as a formalized, rational, symbolic language that could be objectively evaluated. If all of mathematics builds on solid foundations, they thought, you could in principle construct an edifice to answer the field’s most important, unsolved questions. Today, Lean continues this legacy of truth-seeking, giving mathematicians a powerful, interactive tool with which to fulfill Gödel’s dreams of “prov[ing] any theorem using nothing but a few mechanical rules.” Learn more in Kevin Hartnett's THE PROOF IN THE CODE, publishing June 9. Preorder your copy here: https://lnkd.in/eSqeiBqb. --- Image credits (from left): Wellcome Collection gallery, Photo Researchers—Science History Images/Alamy, Christoph Bernhard Francke, Keystone France/Getty Images, Hulton Archive/Getty Images, Alfred Eisenstaedt/The Life Picture Collection/Getty Images.

My team in the Automated Reasoning Group at AWS is looking for people that can hit the ground running working with SAT/SMT solvers and/or interactive theorem provers, especially Lean. This generally means significant experience working on these topics-- either during a PhD or in practice. Feel free to DM me, or contact us to chat about the opportunities. The official job postings are below

Interesting week for AI + math. While OpenAI grabbed headlines disproving an 80-year-old Erdős conjecture, DeepMind quietly dropped what looks like the more interesting paper. AlphaProof Nexus writes proofs in Lean — a formal proof language where the compiler checks every logical step. If it compiles, it's correct. No human review needed. The reported results: 9 of 353 open Erdős problems solved, 44 open OEIS conjectures proved, a 15-year-old algebraic geometry problem closed. Several open since 1970. Cost per problem: apparently a few hundred dollars of inference compute. The paper says the system is already being used by researchers in quantum optics, graph theory, and algebraic geometry. What stood out reading through it: the basic agent — just an LLM looping with the Lean compiler, no RL sub-solvers, no evolutionary search — reportedly solved all 9 Erdős problems the full-featured system did. Fancier variants were more efficient, not more capable. If that holds up, it's a telling signal. The hard part isn't the scaffolding — it's model quality combined with a formal layer that makes outputs verifiable. Everything else is optimization. OpenAI's approach still requires humans in the verification loop. Fine for landmark results. Harder to scale. If the numbers check out, math research just became a throughput problem.

Agentic Systems : Lean - The fundamentals of Verifiability Lean is not just a programming language; it is a theorem prover and a proof assistant. In the context of AI and computer science, it acts as the ultimate, unhackable referee for logic. Here is a breakdown of how Lean manufactures verifiability and why it is being adopted by major tech companies. 1. The Core Mechanism: The Minimal Trusted Kernel The foundation of Lean’s verifiability is its "minimal trusted kernel." When you write a mathematical proof or a software algorithm in Lean, you aren't just writing instructions for a computer to execute. You are writing propositions that the Lean compiler must rigorously check against the fundamental axioms of mathematics. The "trusted kernel" is a tiny, highly audited piece of core code. If a complex AI agent (like AlphaProof) or a human mathematician writes a million-line proof, the kernel checks every single logical step down to its atomic roots. If it compiles, it is absolutely, mathematically correct. There is no room for hallucination, edge-case bugs, or "mostly correct" code. 2. Real-World Verifiability Applications The Lean website highlights that this level of absolute verifiability is no longer just an academic exercise; it is being deployed in industrial engineering: Aeneas (Memory Safety): Lean is being used to verify Rust programs. Instead of testing memory usage empirically (which can miss edge cases), Aeneas leverages Lean to logically prove that memory leaks or faults are impossible within the program's structure. Mathlib (The Collaborative Oracle): Lean hosts "Mathlib," a massive, community-driven library containing over a million lines of formalized, verified mathematics. It acts as a foundational truth repository, ensuring that new frontier research is built on perfectly sound logic. 3. The Enabler of AI Reasoning Lean was the exact technology that made AlphaProof possible. Because Lean provides instantaneous, absolute, binary feedback (it either mathematically compiles or it doesn't), it serves as the perfect reward function for Reinforcement Learning. An AI can generate millions of synthetic, highly creative mathematical theories, and Lean will automatically prune the hallucinations and verify the breakthroughs without ever requiring a human expert to read the code. In short, Lean translates the abstract, fuzzy concepts of human logic into a rigid, verifiable landscape that both software systems and AI agents can safely navigate. Links in comments

In just a few years artificial intelligence tools have progressed from solving formulaic math contest problems to generating novel proofs of long-standing open conjectures. The way math is done is changing, and more change is coming. Anyone interested in math should be paying attention to the unfolding story of AI-assisted mathematics, and this is especially true for math teachers, whose current students will enter a world where “doing math” is likely to mean something dramatically different than it does today. Kevin Hartnett's “The Proof in the Code” is an excellent entry point into that world. Hartnett tells the origin story of Lean, a mathematical formalization tool playing part in the AI-assisted mathematics revolution. Originally developed by researchers at Microsoft to debug code, Lean is now being used in synthesis with generative AI tools like large language models to debug mathematical proofs. The results have been astonishing. “The Proof in the Code” is the story of the people and the ideas behind Lean, but it’s also the story about how we’ve arrived at a place where one of the world’s leading mathematicians recently felt obligated to say “It’s not necessarily the end of mathematics”. Hartnett’s book is a satisfying read for anyone interested in science and technology, but for teachers and learners of math, “The Proof in the Code” isn’t just a compelling tale of recent theoretical advances. It’s part of the backstory of the next chapter of human mathematics. Quanta Books Quanta Magazine https://lnkd.in/eafrBdiw

𝐋𝐞𝐚𝐧 𝟒.𝟑𝟎.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! This release brings 306 changes, including a new 𝚜𝚢𝚖 => interactive tactic, completion of the new LCNF compiler backend with user borrow annotations, and a major overhaul of Lake's caching infrastructure. Notable improvements include: 🧠 𝚜𝚢𝚖 => is a new interactive tactic mode built on 𝚐𝚛𝚒𝚗𝚍. Unlike 𝚐𝚛𝚒𝚗𝚍 =>, it gives users "explicit control over each step," allowing use of all 𝚐𝚛𝚒𝚗𝚍 infrastructure with a custom proof strategy. ✨ 𝚌𝚋𝚟 is no longer experimental and gains 𝚊𝚝 location syntax, a 𝚌𝚋𝚟_𝚜𝚒𝚖𝚙𝚛𝚘𝚌 system, and short-circuit evaluation for 𝙾𝚛/𝙰𝚗𝚍. ⚡ The LCNF expand reset/reuse pass, ported from IR with improved exponential-code prevention, results in a "~15% decrease in binary size and slight speedups across the board." 📦 Lake's caching infrastructure receives a comprehensive overhaul: on-demand artifact downloads during 𝚕𝚊𝚔𝚎 𝚋𝚞𝚒𝚕𝚍, parallel transfers via 𝚌𝚞𝚛𝚕 --𝚙𝚊𝚛𝚊𝚕𝚕𝚎𝚕, and new staged cache subcommands mirroring Mathlib's 𝚕𝚊𝚔𝚎 𝚎𝚡𝚎 𝚌𝚊𝚌𝚑𝚎. 𝐅𝐮𝐥𝐥 𝐫𝐞𝐥𝐞𝐚𝐬𝐞 𝐧𝐨𝐭𝐞𝐬: https://lnkd.in/ePE7EiPg #LeanLang #LeanProver #ProofAssistant #OpenSource #FormalVerification