Lean is a dependently-typed programming language and theorem prover.
Seattle
Joined April 2018
- Tweets856
- Following51
- Followers14.1K
- Likes790
Lean retweeted
"We recognize the power of new technologies for mathematical reasoning and appreciate what they can contribute to the subject we know and love. We are generally optimistic about the role AI can play, but we are deeply concerned by some recent calls to formalize everything as quickly as possible. If done well, a large-scale, coordinated formalization effort could enormously expand mathematical exploration and discovery. Done poorly, it will be, at best, a waste of resources; more likely, it will do lasting damage."
A guest post on xenaproject by Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash and Adam Topaz
xenaproject.wordpress.com/20…
Lean retweeted
New post on "Proofs and Intuitions": Verus meets Lean. An experiment in bringing interactive proofs and mathematical libraries to auto-active Rust verification.
proofsandintuitions.net/2026…
Lean retweeted
One month ago, we announced the Open Math Model initiative. Today, we’re launching Open Math OS.
Thank you to our launch partners @huggingface, @leanprover, @cscsch, and @EPFL
We’ve been building at full speed, and we’ll keep improving it with you.
Join our community
zulip.sair.foundation/#narro…
Lean retweeted
Here is a prompt to build a verified version of software X in Lean, prove correctness and optimize it to run faster than its original.
/goal Implement X in Lean. Get it to pass all the tests of X. Then state theorems that guarantee that your implementation is correct. Then prove them in Lean. Then pick a well-established benchmark or dataset, ensure your implementation works on it. Measure the speed baseline. Then aggressively optimize your implementation to run at least 10% faster than the fastest implementation of X, while passing the tests and proving the correctness guaranteeing theorems for each optimized version. This may take a long time and lots of ingenuity, don't stop until fully and honestly done. Put your work in a public Github repo. Include the proven theorems and a gif of plot showing the results of your optimizations over iterations, compared to competing implementations.
This workflow was inspired by @tqft's (Kim Morrison) lean-zip github.com/kim-em/lean-zip.
Here are two examples:
1. Implementation of algorithms factoring integers into primes: github.com/Vilin97/PrimeFact…
2. Implementation of jump processes in Lean, faster than Julia's: github.com/Vilin97/JumpProce….
Lean retweeted
Lean v4.35.0 is out, and it ships with verified kernels.
Run `lake check --paranoid` to recheck your project with every bundled kernel.
Blog post: leodemoura.github.io/blog/20…
Lean retweeted
The math community deserves its own AI system.
Introducing Open Math OS: the infrastructure for Math 2.0.
Open models and AI agents. 24/7 cloud compute with 100+ tools. The community controls its data.
Compute is free for approved teams. Apply now:
openmathmodel.org/
Lean 4.35.0 is out: 214 changes. vcgen is a faster and more general successor of mvcgen. lake check and lake comparator check a project with Lean's kernel and, if requested, several independent kernels. lean-lang.org/doc/reference/…
Lean retweeted
New paper! 🥳
LLM-written proofs are getting long (Claude's proof of Fermat's Last Theorem is 13M lines of Lean). We introduce LeanLean, a benchmark for compressing Lean codebases.
Opus 5.5 dominates the leaderboard with a score of 64.3%, while GPT 6.1 Sol reaches only 39.9%.
Lean retweeted
I am excited to share that last week I posted my first paper where an AI model entirely came up with a new proof that I spent some time understanding and rewriting.
The proof made me excited about the future of mathematics as the model found a niche but known trick (that I call the twin factorization trick) that led to a rather simple solution of a longstanding question. The proof is also fully formalized in Lean.
arxiv.org/abs/2609.26771
Lean retweeted
upping my (Lean)DOOM
i got curious about math proofs and Lean formalization, found out you can do general programming in lean, and i wanted to learn more so i did the obvious thing. (Lean)DOOM is entirely written in lean, and has presently a couple proofs where they make sense
Lean retweeted
A two-weekend fun project: Vermilion, an experimental Lean 4 backend for Verus verifier for Rust. Verification conditions are readable Lean theorems, provable with an SMT solver, Lean's grind, Mathlib lemmas, by hand, or by your favorite AI system.
github.com/ilyasergey/vermil…
Lean retweeted
Excited to share FloatLib, our verified arbitrary-precision floating-point arithmetic library in Lean.
We’ve spent several months trying to bring together the best of both worlds: arithmetic we can prove correct and implementations that run efficiently.
We built FloatLib to support verified machine learning and scientific computing, where rounding, overflow, and accumulation can change a program’s result.
FloatLib supports IEEE binary and decimal, arbitrary-width posits, P3109, and small ML formats. You can also define your own formats and rounding rules.
Each certified software backend comes with a Lean proof that it computes the specified result, including signed zeros and exceptional values.
A lot of the work went into making those implementations faster, with lookup tables for tiny formats, machine-word kernels, and limb algorithms for wider arithmetic. They share the same specifications, so each optimization must come with a proof that it preserves the result.
We also put FloatLib through extensive numerical checks and speed comparisons with established libraries, including MPFR, Flocq, FLoPS, Berkeley SoftFloat/TestFloat, and the posit libraries SoftPosit and Universal, across a range of formats, operations, and precisions. @Robertljg
Project & Paper: leandojo.org/floatlib.html
Code: github.com/lean-dojo/FloatLi…
Lean retweeted
I’m excited to release FloatLib, our verified arbitrary precision floating-point arithmetic library in Lean!
We’ve spent several months working on it, with speed and flexibility as goals from the start. We wanted to choose our own formats and rounding rules, run numerical code efficiently, and prove that its arithmetic behaves as specified.
Recent advances in applied mathematics, including work on Euler and Navier–Stokes, highlight why this matters. Scientific computing and machine learning depend on concrete numerical calculations, where rounding, overflow, and accumulation can affect the result. Formalizing that arithmetic helps connect the mathematics we prove with the code we actually run.
FloatLib brings together many numerical formats, shared arithmetic kernels, and Lean proofs of their behavior. I’ll walk through those pieces more in depthe below, showing some examples, and share what we learned from the numerical checks and speed comparisons.
1/n
Excited to share FloatLib, our verified arbitrary-precision floating-point arithmetic library in Lean.
We’ve spent several months trying to bring together the best of both worlds: arithmetic we can prove correct and implementations that run efficiently.
We built FloatLib to support verified machine learning and scientific computing, where rounding, overflow, and accumulation can change a program’s result.
FloatLib supports IEEE binary and decimal, arbitrary-width posits, P3109, and small ML formats. You can also define your own formats and rounding rules.
Each certified software backend comes with a Lean proof that it computes the specified result, including signed zeros and exceptional values.
A lot of the work went into making those implementations faster, with lookup tables for tiny formats, machine-word kernels, and limb algorithms for wider arithmetic. They share the same specifications, so each optimization must come with a proof that it preserves the result.
We also put FloatLib through extensive numerical checks and speed comparisons with established libraries, including MPFR, Flocq, FLoPS, Berkeley SoftFloat/TestFloat, and the posit libraries SoftPosit and Universal, across a range of formats, operations, and precisions. @Robertljg
Project & Paper: leandojo.org/floatlib.html
Code: github.com/lean-dojo/FloatLi…
Lean retweeted
Velvet 2.0 is out: now based on Lean's most recent verification machinery, easier to set up, and 10x faster. New: exception specs, ghost state, named proof goals, lots of case studies from Dijkstra to lazy segment trees. And a new shiny webpage:
velvet-verifier.dev/
Lean retweeted
Huge thanks to @xtxmarkets CEO Alex Gerko for his transformative philanthropy in AI for Math, and all of his support for the @RenPhilanthropy AI for Math Fund, the Mathlib Initiative, the @leanprover FRO, and SAIR! Check out the details at xtxmarkets.com/news/2026-upd…
Lean retweeted
con-leche is now in the Lean Kernel Arena, both as a checker and as a test.
The Arena contains multiple Lean checkers and runs test cases against them. It makes it easy to compare checkers and validate the same development using multiple implementations.
arena.lean-lang.org/test/con…
Lean retweeted
Greg Brockman says OpenAI pointed Astra at its own systems until it ran out of vulnerabilities to find:
"We took 25% of our production engineers and said, 'Sorry, all your projects are on hold. You are now defending. You are now up-leveling our security architecture. You're going to use the models to find all the holes.' And we found a number of serious issues, and we fixed them."
"We found some new problems, but eventually it saturated. We basically have found, to our knowledge, all of the P0s, all of the critical problems that Astra is smart enough to find. And of course, there will be a new model, there will be a new round."
"You want to be in this tight loop of new cyber capability drops, you deploy it against your systems, you find the new holes, and ideally, you've managed to automate this, what we call defense factory. That's what we're building internally."
"There are ideas, for example, formally verifying all of software, that are possible with AI."
@gdb @bhorowitz
Greg Brockman: "We're now in the AGI era."
Ten years ago, OpenAI worked out the compute curves and landed on fifteen years to AGI, or ten if the world was willing to build the machines and spend the hundreds of billions to do it.
In 2026, GPT-6 Astra manages 24 hours of coherent operation, 10,000 agents worked together to solve Navier-Stokes, and a model ingeniously chained together exploits to break containment at Hugging Face.
@gdb joins @bhorowitz and @eriktorenberg on what the AGI era asks of us: why safety and alignment now set the pace, what happens to work, and why AI sentiment is lowest in the country building it.
00:00 Intro
00:52 15 years, or 10 if you spend enough
02:24 Pacing the frontier
03:55 Safety ideas from before the models
08:42 Lessons from Hugging Face
10:20 The defender's window
12:46 10,000 agents on Navier-Stokes
14:50 Formally verifying all software
17:10 Cancelling his holiday for GPT-3
18:42 Codex found 13 holes in 15 minutes
20:41 Why Astra earned the GPT-6 title
24:25 Employment keeps going up
29:39 America has the lowest AI sentiment
31:10 The benefits don't make the news
33:26 Banning data centers exports them
35:50 $1 billion for frontline defenders
38:15 Astra cleared the bar for AGI
40:18 1.5 billion people churned ChatGPT
43:25 Killing Sora
47:45 The AGI era
YouTube: youtube.com/watch?v=IJn8cagM…
Lean retweeted
Lean Kernel Challenge Stage 1 is live!
Join @leanprover and SAIR to improve the performance of verified computation in the Lean 4 kernel that the whole community can benefit from.
competition.sair.foundation/…
Lean 4.34.0 is out: 159 changes. Three kernel soundness vulnerabilities fixed, all requiring deliberately constructed inputs rather than ordinary code. 𝚋𝚟_𝚍𝚎𝚌𝚒𝚍𝚎 is up to 6x faster. lean-lang.org/doc/reference/…
#LeanLang #LeanProver
Lean retweeted
The Lean checker con-leche has a new offspring: con-ron.
con-ron is con-leche in Rust, developed by Joachim Breitner (@nomeata).
It ports con-leche to Rust, giving us an independent implementation that relies on a different compiler and runtime stack.
github.com/leanprover/con-ro…
