Friends & Investors Engineers Technical Investors

The Academic Parallel

Mathematics had the same problem. Terence Tao solved it. We're applying the same approach to software.

The Bottleneck Shift

Mathematics Had the Same Problem

AI compressed every "generative" phase of academic research. What remained? The tasks that require trust and verification.

Pre-AI Research Workflow 100% of time
Post-AI Research (2025) ~43% of original time
Rescale to 100% — see what dominates now

AI made generating research cheap. The bottleneck shifted to verification — peer review.

The Breakthrough

Tao's Insight

AI has driven the cost of idea generation down to almost zero, in a very similar way to how the internet drove the cost of communication down to almost zero. Now the bottleneck is different. People can generate thousands of theories for a given scientific problem. Now we have to verify them, evaluate them.

— Terence Tao, Fields Medal laureate

His solution: replace social trust with mechanical verification. Here's how it works:

1
Formal Verification Replaces Social Trust
▼

Traditional peer review: you trust the reviewer's expertise. Your collaboration is limited to ~5 people because you must personally verify each person's work. Trust doesn't scale.

Formalization (Lean): the proof assistant checks correctness mechanically. As Tao put it: "You don't need the same level of trust" when the system checks every step.

The result: The PFR project — a major conjecture — was compiled and verified in half an hour. The equational theories project achieved 99.9963% completion in just 19 days with crowdsourced contributions from strangers around the world.

2
Decoupling Conceptual from Technical Skill
▼

Formalization separates concerns: some people focus on mathematical direction, others specialize in turning pieces into formal proofs, others build automation tooling.

As Tao describes it: "Not everyone needs to be a programmer — some can focus on mathematical direction."

This enables massive parallelization of what was previously serial expert work. The equational theories project had dozens of contributors, none of whom needed to understand the full picture — only their piece, verified by the system.

3
The Quality Flywheel
▼

Each formalized result becomes a building block for future work. Proofs compose: theorem A + theorem B → theorem C, all machine-verified.

The mathematical knowledge base grows with mechanical guarantees. Every new theorem can safely build on every previous one.

There's no "trust chain" that degrades with length. In traditional math, citing a paper that cites a paper that cites a paper introduces compounding uncertainty. In formalized math, every link in the chain has been mechanically checked.

The Comparison

What Peer Review Achieves — and How Formal Methods Achieve the Same

Every function of peer review has a formal-methods equivalent. The difference: one scales, the other doesn't.

What Peer Review Does Traditional Approach Formal Methods Approach
Correctness guarantee Reviewer re-derives the argument Proof assistant checks every step mechanically
Reproducibility Other researchers replicate results Proof compiles deterministically from source
Error catching Human spot-checking, intuition Static analysis across ALL possible cases
Building on prior work Citation + trust chain Import proven theorem, compose with new proof
Social trust / reputation "Published in Nature" "Verified by Lean" — trust is mathematical, not social
Scalability ~5 trusted collaborators max Unlimited — anyone can contribute, system verifies
The Mapping

Software Is the Same Pattern

The parallels aren't metaphorical. They're structural. Every concept maps 1-to-1.

Mathematics Software
Mathematical proof Property / invariant over code
Proof in Lean Property verified by AG framework
Peer review Code review / security audit / compliance check
Theorem Invariant (e.g., "no SQL injection possible")
Proof assistant (Lean) AG framework + abstract interpreter
Formalization (annotating a proof) Annotation / attribute declaration in code
Crowdsourced contributors AI agents generating annotations
Proof compilation (Lean checks) AG evaluation (framework verifies)
Library of proven theorems Library of proven code properties
Evidence

The Results Are Already Coming In

Formal verification isn't theoretical anymore. It's shipping in production.

Mathematics

Lean + Crowdsource
PFR Conjecture

Formalized in Lean, verified mechanically. What would have taken years of peer review was checked in half an hour.

Lean + Crowdsource
Equational Theories

22 million implications, 99.9963% verified in 19 days. Crowdsourced from contributors worldwide.

AI + Formal Verification
Fields Medal Proof

AI-human collaboration formally verified sphere-packing proof for the first time — a landmark in mathematical trust.

Software (Precedents)

Rust Language
Ownership Model

The compiler proves memory safety. No garbage collector, no manual review needed. Formal verification going mainstream.

NICTA / General Dynamics
seL4 Microkernel

Fully formally verified OS kernel. Zero exploitable bugs found in production.

INRIA
CompCert

Formally verified C compiler. Proved to never miscompile. Used in safety-critical aviation and nuclear systems.

Formal verification isn't theoretical anymore. It's shipping in production. The question isn't will it come to mainstream software development — it's who builds the infrastructure.

The Missing Piece

The Key Difference: AI Agents

Tao's formalization projects required skilled humans to write the Lean proofs. That's still a bottleneck — just a different one.

The breakthrough for software: AI agents can generate the annotations. They do the "creative" part (deciding what to assert) cheaply and at scale. The framework does the "verification" part (checking the assertion holds) mechanically.

This is the missing piece that makes formal methods practical for everyday software development.

Want the deep technical version? See The Sudoku Insight →