In my last post, I mentioned that I’d been following Analysis I (fourth edition, 2022) by Terry Tao. This is a lovely book on real analysis (basically, the theory of calculus) based on an honors analysis course Tao taught at UCLA in 2003. In this post, I’ll briefly discuss some of the book’s features, and then show how recent developments related to the text tie into a more current topic, namely, math and AI.
1 Real analysis
As part of my math learning project, I’ve already covered several aspects of real analysis, but the time had come to read a book dedicated to the subject. I originally started with Understanding Analysis by Stephen Abbott,1 an excellent book that is good at building intuition, especially for the pathological examples that largely motivated putting calculus on rigorous foundations. But by design, Understanding Analysis (like most modern analysis texts) skips the up-front cost of defining things like the real numbers rigorously. One consequence is that it is sometimes difficult to know what we are allowed to assume and what we must prove. Since I was most interested in foundational understanding, this led to a constant battle against circular reasoning.
Analysis I avoids this problem entirely. Instead, it starts with the Peano axioms of arithmetic and the axioms of set theory and builds analysis “from scratch”. This takes more time initially, but (as Tao mentions in the foreword) the facility with abstraction means you can move more quickly later on. (Or at least so Tao claims; I don’t know if there’s been a properly controlled study on the subject.) In any case, I’ve generally found the approach well-suited to my own style of learning, and I consider the book a great success.
One recent addition to the text, added only last year, is a Lean companion to Analysis I, which translates parts of the book’s proofs into the Lean proof assistant language, while also adding some exercises in Lean. The result is well-aligned with recent developments in proof formalization, which involves writing mathematical proofs in a form that can be executed directly by a computer. This gives much greater confidence that the result is correct (although it’s not 100%, since among other things the formalization language itself might have bugs).
2 Math and AI
Proof formalization has played a key role in the burgeoning field of AI and math, in which artificial intelligence systems frequently include “Lean certificates” demonstrating the correctness of the result. Tao himself has been an active participant, including giving frequent talks on the subject. For example, last year I was lucky enough to see a private talk Tao gave on proof formalization to the RAND Corporation. And last week I was in attendance at Tao’s public lecture “Math 2.0” at Caltech2 (my own graduate school alma mater), which addressed the broader subject of math and AI.
Attending Tao’s Caltech talk felt like being a part of history, since it came only a few days after OpenAI dropped claimed solutions to an astonishing \( \sim 372 \) open problems in mathematics,3 the result of pointing an internal development model at a list of around \( 4000 \) such problems. This came hot on the heels of OpenAI’s claimed solution of the Navier–Stokes problem, one of seven Millennium Prize Problems considered to be among the most difficult and important problems in mathematics. (Until this year, only one had been solved: the Poincaré conjecture.) And over the summer, a mathematician at Anthropic,4 makers of Claude AI, casually tweeted out a counterexample to another important open problem, the Jacobian conjecture. (Terry Tao’s ChatGPT session makes particularly interesting reading on this one.)
Although some might object that producing \( \sim 372 \) solutions out of \( 4000 \) problems represents a batting average of “only” \( \sim 9\% \) (a point Tao somewhat enigmatically made in his Caltech talk), by the same standard OpenAI cracked “only” \( 1/6 = 16.7\% \) of the open Millennium Prize Problems. These were major open problems, and many of the OpenAI results (including of course Navier–Stokes) would be signature career accomplishments for most human mathematicians. Moreover, the results from the main OpenAI drop were produced with only an average of three hours per problem. This is an astonishing development given that AI models first achieved gold-medal performance on the hard but still high-school-level International Mathematical Olympiad only last year.
Most knowledgeable observers agree that these trends are only going to accelerate. It’s hard to argue the contrary in light of stats like the ones in this recent post from Anthropic:
In May 2026, Anthropic averaged around 2,500 code changes merged per day; as of September, we merged over 30,000 per day. We don’t expect this rate of growth to slow down anytime soon; the latent demand for merging code is practically infinite, and every bottleneck we remove immediately leads to a further increase in the amount of code we produce.
In short, current frontier AI models are already solving problems at least at the level of a first-rate human mathematician, and they’re getting better fast. It’s clear that mathematical superintelligence is upon us.
3 Math learning project
So where does this leave my math learning project? The pace of change in AI has caught many mathematicians unawares, with many expressing sadness at or even hostility to the stunning developments. Fortunately for me, I always approached this project in large part as one of intellectual gratification, and AI doesn’t change that; if anything, it’s an unprecedented learning resource. It’s true that my math project was also aimed at possible theoretical physics research, and AI is clearly coming for theoretical physics as well.5 But AI physicists could be a great boon for anyone who wants to ask the really deep questions, since in effect all technical barriers are falling to AI.
When thinking through the implications, I’ve concluded that AI opens up a lot of projects that would have been too difficult or tedious even a year ago. Given the many possibilities, I’ve decided to wind down my math learning project per se and open the field to nontechnical subjects as well. I’m not sure which direction I’ll go, but I’m going to have fun exploring.
Since my AI-aided activities may include subjects outside of math and physics, I’m planning to make fewer posts to my original Substack email list, with a focus on announcements directly related to Tau Day and The Tau Manifesto. As part of this transition, the canonical URL for the original list has changed to posts.tauday.com (and, unless there are any objections, I’ll be turning off the paid tiers). I haven’t decided yet if I’m going to make any posts on other subjects, but in case I do I’ve created a more general email list at posts.michaelhartl.com. If you’d like notifications for future posts (if any), you should subscribe there.
4 Great Mambo Chicken
I’ve been closely following AI and other speculative advanced technologies ever since reading a wonderfully idiosyncratic book called Great Mambo Chicken and the Transhuman Condition: Science Slightly Over the Edge by Ed Regis (1990). I later devoured works like Eric Drexler’s Engines of Creation: The Coming Era of Nanotechnology (1986) and Ray Kurzweil’s The Age of Intelligent Machines (1990), The Age of Spiritual Machines (1999), and The Singularity Is Near (2005). It’s amazing to see so many predictions, considered by many to be utterly outlandish, actually coming true.
Of course, I don’t know exactly what the future holds, but it’s bound to be wild. To paraphrase the safety warning for Big Thunder Mountain, one of my favorite rides at Disneyland: “Hang onto them hats and glasses, ’cause this here’s the wildest ride in the multiverse!”