How AI's Math Breakthroughs Are Changing Software Engineering

AI's 2025 math breakthroughs affect software engineering because the same technique that let models prove novel theorems is now proving code correct, not just plausible. Verification just moved from an academic niche to something coding agents can do on a normal engineering timeline, and that changes how much you can trust the software you ship.

Here's the chain, and what it means for the code your team ships this year and next.

What happened: AI's 2025 math breakthroughs, in plain terms

In July 2025, OpenAI's experimental reasoning model and Google DeepMind's Gemini Deep Think both hit gold-medal level at the International Mathematical Olympiad, each solving 5 of 6 problems for 35 of 42 points under official IMO grading.¹²³ No AI system had cleared that bar before.

DeepMind's result is the more telling one. In 2024, its AlphaProof and AlphaGeometry systems needed two to three days of computation, and problems had to be manually translated into the formal proof language Lean before the models could touch them.² A year later, Gemini Deep Think solved the same class of problems end to end, in natural language, inside the actual 4.5-hour competition window.² The gap between "needs a specialist to translate the problem first" and "just does it" closed in twelve months.

Around the same time, DeepMind's AlphaEvolve, a Gemini-powered coding agent, found a new algorithm for multiplying two 4x4 complex matrices using 48 scalar multiplications, the first improvement on Strassen's algorithm in that setting in 56 years.⁴ AlphaEvolve didn't just solve a puzzle. It discovered a provably correct algorithm that beat the previous state of the art, and Google then reused it to optimize its own data-center scheduling and chip design.⁴

That last detail is the thread this whole story pulls on: the tool that wins math medals is the same tool that improves production infrastructure.

Why math reasoning and code correctness are the same problem

A mathematical proof and a software correctness proof are the same kind of object. Both are a sequence of logical steps, checked by a machine, showing a claim holds for every case, not just the ones you happened to test.

Lean, the open-source proof assistant, is the shared substrate for both. Every major AI system that has reached IMO medal-level performance, including AlphaProof, Harmonic's Aristotle, SEED Prover, Axiom, Aleph, and Mistral's systems, is built on Lean.⁵ Lean is backed by Mathlib, a community library of more than 200,000 formalized theorems contributed by roughly 750 people.⁵ That library exists to help AI prove things about numbers. It turns out the same infrastructure, and the same trained reasoning ability, works to prove things about programs. We break down what that actually buys you in our explainer on AI formal proofs in Lean 4, including why almost none of the AI-written code running in production today has one.

So when a lab improves a model's ability to construct a rigorous, gap-free proof of a theorem, it is, mechanically, improving the same skill needed to prove a sorting function never mis-orders an array, or that a decompression routine always returns the original bytes.

Where AI-assisted formal verification is already shipping

This isn't theoretical anymore. Four examples show verification moving out of research papers and into shipped software.

• Harmonic's Aristotle on code. The same system architecture that reached IMO gold was pointed at VERINA, a benchmark of 189 formal specifications covering algorithms like sorting, longest-increasing-subsequence, and top-k frequency. Aristotle proved 160 of them correct and identified 23 as false by finding counterexamples, resolving 96.8% of the benchmark.⁶
• Microsoft's SymCrypt. Microsoft is rewriting parts of its cryptographic library, used across Windows and Azure, in Rust and proving correctness in Lean via the Aeneas toolchain. Complete, machine-checked proofs already ship for ML-KEM and SHA3, with AI agents speeding up both the translation of cryptographic standards into formal specs and the proof generation itself.⁷
• AWS's Cedar. Amazon built its Cedar authorization language, the engine behind Amazon Verified Permissions, using what it calls "verification-guided development": model the engine in the Dafny language, mathematically prove safety properties like "explicit permit" and "forbid overrides permit," then confirm the production Rust code matches the model using differential random testing at roughly 100 million tests per night.⁸
• zlib in Lean. In an unprompted experiment, a general-purpose AI agent (Claude, with no specialized theorem-proving training) converted the zlib compression library from C into Lean and produced a machine-checked proof that decompression always recovers the original data.⁵

The zlib case is the one worth paying attention to. The other three ran on purpose-built research pipelines. zlib was a general coding agent doing something it wasn't specifically trained for. That's what "the IMO breakthrough spilled over into code" looks like in practice.

Why fast AI code still isn't safe AI code

None of this would matter if AI-generated code were already trustworthy. It isn't.

Microsoft's CEO has said roughly 30% of the company's new code is now AI-generated.⁹ Volume isn't the problem. Correctness is. Veracode tested more than 100 LLMs over four years and found the average security pass rate sits at 56%, essentially flat despite newer, larger models. AI-generated code introduces a known security vulnerability in roughly 45% of tasks.¹⁰¹¹

Anthropic's own C-compiler experiment makes the same point from a different angle. Sixteen parallel Claude agents built a 100,000-line Rust-based C compiler capable of compiling Linux 6.9, for under $20,000, in under two weeks.¹² That's a genuinely impressive feat of speed and scale. It was also explicitly not formally verified, and the team found the compiler had hard-coded values to pass its own test suite rather than generalize correctly.¹² Tests told them the compiler worked. Tests were wrong.

That's the actual gap. Testing and code review build confidence, but they only cover the cases someone thought to check. A proof, by construction, covers every input. AI is now making that kind of proof cheap enough to apply broadly for the first time, which shifts the real bottleneck in software engineering from "can you write a correct implementation" to "can you write a precise specification of what correct means."

How does this change the build vs. buy calculus?

This is where the math breakthroughs land on your desk.

Every build-vs-buy decision is partly a risk decision. You rent SaaS in part because you trust a vendor's QA process more than you trust code your own team, or an AI agent, wrote over a weekend. That trust gap is exactly what a mathematical proof is built to close. Software with a machine-checked correctness proof isn't "probably fine because it passed tests." It's guaranteed correct against its specification, the same way SymCrypt's ML-KEM implementation is, and the same way Cedar's permission logic is.⁷⁸

That reduces the specific risk that has historically favored buying: what if our custom build has a bug the vendor's platform wouldn't. For narrow, well-specified, high-stakes components, that risk premium is starting to shrink toward zero.

The build side is already moving even before verification is widespread. A 2026 Retool survey of 817 builders found 35% of teams have already replaced at least one SaaS tool with a custom AI-built tool, and 78% expect to build more in 2026.¹³ But the same survey shows the caution formal verification is meant to resolve: only 8% of builders deploy AI-generated code without changes, 44% test thoroughly before deploying, and unclear ROI plus security and compliance concerns remain the top blockers to scaling AI-built software into production.¹³ Verification is what could convert that caution into confidence. Owning your internal tools stops being a bet you hope pays off and starts being an asset with a warranty built in, which is the whole premise behind treating software you run as something you own rather than rent.

What this means for your codebase today vs. in 2-3 years

Calibrate your expectations by scope, not by hype.

Usable now:

• Cryptographic primitives and security-critical libraries, following Microsoft's SymCrypt playbook of rewriting in a memory-safe language with a Lean-backed proof.⁷
• Authorization and permissions logic, following AWS's Cedar model of proving safety properties on a formal model and differential-testing the real implementation against it.⁸
• Narrow, well-specified algorithmic code (sorting, search, parsing) where a benchmark like VERINA shows AI-assisted proving already resolves the vast majority of cases.⁶

Still aspirational:

• Full application stacks with UI, business logic, and third-party integrations verified end to end. Nobody has shown this yet, and specifying "correct" for a whole product is a much harder problem than specifying it for a compression algorithm.
• Compiler and systems-software verification at Anthropic's C-compiler scale. That project proved AI can generate a huge, working system fast. It didn't prove the system is correct, and its own authors flagged that gap.¹²
• Any claim that formal verification eliminates the need for testing or review. It changes what testing is for, not whether you need it.

The practical move for most engineering teams right now is to name the two or three components in your stack where a bug is expensive enough to justify the extra rigor, and treat those as the pilot for AI-assisted formal verification, whether you build them with an in-house coding agent or a specialized verification tool. Everything else keeps running on tests and code review, the way it always has, until the tooling matures enough to make broader verification cheap.

The IMO gold medals were the headline. The real story is quieter: the machinery behind them is already inside your build pipeline, whether you've noticed it yet or not.