Lean FRO

Aleph Prover, our fully autonomous AI agent system for formal verification, aced all major theorem proving benchmarks including PutnamBench, VeriSoftBench, and Verina. Read more about this accomplishment and what it means. https://lnkd.in/eg7b3qBG The implications for these formal tests for “correctness” extend far beyond academic competition: ▪️ Provable correctness in safety-critical software ▪️ Hardware verification for chips and embedded systems ▪️ High-assurance cryptography and infrastructure ▪️ Automated theorem proving for scientific research ▪️ AI-generated code with provable guarantees Traditional AI systems generate outputs in natural language or source code. Even when those outputs appear convincing, they often contain subtle logical failures, unverifiable assumptions, or hidden correctness issues that only reveal themselves downstream. In low-risk consumer applications, those errors may be tolerable. Inside critical infrastructure or production engineering systems, they are not. Join the waitlist for Aleph here: https://lnkd.in/eWzSKpqT

👥 Save the date: CSLib Online Meetings Announcing the beginning of the CSLib online meetings, aimed at coordinating and facilitating the development of the library and its use. The meetings are an opportunity to discuss CSLib and exchange information with the rest of the community and the maintainers. The first meeting will take place on Thursday, 21 May 2026, at 12:30. If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes. #Lean #FormalMethods #CSLib #FORM Lean FRO Centre for Formal Methods and Future Computing (FORM)

As part of a deep dive into AI-assisted, assembly-level programming in Lean, I recently implemented and formally verified a toy VM in Lean. You can play 2048 in your terminal! (For real, test it out!) This is an implementation of LC3, a VM commonly used in university courses. It has eight general-purpose registers, a program counter, condition flags, and a 2^16-word address space. At each step the machine fetches a word from memory at the PC, decodes it as one of fourteen opcodes (from arithmetic and bitwise operations to loads, stores, branches, jumps, and subroutine calls), then updates registers, memory, and control flow accordingly. Beyond those opcodes, LC-3 programs rely on trap routines for console I/O and on memory-mapped I/O for the keyboard—so a faithful simulator must implement both the core instructions and this I/O story. Finally, each of the fourteen opcodes are formally verified with respect to a specification written in Lean. Now you can rest easy while playing 2048 in my VM ;) This is a toy example, but we're currently in the process of scaling this type of programming up in some serious ways. We are becoming more and more convinced that Lean is an exceptional macro assembler (maybe the best?) and AI + formal proof could make it feasible to write super-efficient, custom programs at the assembly level with associated proofs of correctness. Stay tuned for more on that! For the repo: https://lnkd.in/eZPsiESZ An associated blog post: https://lnkd.in/egkeG4Ki

I’m very excited that TorchLean is finally public! Anima Anandkumar already shared a great overview, so I’ll keep this more personal. I’ve been working on TorchLean over the past year, thinking about one question: What would it mean for neural networks to not only run, but also carry precise, checkable meaning? TorchLean explores this in Lean 4: typed tensors, graph IRs, runnable training, GPU/CUDA support, autograd, Float32/IEEE-style semantics, verification, and certificate checking. Huge thanks to Jennifer Cruden, Xiangru Zhong, Huan Zhang, Will Adkisson, Anima Anandkumar, the Lean community, and everyone who gave feedback. I’ll put the codebase, project page, and a longer blog I wrote in the comments. #MachineLearning #ScientificComputing #FormalVerification #Lean

📣 The SAIR Science x AI Summit is going live at 9:30AM PDT today! The summit brings together "the world's leading scientists, AI pioneers, industry leaders, investors and builders for two days of high-signal conversation at the frontier." 𝐀𝐭 𝟏𝟏:𝟎𝟓𝐀𝐌 𝐏𝐃𝐓 𝐭𝐨𝐝𝐚𝐲: Keynote by Lean FRO Chief Architect Leo de Moura, describing where Lean stands today: 250,000+ installations, 270,000+ formalized theorems in Mathlib, supporting IMO gold medals, verified production software at AWS, Microsoft, and Google, and what comes next as AI takes on a larger role in proof development. 📺 Tune into the livestream: https://lnkd.in/gVRY5zrU #LeanLang #LeanProver #SAIR #Science #AI

The Hackathon "LeanLang for Verified Autonomy" by Indian Institute of Science (IISc) and Emergence AI had participants starting #leanprover from scratch and delivering projects in 10 days. The participants rose to the challenge and delivered amazing projects. A delightful blog post by one of the prizewinners, Durwasa Chakraborty, whose project with Vimala Soundarapandian showed how Lean can be used to translate JSON queries to SQL with proof of correctness. . Leonardo de Moura Lean FRO http://disq.us/t/53xgx9a