The Machine Found the Answer. Now Who Can Read It.

In October 2025, Boris Alexeev and Dustin Mixon showed that this little set does away with a conjecture Paul Erdős posed for two decades and put a $1,000 prize on. It is a Sidon set, a collection of integers whose pairwise differences never repeat, and it cannot be extended to a finite perfect difference set. The human insight is actually fairly short.

To be sure of the result, they formalized the argument in Lean using ChatGPT to actually write it. A formally checked proof spanning thousands of lines was used to confirm a fact you can explain in a paragraph.

This illustrates a growing gap in AI-driven discovery: the distance between verifying a result and understanding it.

Yes, mathematicians must still check the assumptions and the like, but even a verified argument can leave readers struggling to see the main ideas that make it work.

I tell my students to verify AI outputs, but verification is not the difficult part. A machine can hand you a result, which you can check and still not understand. Perhaps you get a result that answers a somewhat different question from the one you asked.

The interesting question is no longer whether AI can find the answer, it's what we're supposed to do once it hands us one.

Intelligence is search, plus the map in which you searched

Few people agree on what intelligence is. The Turing Test is a workaround. It essentially says, I'll know it when I see it. The definition I keep coming back to is from Douglas Lenat and Edward Feigenbaum, in their 1987 paper "On the Thresholds of Knowledge":

"Intelligence is the power to rapidly find an adequate solution in what appears a priori (to observers) to be an immense search space." D. Lenat and E. Feigenbaum

Underneath the marketing hype, a lot of AI really fits into this. A chess move, a weight configuration, the next action an agent takes: you stand in a vast space with a goal in mind, looking for one path and ignoring most of the rest. No one brute-forces the games of chess or Go. In the case of Go, there are more board positions than observable atoms in the universe. Complete computation is not even theoretically possible. A better heuristic gives you assurance that you don't need to look in most places.

When I say "AI is search," I should distinguish between three separate processes.

• During training, optimization searches a space of possible model parameters.
• An agent may search more explicitly, proposing actions, testing them, and using the results to decide what to try next.
• A trained neural network can produce an output in a single forward pass without explicitly exploring alternative answers. It applies what training has built into its parameters.

These processes are related, but not all pure "search." The concept helps us ask what possibilities a system explores, what guides it, and how it evaluates success. For example, an agent's tools and instructions shape which actions it can consider. Search is a valuable capability, but so is the map in which it operates. If the map is wrong, search will happily find a great solution to the wrong problem.

The representation matters as much as the exploration. Following the definition in their paper, Lenat and Feigenbaum's Knowledge Principle (KP) says a system looks intelligent largely because of the specific knowledge it can bring to bear: concepts, representations, methods, heuristics.

This general search framing has held up for a few years. What I did not expect was how quickly the results would stop being reassuring.

Vibe proofing: Verification is not an explanation

On September 8, 2026, OpenAI announced that an internal system had produced a proposed resolution of the Navier–Stokes existence and smoothness problem, one of the Clay Millennium Prize Problems. The claim: a three-dimensional incompressible fluid, starting from rest and driven by a smooth external force, can develop unbounded velocity in finite time while its total kinetic energy stays bounded. The claimed result establishes statements C and D in Charles Fefferman's official formulation, while leaving the unforced regularity question open.

The scale is my focal point here. On the order of 10,000 concurrent agents, working an internal model OpenAI described as more capable than GPT-6 Astra, reached the result on September 5, about 88 hours after launch. Lean formalization and verification took another 17 hours. OpenAI reported about 2.7 million agent messages and 130 billion output tokens on this problem alone. The writeup runs over a hundred pages. The Lean development includes hundreds of thousands of lines. Clay later said the problem had "apparently been settled," and that its evaluation would be deliberately unhurried. OpenAI said it would not claim the prize.

Ironically, the discovery process has now become a challenge. An enormous record of agent messages is not the same as a useful explanation of how to find the solution.

Human mathematicians reorganize their arguments after finding them. The question is whether the resulting account helps someone recognize the mechanism, reuse the method, or see where to look next.

As part of the follow-up, Ramani Duraiswami recognized the construction's swirling core as an idea related to a solution he and Nail Gumerov found way back in 1998. From September 12 to 15 he worked with Claude examining the possible connection and later wrote about it. Other mathematicians identified conditions under which constructions with those features cannot yield unforced blowup.

Truly understanding a proof (or research in general) includes understanding the bounds of where it stops.

I expect to see much more of this pattern.

• Search delivers verified results faster than a field can absorb them.
• Turning knowledge into understanding is a separate job, one left to humans, albeit performed with AI assistance.
• Understanding is a slower process that compresses research into ideas you can grasp in your mind and reason about.

The distinction has been around for a while now. In 1976 Kenneth Appel and Wolfgang Haken proved the Four Color Theorem with a computer enumeration of nearly two thousand configurations, and mathematicians argued about what it means to accept a proof you cannot check by hand. What changed is who finds the argument.

In late 2025 Alexeev selected several Erdős problems, launched Harmonic's Aristotle system, and went to bed. He woke up to read an email that Aristotle had solved Problem 124. The details matter here though. Aristotle had solved an easier, later formulation, not the harder original question.

Thomas Bloom, who curates the Erdős problems database, noted that while the AI's proof was almost certainly the simplest possible for that specific statement, it was not a true "proof from the Book". His test is whether a proof has surprise and revelation, and whether he can tell himself a plausible story of how he would have found it. For 124, he could: the obvious inductive argument that generalizes base 2, reduced to one inequality, which happens to hold.

So what do we learn from a machine-generated proof, what has come to be known as Vibe Proofing? A proof shows a logical conclusion, but there is still work to be done after that.

Much of "discovery" is retrieval

Once people pointed models at the Erdős catalog, a number of problems marked "open" turned out to have been solved decades earlier and forgotten. Problem 707 is a case in point. The answer existed, but it was hiding in a 1947 paper nobody had cross-referenced. In this case, Alexeev and Mixon report that LLMs failed to locate Hall's result, even with substantial prompting. They found the paper accidentally during another literature search.

In October 2025, UCLA's Ernest Ryu used GPT-5 on a question about Nesterov's accelerated gradient that had sat open since 1983. He did not describe a machine inventing mathematics. He described a machine that kept trying odd moves, pulling techniques from adjacent fields, proposing and discarding variations faster than he could. Most of what it produced was wrong. This feels much like my research today using AI.

Ryu checked every step. Twelve hours over three days and an incorrect but helpful structural suggestion later, he built the proof. GPT-5 is noted in the abstract of the preprint, it is not a co-author. Ryu was the outer loop.

• The machine is a fast search engine with a weaker sense of what matters.
• The human is a slow search engine with (hopefully) good sense.

The model found the line of code. A human still has to know why.

In May 2025, security researcher Sean Heelan gave OpenAI's o3 model roughly 12,000 lines of the Linux kernel's ksmbd SMB server and asked it to look for use-after-free bugs. In one of 100 runs on that larger context, it described a real one: in the session-logoff handler, one thread could free an object another thread was still using. Heelan recognized the report, confirmed it, and disclosed it. That became CVE-2025–37899, a publicly documented Linux kernel zero-day found with an LLM.

The numbers people repeat though are from a different experiment. On a smaller context, o3 found a known Kerberos authentication bug in 8 of 100 runs, with other runs exhibiting numerous false positives and missed detections. Heelan put the signal-to-noise near 1:50. That is not a system that inherently knows where the bug is. It is a noisy heuristic search over a space a human already chose, aimed at a type of bug humans already named.

Our job is to separate out the real bits, separate fact from fiction, and understand what broke and why. The model can point at a line, but a patch needs the reason.

The same cybersecurity engine is available to whoever runs it. A defender (cybersecurity professional or ethical hacker) who searches first and understands fastest wins, but unfortunately, so can an attacker (or malicious user).

Where the framing breaks down

My thesis of "AI is search" is not perfect, and I'll be the first to point that out. One-shot learning and emergent "intelligence" still require a good deal of research to fully understand. Search wants iterations, yet a child learns "giraffe" from one picture. If intelligence is navigation of an immense space, humans arrive at it absurdly fast, often times with very little data. The background that we bring before we start looking is doing some heavy lifting. This is the Knowledge Principle in action.

Where do we go from here

Historically, the hard part was finding an adequate answer in a large solution space. What changed is that, in some domains, machines can return answers faster than we can absorb them, especially if strong verifiers exist. That is the case in mathematics and coding, to name a few areas where we have seen rapid progress recently.

Computer science gives us a familiar distinction: finding a solution can be much harder than checking one. P versus NP asks whether every problem whose proposed solutions can be verified in polynomial time can also be solved in polynomial time. AI has not overturned that question. But AI-generated proofs highlight another distinction: a machine may check an argument faster than a person can understand its significance. Verification can establish that the steps hold together without making the underlying idea clear.

The cybersecurity example shows that someone still has to separate real vulnerabilities from plausible false alarms. Finding a candidate, verifying it, and understanding it remain distinct jobs, and any one of them can be the bottleneck.

AI changes the balance of effort. As search becomes faster, more of our work may shift toward checking that we asked the right question, evaluating what came back, and turning a valid result into knowledge we can use.

We remain the outer loop. Our role is to judge when verification is sufficient, when further investigation is needed, and what the answer actually teaches us.

Will we keep investing in our part of the work as answers arrive faster? As an analogy, how much of AI generated software/code is still reviewed line-by-line by humans?

It has become difficult for people to keep up with the speed of generation. Will we settle for knowing that something is true without understanding what makes it true?