Intuition as Compressed Verification
Recently, mathematicians have found themselves to be some of the first intellectual workers to be disrupted by AI. A field that many consider to be the pinnacle of human intelligence is now at risk of being washed away.
Have you ever been humbled by a topology or abstract algebra midterm, or spent hours staring at a problem when someone else intuited the solution just by glancing at it?
There is a certain level of "genius" that you have no choice but to appreciate. Some people just see things. They might not see the solution immediately, but they see the path, or think that some path is likely to work out. This internal world model for prediction is developed through a lifetime of scrubbing problems, aka experience, which allows them to reduce the cost of search for a solution (in theory).
However, with Lean, AI's cost of search is reduced at an even greater magnitude. It can verify things in a matter of seconds, whereas mathematicians may take hours to weeks. Certainly, on this second axis, AI outperforms mathematicians.
Let's give humans the benefit of the doubt, and say that intuition is much stronger than the reasoning chains that AI can produce from its vast training data. 1-1, right?
But there is a third axis: scaling. A single mathematician, constrained by mental energy, time, and caffeine, faces the prospect of competing against thousands of AI agents, a "fleet" or "swarm", which can explore different approaches in parallel. With tools like Lean, the agents can continuously test their approaches and reasoning magnitudes of more times than a human mathematician. The sheer volume and speed of iteration triumphs over human intuition.
"But hold on," the reader objects, "Some of the problems that have been solved have been done without Lean!"
This is true. Lean is not the primary driver; in fact, with Navier-Stokes, OpenAI spent approx. 10,000 agents exploring the problem, then generated proposed solution in 88 hours, and then spent another 17 hours formalizing and verifying it.
In fact, AI scales the entire mathematical process. The central advantage, is not that it can only verify faster, but that things scale cheaply (relative to the physical world, as tokens are much cheaper and more reliable than human willpower and cortisol). Math itself is vulnerable because it has unusually strong verification mechanisms (both formal and informal).
Now, let's move on from math. Certainly, there are other intellectual fields (scientific research, software) which are also susceptible to AI disruption. But these require longer and/or more expensive verification loops. If you assume generation is not the bottleneck (a valid assumption, given the "AI slop" you see in articles and codebases nowadays), then AI is bottlenecked by either time or resources (compute, money, wetlab machines).
More importantly, the data needed to develop intuition isn't equally accessible across all of these fields. Longer loops mean you have less data, less decision points, and therefore lower chance of "sight" of patterns. The learning signal is especially scarce where you have uncertainty.
All of this is still without moving into the physical world. As taken from my substack on Moravec's Paradox:
Part of the reason AI seems so daunting is that tasks which are easy to us (mobility, dexterity), are taken for granted. They are such vital aspects of our daily life that don’t require a shred of cognitive thought. Imagine this: suppose we were thinking machines just as artificial intelligence is now, and were not able to interact with the physical world (and if we were, only on a very limited basis via robot dogs, Waymos, and the sort). The value of movement and perception would skyrocket! Many of us “knowledge workers”, deprived of touch and sensation, would pay a king’s ransom for the scarce ability to physically manipulate the world through environmental interaction.
We confuse abundance with simplicity. Because nearly every able-bodied adult can walk across a room, open a refrigerator, and pour a glass of water, these actions are considered trivial. But this hides the physical complexity. If only one person in a thousand could physically manipulate the world, hand dexterity would not be considered menial, but rather, a superpower.
Now, since I wrote this, robots have made remarkable progress, moving into factories and physical tasks, and foundational models have become more capable at generalizing across these tasks at few-shot. There are two reasons: 1) robots are being used to do repeatable tasks, and 2) part of this advance is because robot training and testing is increasingly being done in simulated environments. Training in simulation is both cheap and has a shorter loop. The fixed cost of creating a good simulation is very much worth it when compared to the cost of real-environment training.
The fundamental bottleneck has always been the cost of experience, and now, it is being removed. Obviously a simulation isn't exact verification like Lean (sim-to-real gap), and this has been known and done since 2017. Most of the recent advances have been scaling (GPU-accelerated parallel frameworks), as well as just quality improvements (better physics engines, better rendering, sensor modeling, etc.)
Intuition has always been scarce because experience is always expensive. Every person only has one lifetime to develop intuition. This limits how many "experiments", "proofs", "prototypes" people can run.
In a sense, intuition is compressed verification: the accumulated outcomes of past experiences, distilled into a single prediction or inkling.
But what happens when verification itself becomes cheap?
When thousands of agents can explore millions of possibilities in parallel, the previously-large advantage of knowing which path to take is much smaller. Computation, iteration, and feedback starts to replace intuition.
Obviously, intuition isn't useless. The search space of solutions, if high-dimensional, is massive. Even machines need to know where to look. But the economics of intelligence have definitely changed. You just need to know what paths to look at in general, or have a general idea of which paths to look at, then send your agent fleet to explore all subpaths of those, instead of needing to do so and refine things yourself.
We will soon have abundant intelligence, both capable and cheap. This brings us back to Moravec's Paradox, but in reverse: we might begin to take intelligence for granted just as we have always taken basic physical abilities for granted.