The Verifier Decides: Why AI Broke Through in Mathematics and Stalled in Music

Leftover from the last post

In what AI changed in music I wrote that as of 2026 there is no single discovery you could point to and say AI solved a long-standing mystery. After publishing it, the obvious question nagged at me.

What about every other field?

There are such discoveries. Dramatically so. And the interesting part is that the gap doesn’t correlate with how intellectually hard the field is.

In mathematics, problems are actually falling

In May 2026, DeepMind’s AlphaProof Nexus autonomously solved 9 of the 353 Erdős problems it attempted. Two of them had been open for 56 years. Inference cost: a few hundred dollars per problem.

Since October 2025, AI has cleared roughly a hundred of Erdős’s open problems. An OpenAI model toppled an eighty-year-old geometry conjecture; a 23-year-old settled a sixty-year-old problem with a single chatbot prompt. AxiomProver solved all twelve problems on the 2026 Putnam, eight of them within the official contest time.

Mathematics is hard. And mathematics is where AI’s results are most spectacular.

The things that quietly went to production

• Weather — ECMWF put AIFS into operations in February 2025, with the ensemble version in July; NOAA followed in January 2026. The first large-scale case of machine learning replacing physical simulation in production, at an order-of-magnitude lower compute cost
• Materials — DeepMind’s GNoME predicted ~2.2 million candidate structures and flagged ~380,000 as stable. By the time of the Nature paper, outside labs had physically synthesized 736 of them
• Fusion — Princeton demonstrated AI controlling plasma on millisecond timescales, far faster than a human operator can react
• Autonomous driving — Waymo runs 150,000+ weekly rides across four US cities. Baidu’s Apollo Go operates in 10+ Chinese cities with over 10 million cumulative rides
• Drug discovery — As of July 2026, 117 AI-derived therapeutic assets across 63 companies have entered human trials. But only 8 have completed Phase 2, and no fully AI-designed drug has FDA approval

Weather is the least discussed and the most widely used. The machinery behind everyone’s daily forecast got swapped out and almost nobody noticed.

Meanwhile, inside companies

• Gartner (April 2026) — only 28% of AI projects fully achieved ROI; 20% failed outright
• RAND — over 80% never reach production, with data quality the leading cause
• BCG — 74% of adopters can’t scale past a successful PoC
• A meta-analysis of 106 studies — human–AI combinations perform worse on average than humans alone

That last one is the striking one. It feels like it’s working, and the measurement says otherwise.

What lining them up revealed

Mathematics is hard. Enterprise operations are, at minimum, easier than mathematics. The results run the other way. Difficulty doesn’t explain it.

What the successful fields share is three conditions:

1. There is a verifier — correctness can be judged mechanically and objectively
2. There is structured data at scale
3. The bottleneck was the number of attempts — human throughput of trials was the limit

The first one is decisive.

Field	Verifier	Time to a verdict
Mathematics	Lean and other proof assistants	Seconds to minutes
Plasma control	Does the machine stay stable	Milliseconds
Weather	Tomorrow’s actual atmosphere	One day
Materials	Can it actually be synthesized	Weeks to months
Drug discovery	Clinical trials	Years
Music (generation, performance judging)	None	—
Management decisions, education	None (and where proxies exist, slow and confounded)	—

Lean returns a verdict in seconds, so mathematics became AI’s playground. Clinical trials take years, so drug discovery stops at “faster.” What sets the pace is not how smart the AI is — it’s how fast and cheap the verifier is.

The cost of a wrong answer goes to zero

Why does a verifier matter this much? Three reasons, I think.

1. Wrong answers become free. A proof Lean accepts is correct. If the AI emits 999 wrong proofs and one right one, you throw the 999 away. Low generation quality is survivable, because brute force works.

Without a verifier, a human pays the cost of sorting out the wrong ones. The more the AI produces, the more work the human has. That’s probably what the 106-study meta-analysis is measuring.

2. The self-improvement loop closes. The verifier’s verdict is a training signal, so capability rises without hand-labeled data. AlphaProof, plasma control, Go and shogi — all the same shape.

3. Truth stops being negotiable. Generative music and enterprise AI are precisely where this fails. Nobody can adjudicate “is this a good song” or “did this help,” so the argument moves to courtrooms and internal politics.

Music turned out to be the clean example

Reread the previous post through this lens and it closes neatly.

Source separation and transcription had verifiers. A separated stem can be compared against the original stem. A transcription can be compared against Disklavier MIDI. That’s why they reached practical quality.

Generation and performance judging have no verifier. No machine adjudicates “good song” or “good playing.” So it never became a technical conversation; it became a conversation about ownership.

Within one field, only the side with a verifier moved. Music is the best illustration of the claim I’m making.

Verifiers come in four kinds

Kind	Examples	Character
Formal verification	Lean, type checking, model checking	Fast, cheap, certain. Narrow applicability
Physical experiment	Synthesis, clinical trials, road testing	Certain but slow and expensive
Nature answering back	Tomorrow’s weather, market prices	Fast and cheap, but you have to wait
Diff against a reference	Original stems, an existing implementation’s output	The reference’s quality is the ceiling

Source separation and transcription are the fourth kind. A reference existed — that is exactly why the separating side of music moved.

This is also a question about my own work

Building a language makes this personal. I decide whether to advance based on whether the gates are green, so the quality of my verifiers is the quality of the work.

But as I wrote in fifteen green gates and the question none of them asked, having a verifier isn’t sufficient. What it asks matters just as much. All green, and the unasked question is still sitting there.

Back at the level of fields, this becomes: can we build verifiers where there are none? Self-driving labs are exactly that attempt — taking the slow, expensive verifier of physical experiment and making it fast and cheap through robotics. Environments like CMU’s Materials Innovation Cloud Lab are coming online.

And conversely: where a verifier can’t be designed, this shape persists. Art, education, management judgment, and care work all live there.

So, in the end

AI produced revolutions not in “intellectual” fields but in fields where you can check the answer. Mathematics leads not because it’s hard, but because proofs are machine-checkable.

Which means there’s one question worth asking when you’re unsure.

Is there a way to confirm this work is correct without a human judging it?

If yes, AI is worth deploying. If no, use AI to increase the number of candidates rather than the speed, and decide up front who pays the cost of sorting them.

Back at the piano: recording your own playing as MIDI and aligning it against the score is building yourself a verifier. Machines can help that far. Past it — whether the playing is musically good — nobody has a verifier yet.