Lean is a dependently-typed programming language and theorem prover.
Seattle
Joined April 2018
- Tweets873
- Following52
- Followers14.5K
- Likes812
Lean retweeted
We're in @nytimes: if AI can prove open math problems, can it prove software has no bugs? That is what we work on, with Lean as the foundation for machine-checked trust.
nytimes.com/2026/10/29/scien…
Lean retweeted
I'm thrilled to bring &Truth out of stealth as its co-founder and Chief Science Officer. With a team I'm proud to be part of, we're setting out to specify and prove all the world's software correct and secure.
If you geek out over code people can understand and trust, join us!
We are out of stealth! As AI writes more code, we're building tools to prove programs meet precise requirements, with Lean proofs anyone can independently check. Let's make verified software the norm in every language and application.
Come take a look: andtruth.com
Lean retweeted
We are out of stealth! As AI writes more code, we're building tools to prove programs meet precise requirements, with Lean proofs anyone can independently check. Let's make verified software the norm in every language and application.
Come take a look: andtruth.com
Highlighting two great sites for the latest on Lean, both built and curated by @soonhokong .
📄 𝐏𝐚𝐩𝐞𝐫𝐬 𝐖𝐢𝐭𝐡 𝐋𝐞𝐚𝐧: "arXiv papers that use Lean, the interactive theorem prover. Updated daily." You can browse by topic or by the last 7 or 30 days.
paperswithlean.com
📰 𝐋𝐞𝐚𝐧 𝐖𝐞𝐞𝐤𝐥𝐲: News about Lean, from Lean core to verification to AI and formalization, organized by week.
leanweekly.news
We're grateful to Soonho for this work.
Software Verification in Lean on November 7 has reached in-person capacity! If you're interested in attending live, please join the waitlist: A livestream link will be shared with all waitlisted registrants a few days before the event.
Software Verification in Lean (SVIL) comes to Stanford University on Saturday, November 7.
Co-organized by Beneficial AI Foundation and Lean FRO, it is a day of public lectures on advancing Lean’s software verification ecosystem toward production use, with a focus on end-to-end verification of security-critical systems.
Talks will cover Rust verification with the Aeneas framework, low-level software verification, and formally verified OS kernels.
Speakers include Max Tegmark, Shaowei Lin, Leonardo de Moura, Jonathan Protzenko, Andres Erbsen, and Mike Dodds.
In-person space is limited. Non-local and waitlisted registrants will receive a livestream link, and recordings will be available afterward.
Program and registration: beneficial-ai-foundation.git…
Lean retweeted
We also thank the Lean and Mathlib communities.
Completing the formalization is one milestone; making it more useful to mathematicians is ongoing work.
We’ll maintain and improve this codebase: faster builds, clearer organization, and results that are easier to find and reuse.
Congratulations to the Axiom team on this expansive undertaking.
Lean retweeted
1/🧵 Coding agents can make code faster. Can they also prove it still does the same thing?
Introducing Agentic Verified Optimization 🚀 Agents return faster code plus a Lean proof that it equals the original on every input.
🌐 Blog: aqueduct.verina.io
📄 Paper: arxiv.org/abs/2610.30188
Lean retweeted
9/ 📄 Paper: arxiv.org/abs/2610.30188
🌐 Blog: aqueduct.verina.io
Amazing work by @0xlf_, @udayaghai, @uniq_zz, @dawnsongtweets, @soonhokong 🙏
This work is done during my internship at @AmazonScience.
Software Verification in Lean (SVIL) comes to Stanford University on Saturday, November 7.
Co-organized by Beneficial AI Foundation and Lean FRO, it is a day of public lectures on advancing Lean’s software verification ecosystem toward production use, with a focus on end-to-end verification of security-critical systems.
Talks will cover Rust verification with the Aeneas framework, low-level software verification, and formally verified OS kernels.
Speakers include Max Tegmark, Shaowei Lin, Leonardo de Moura, Jonathan Protzenko, Andres Erbsen, and Mike Dodds.
In-person space is limited. Non-local and waitlisted registrants will receive a livestream link, and recordings will be available afterward.
Program and registration: beneficial-ai-foundation.git…
Lean retweeted
The computer science collaboration will understand and explain a result concerning the Exponential Time Hypothesis (ETH), a longstanding conjecture about the computational complexity of Boolean formula satisfiability, a problem deeply related to the P vs. NP problem.
Surprisingly, our system has recently proved that the ETH is false, a result that was subsequently verified in Lean.
The refutation of the ETH reopens questions about how much faster these tasks could become, and may help guide the search for better algorithms. Finding such algorithms, and turning theoretical advances into practical improvements, will require significant further research.
Our system found its natural language disproof for the ETH we reached out to to @rrwilliams. Ryan will form a collaboration with Russell Impagliazzo and Ramamohan Paturi to verify and shepherd this result. Impagliazzo and Paturi, along with Francis Zane, are the original proposers of the Exponential Time Hypothesis, and Williams has refuted strong versions of the ETH, used ETH for hardness results, and connected algorithms and lower bounds.
This group asked us to make all raw data of the results public to facilitate independent verification by the community, which we have done by posting the natural language proof and Lean formalization to our GitHub repo. The group also invites the community to help organize an open examination of the ETH claim and to discuss the broader questions that AI-generated breakthroughs raise about verification, access, credit, and the future of research.
github.com/openai/math/blob/…
Lean retweeted
The result in mathematics concerns harmonic analysis.
Our models produced a proof of the local smoothing conjecture in every dimension and therefore also resolve the Kakeya conjecture and Stein’s restriction conjecture in all dimensions. The new proof is based on a novel auxiliary partial differential equation.
We obtained our AI output, and then we reached out to an expert to discuss forming a collaboration around this result. Following their recommendation, we decided to release the AI output publicly, following the same strategy for this result as our October 6th, 2026 release. We have released both an AI natural language output writeup produced by our models and a Lean proof in our public GitHub repository.
github.com/openai/math/blob/…
Lean retweeted
This weekend we launched EthLib, a Lean4 library for Ethereum!
The goal is to bring Ethereum's primitives, specifications and theorems into one place, building a shared foundation for formally specifying and proving things about Ethereum.
github.com/ethereum/EthLib
Lean retweeted
More than 300 research teams have been approved and are using Open Math OS.
We recommend applying with your research institution email so we can easily verify your affiliation.
We’re scaling up to serve the math and science community.
Apply now:
openmathmodel.org/
Lean retweeted
Small announcement: ✅ formal-git
As an experiment, over the last 2 months we've modelled ~30% of Git in Lean 4, making heavy use of coding agents, and proved >8000 theorems of varying usefulness about the implementation.
In the process of doing this we've uncovered >100 potential defects in Git v2.55, at least two of which may constitute security vulnerabilities. We've also built a DRT (differential random testing) harness and the biggest corpus of relevant pinned differential test cases for Git implementations with >10k unique tests at the moment.
We've used the test cases to test our own small internal implementation of Git in TypeScript. The next step will be to differentially test all notable public Git implementations against this corpus of tests to help improve their correctness and security 🫡 We'll be reaching out to library maintainers in due course.
If you have a Git implementation you'd like us to help you test, please reach out and let me know. We'll open-source all this eventually, after potential security issues that were uncovered are responsibly disclosed and fixed.
ALT Infographic: Reads: formal-git, Git, rebuilt in Lean 4, with machine-checked proofs
Lean retweeted
We’ll write about the methodology, the process and the learnings soon.
One takeaway is that Lean 4 is a very beautiful programming language ✨
Lean retweeted
Over the past year, the Discovery team at @GoogleDeepMind, in a project led by student researcher @dsantosmarco, has made new discoveries in one of the most beautiful open problems at the edge of computation: Finding the 6th Busy Beaver (BB) number.
While most AI math systems solve human-generated problems, like theorems, this work tackles a different aspect of mathematical creativity: Discovering hidden problems.
For years, the BB Community has pursued one of theoretical computer science’s most captivating collaborative quests: finding the simplest programs that run the longest before halting. Because determining whether these programs ever stop is uncomputable, no universal algorithm can solve it, meaning new mathematical techniques need to be found and invented to make progress.
In this way, the BB challenge serves as an open ended domain for mathematical creativity and, in particular, a generator of hard math problems called Cryptids. These are tiny programs whose halting behavior is governed by and equivalent to deep, unsolved math problems in number theory, similar to the Collatz or Goldbach conjectures. Historically, the BB community had recognized ~20 Cryptids in BB(6), and the best problems were selected for the Busy Math Olympiad (BMO).
Building on their work, Marco built a pipeline powered by Gemini 4 Argon that:
1️⃣ Simulates raw Turing machine traces to compress recurring patterns.
2️⃣ Conjectures mathematical transition rules & runs synthetic experiments to test edge cases.
3️⃣ Proves the equivalence formally in Lean 4.
Using this pipeline, Marco and the team discovered 20 new potential Cryptids and verified 33 more machines previously studied in the BB community. All the proofs were open sourced and shared in the community discord channel and we hope that they will help the community to make progress towards resolving BB(6). We also contributed related halting/non-halting proofs directly to the community GitHub repository.
Finding these Cryptids shows hidden links between simple programs and number theory, and helps mathematicians map the limits of computation. I'm also excited about Gemini 4 Argon's ability to help researchers both solve hard problems and accelerate scientific discoveries, of which Busy Beaver is just one example.
Work led by our student researcher @dsantosmarco with paper contributions from @vivek_veeriah, @Dahoas1 , Andrew Bolt, @zuza777 , Satinder Singh, and myself with additional contributions from Hussain Masoom, @maxencefaldor , @MoritzFirsching and Petar Sirkovic.
Read more about it in our paper: arxiv.org/abs/2610.22603
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…
