The news that caught my attention this week: Mistral released Leanstral 1.5 as an open-weight model that generates complete Lean 4 proofs. Give it a function with a bug, and it produces a formal proof of the vulnerability, verified by the Lean kernel. The whole pipeline works end to end.
This is not a toy. The model found a real overflow bug in the Uniswap v4 codebase, a value+1 wrapping on U64.MAX that compilers do not catch because it passes type checks. Leanstral produced the proof, Lean confirmed it, and the vulnerability was real. The demonstration is convincing enough that several crypto auditing firms have already started evaluating the tool.
Most of the commentary I have seen focuses on the obvious implications: math education will change, formal verification costs will drop, bug finding will accelerate. These are real but they miss the deeper shift. The interesting question is not whether Leanstral works. It is what happens when proof generation costs pennies.
The first consequence is an inversion of the verification economy. Today formal verification is expensive because it requires expert time. A single proof of a non-trivial property can take a PhD week. At that cost structure, you only verify things that matter enormously: cryptographic implementations, kernel safety properties, financial settlement logic. When a model generates the same proof for a few cents of compute, the economic calculation flips. You can afford to verify everything. The question becomes what you should verify, not whether you can afford to.
But cheap verification creates a second-order effect that almost nobody is discussing. When proof generation becomes a commodity input, formal verification becomes an offensive tool as well as a defensive one. A competitor can run your compiled binary through Leanstral for eight dollars, find a kernel-verified timing side channel in your signal processing code, and publish the proof. The vulnerability landscape shifts from "can we find a bug" to "can we prove a bug exists." That changes the incentive structure for shipping software in ways that liability frameworks are not ready for.
There is a subtler problem hiding in the marquee bug itself. The overflow on U64.MAX is what working programmers call a trivial bug. Compilers do not catch it, but experienced engineers catch it during code review. The gap between a correct proof and an interesting proof is wider than the current demos suggest. Leanstral generates correct proofs. It does not generate insightful proofs. The risk is that we flood the ecosystem with millions of verified-but-trivial properties, creating a signal-to-noise problem that mirrors what happened to unit test coverage when mocking frameworks made tests cheap.
The infrastructural question is more serious. Every Leanstral proof ultimately depends on the Lean kernel. If the kernel has a bug, every theorem verified through it is compromised. Traditional mathematics distributes verification across thousands of independent human readers. There is resilience in that distribution: a subtle error in a published proof might take years to surface, but it will surface. Centralizing verification trust in a single codebase creates a monoculture risk, and we just learned from the xz backdoor what happens when monocultures in foundational infrastructure get compromised. Formal verification does not eliminate the monoculture problem. It concentrates it.
The social consequences are harder to quantify but possibly more important. Mathematics has always been a human activity organized around proof. The pace of proof production was slow enough that the community had time to digest each result, argue about it, rewrite it, and absorb it into shared understanding. Leanstral inverts that rhythm. A theorem is verified before anyone discusses it. The community shifts from being the arbiter of correctness to being the interpreter of consequences. That changes not just who does mathematics but what mathematics is for.
There is a generational question that follows. The struggle of constructing a proof is how mathematical intuition develops. You wrestle with the gap between what you know and what you need to show, and that wrestling builds the mental muscle that lets you recognize which theorems are worth proving and which are dead ends. An undergraduate who learns to prompt a proof generator instead of constructing arguments will be missing that apprenticeship. The gains in speed will come with losses in judgment.
The authorship question is not just academic. When a model suggests the proof structure, the human refines the specification, and the kernel performs the verification, who gets credit for the theorem? The prestige system in mathematics rewards the solver, not the asker. But when solving becomes the easy part, the person who asked the right question becomes the scarce resource. Departments that reorganize around problem-finding rather than problem-solving in the next decade will be the ones that thrive.
The unreadable proof points in the same direction. An AI generates a formal argument, the kernel verifies it, and the human trusts the result without ever reading the proof. The mathematical understanding lives in a pipeline of black boxes. Nobody checks the reasoning anymore because the reasoning is machine language. This is epistemically fragile in ways that go beyond the monoculture risk of the kernel itself. It changes what it means to know that a theorem is true.
All of this is coming faster than the institutions that depend on mathematical proof are prepared for. Mistral released Leanstral as open-weight. That means the capability is not controlled by any single organization. Proof generation will spread through every domain that touches verification: smart contracts, operating systems, cryptographic protocols, compliance audits, regulatory filings. The question is not whether the shift happens but which norms break first.
Proofs are cheap now. The cost of certainty just dropped by several orders of magnitude. The hard part is figuring out what we actually want to be certain about, and who gets to decide.