This is coming next. There's nothing particularly special about theory building. Successful theory building is always oriented towards solving a problem, because otherwise even humans can easily spam out a bunch of nonsense. This is a real problem that the math community has experienced on multiple occasions pre-AI. I'd go further and say that theory building is irrelevant if it doesn't help solve problems people care about.
It's not survivorship bias, because math isn't a bunch of independent, parallel things, where one turned out to be useful and the rest was junk. There is no known way to advance only the portions of math that, centuries later, will turn out to be economically useful. Even with AI, we only know how to advance the entire subject.
You're effectively asking to predict the future hundreds of years in advance. Nobody and nothing can do that. With math, as with all science, you must be willing to accept that not everything will be a hit. There will be misses, and often the same person will generate both hits and misses, because it's fundamentally unpredictable what remains a miss and what doesn't over centuries. The best demonstration of this is that your own thinking here would've banned the invention of calculus: it didn't materially affect daily life for a solid century.
I actually think it's the opposite: Lean proofs and autoformalization make it very easy to announce proofs alongside proofs of the correctness of those proofs (Lean certificates). It's not an absolutely fool-proof combination (the Lean kernel could still contain bugs), but it does immediately attach a very substantial degree of credibility to the result.
And that I think is essential to why some of the world's leading mathematicians are taking this so hard. In a world where we "merely" have AI systems capable of superhuman informal reasoning, verification, correctness, and acceptance could still only be conferred or anointed by human mathematicians. But a world that combines superhuman informal reasoning with superhuman autoformalization is a fundamental shakeup in the institutional order.
The recent proof of Fermats Last Theorem is interesting: it is (iirc) 13 million lines of lean code. And type-checking takes 5 hours or so on a pretty beefy machine. I cannot independently verify the proof, and I have to take Anthropics word for it that it actually type-checks.
That seems like a red herring. Have you independently verified the human generated proof of FLT? Surely someone else will try to verify Anthropic's formalization on different hardware. Plus, it seems likely that FLT formalizations will improve / get shorter over time, requiring less compute. And computers (and type-checkers) will continue to get faster over time as well. So maybe in 5 years you could own a computer fast enough to verify a/the proof in say a week, instead of 5 hours.
It'd cost you $30-$50 on AWS for a clean Lean build or maybe $100-$150 for the full verification suite. You are, in fact, capable of independently verifying the proof yourself if you don't trust all the people who've already done so.
None of these incidents involve single instances of commercially or publicly available systems. They all involve large swarms of internal models. The stuff you're describing is not the research frontier. It's really not even close.
I think it's easy to infer that alignment of a single model does not clearly transfer over to alignment of a swarm of thousands of copies. Moreover, we're also seeing clearly that large swarms also unlock a step function change in capability, as a swarm can act like a complete research institution, spending thousands or millions of subjective hours of wall-clock thinking time just to deceive a single evaluator or crack a single math problem or design a single cyberattack.
The work is either: (1) the act of concealment: generating an AI book that cannot be detected as AI generated; or (2) actually just writing the book yourself.
It's easy to come up with new open problems. It's hard to come up with new open problems that seem to teach us something fundamentally new about the world. Our current batch of problems went through a complex selection process over decades (or centuries) based not purely on difficulty but also on perceived insightfulness.
I studied math, but I am not a mathematician, so I think I have a slightly different perspective on this than Tao overall. This is certainly the definitive end of an era in mathematics, but I think he's wrong that insightful new open problems are truly non-renewable. They might be non-renewable by humans at the rate at which they are being closed, but I see no reason why AI systems could not also discover insightful new open problems. In fact, once we have Riemann-capable AI mathematicians, I'd personally love to see what the next Riemann hypothesis is, which even these AI systems cannot solve with any amount of available compute.
I think we're about to find that, on the spectrum of mathematical intelligence, the best human mathematicians were only a fraction of a percent forward from the very beginning, and there's a vast universe of mathematical depth that's beyond our ability to imagine or work on directly in any way. We're used to feeling like we're able to directly perceive the Platonic realm, but we're almost certainly going to discover that our own minds, even when joined together over centuries of deliberation, can only interact with a tiny little shadow within it.
I haven’t been following the AI proof stuff very closely, but the impression I got was that these models are producing massive Lean programs that prove the statement one way or another, but are quite difficult to fully understand.
Actually, I have to admit I don’t really know what math is. With physics we suspect there’s a universe, and when we study physics we’re improving our description of the behavior of that universe, right? The universe exists whether or not we know how it works.
Eventually, as you suggest, maybe we’ll hit math that won’t fit in anybody’s head at all. What is the nature of mathematics that doesn’t fit in any human’s head? Does it even exist in some sense?
I think math is compressible structure. That's why we care about something like the Riemann hypothesis but, to use Tao's example, we really couldn't care less about computing the 10^10^10th digit of pi. The first compresses a vast amount of information about the primes, while the second decompresses information that we've already compressed (a few lines of code can define every digit of pi).
Most patterns that exist are incompressible. Math is basically a search for those compressions that do exist. An example I personally really like is the amplituhedron: a geometric structure that humans have just barely been capable of recognizing compresses information about scattering amplitudes and Feynman diagrams. That one happens to be within our reach, but it's right at the edge, and we can only imagine what glorious, wondrous compressions exist in abundance beyond the edge. Math accessible only to superintelligence would exist entirely beyond that edge, compressing patterns whose existence we cannot even detect using objects and constructions that we cannot grasp.
As an aside, I also think this is why AI is quickly becoming superhuman at math: intelligence is essentially a form of pattern compression.
I think part of mathematics is taking things that don't fit in our head and giving them human abstractions so they can.
Take infinity. Infinity can't fit in your head, hell, it can't fit anywhere, but you can abstract away the endlessness and look at infinities of different sizes, et al.
Now, is there a single formula for something actually represented in this world that would take most of a humans life just to read it, no idea.
The models produce both Lean code for formal verification and a traditional-style narrative proof. Like the general long-form output of frontier models, the math papers produced appear to be generally correct technically, but written in an ungraceful and sometimes hard-to-follow style, so they are often polished by a human mathematician as of today.
What you are saying implies that by some technique that hasn't been discovered yet, we can make the models to have the capabilities of extrapolate the information they are trained on and also interpret that what they are extrapolating are Riemann-capable hypothesis.
I do believe it will accelerate the discovery of that "vast universe of mathematical depth that's beyond our ability" but at the cost of removing the "fun part" of solving the problems. Not sure if the community is willing to do that.
What's just as interesting is this morning Axiom Math announced 212 and OpenAI then appears to have rushed out their 186 announcement just 1-2 hours later followed by Astra. Did they accelerate the release of Astra itself? Not necessarily, but it definitely looks like they ended up pushing much harder and faster than planned on their 186 result. X activity suggests Anthropic had a similar result as well but wasn't as fast as OpenAI in packaging it up and sharing it in response to Axiom, so they mostly just bolted onto OpenAI's messaging.
The reason I think this is interesting is that Axiom is a tiny lab in comparison that wouldn't have had access to Astra at all. I'd be curious to learn how Axiom is able to effectively compete at this frontier with vastly fewer resources.
My most controversial opinion by far in tech circles is that I still just use a standard Windows gaming PC as my home desktop. My current machine I just bought pre-built from Microcenter, complete with a 5090 and everything.
I can fire up a Linux terminal with WezTerm and WSL2 at any point. It's customized and beautiful and totally fine. I have Codex running in one right now. I can listen to Dolby Atmos music through Apple Music or fire up a game with zero compatibility issues and full RTX support. It's just versatile like nothing else. I pair it with a gigantic 48" LG OLED TV as my monitor.
The only thing that might tempt me away from this is a fully loaded Mac Studio with 512GB of unified memory. That would be a real capability gap from my current machine. But I've contemplated wiping Windows and installing Omarchy, and I just can't figure out really what I'd gain, but what I'd lose is quite clear.
Windows has also come a long way from a terminal perspective. Sure, the UI is a bit of a mess, but Powershell can do anything in the UI from the command line, and agents are very capable with PoSH. If you really care about ricing the UI, there's hundreds of utility apps to do almost anything you want.
Agents are also able to tweak and debug Windows errors, since the registry, group policy, event log, and other Windows internals have been largely unchanged for 25+ years and are well documented. All have old command line tools or modern Powershell to manage.
you have to understand that 90% of HN use macs and the only time they see windows is once every 5 years when a relative asks to setup a new or clean an infected one
The rank of a rational elliptic curve can be seen as a measure of how complex its arithmetic structure is. Roughly speaking, you can imagine that a curve of rank r has a substructure of dimension r. So a curve with a high rank is a pretty exotic object. This curve here has a 30-dimensional (or greater) lattice substructure. You can think of it as being possible to arrange the rational points on this curve into a predictable structure in a vector space of dimension at least 30. In that space, there would be at least thirty independent directions in space that could be combined together to produce distinct rational points on the curve.
To really quantify how exotic, it's conjectured that curves with rank 2 or greater have an asymptotic density of zero. That doesn't mean they don't or can't exist, but it does mean they become vanishingly rare, so finding even individual examples of high-rank curves has been absurdly hard.
It's not really quite that simple. You wouldn't hire Jeff Dean to do bug fixes in your mobile app. I'm sure he's capable, but I honestly doubt he'd stay interested and focused on it enough to really do a good job. That doesn't mean he's not a superstar.
What it comes down to is that there are different types of high performance. Some people are good at just executing tasks given by their manager. Some people are good at being generative, thinking across boundaries, acting autonomously, creating value without direction, etc. A term like "superstar" will get disproportionately applied to someone really good at the latter and rarely someone really good at the former, because the potential impact of the former is typically strictly capped, while the latter is uncapped.
reply