OpenAI 数学推理突破内幕

1. From Practicing Mathematician to OpenAI: Meet Mark & Mehtaab

Well, thank you guys for coming. This is really exciting because I think math has been moving so fast with AI. I'd just love to get to both practicing mathematicians who work at OpenAI to chat on some of these results. We have with us Mark Sellke and Mehtaab Sawhney. Both of you guys have worked much more deeply in math since I've quit, many, many—over a decade ago. This is very exciting to hear a download of your thoughts on how OpenAI has been approaching this and where you think math is going with the incredibly rapid advance of AI. How did you come from being a practicing mathematician to working at OpenAI?

Yeah, I mean, I guess we both broadly got excited last year when the model started to really take off in math.

Yeah. I joined a little bit before Mehtaab. I saw the IMO gold medal last summer, basically, and thought, “This is amazing. I want to see what the heck they did. Let me go see.”

Then, in the fall, Mark gave me a GPT-5 account, and I started playing with the models. Very quickly, I became convinced that it was extremely exciting to play with them.

You two were collaborating before this? You’ve known each other for a while?

Yeah, we had 1 paper we actually wrote jointly.

2. Why GPT-5 Was the Conversion Moment

So GPT-5 was your conversion. What was the magic? What question did you throw at it? What was the process?

I think how this started was—at least for me—the starting moment was something like this: There’s a collection of problems called the Erdős Problems. Paul Erdős was a very famous mathematician who posed a bunch of problems, and they’ve now all been collected on this site.

I specifically worked in combinatorics, and a lot of these questions are among the most important problems in the field. It’s always fun to flick through the site, but one thing that often happened to me, which was extremely frustrating, was that I would look at a question, see that it was marked as open, and not actually know if it was correct or if it was still unsolved, because the literature is often quite hard to search.

One instance, I just plugged it into GPT-5, and 5 minutes later it found a reference. This was a case where a few of my friends had actually started thinking about the problem on the site. I was talking with them, and we had spent a few hours on it. It wasn’t clear if the problem was within reach, and it was just very nice to be told, “Yes, this is within reach. Here’s how you do it.” GPT-5 told me this, and then I told Mark about it. This was quite a surprising moment. We looked more into it and found 10 more cases like this at the time.

3. Beyond Search & Connections: How Recent Progress Goes Deeper

At the time, I felt that being better at making connections between wide-ranging areas—or even just searching to see whether there had been an earlier result or a related result—was humanly hard but perhaps easier for a machine. I imagine that, as progress has happened over the last year, what’s been impressive has gone beyond that.

Maybe, by talking about it more abstractly, or by talking through one of the problems that was recently announced through Astra, you can enlighten me as to how the recent progress has been more than just searching through more areas and making connections between fields. Is it actually deeper mathematical reasoning that’s similar to the reasoning of a working mathematician?

I think this search point—being familiar with everything—is still definitely a relative strength, and that perhaps informs the types of problems that AI is solving. There are some other relative strengths and weaknesses, too.

Another relative strength that’s pretty noticeable is that it’s very good at executing on an idea once it has it. Whenever you have an idea, there’s usually some amount of getting everything lined up: Is epsilon smaller than delta? This kind of thing. You have to get everything correct, and for a human, it’s easy to get lost in these details. The AIs just kind of always nail these arguments, I find.

For the unit-distance problem, was the approach there a contribution from OpenAI, while the underlying approach had perhaps originally been suggested by Erdős? Was the actual reasoning just a very momentous feat?

For a human, you have a limited amount of time. If, after so many steps, it’s still not clear, maybe you’re Andrew Wiles and you spend 10 years alone doing something, but it’s not clear that the risk-reward is good enough. Whereas for GPT, it’s like, “A human told me to do this. Let’s just do this.” That’s why we’re in this renaissance of reachable results.

Does that track? With the Astra results, is that where the strengths have primarily been, or is there an extra ingredient or some magic here?

I think the unit-distance example is quite telling. You can make the exact construction look very similar to what people had tried before, but getting an idea to work can be a large portion of the battle.

Often, as a practicing mathematician, you have an idea, and then you think it might work. You try for a few hours, a few days, or a few weeks, and at some point you give up. A not-uncommon experience is that you find out a year or 2 later that somebody else got the idea to work—the idea that you thought didn’t work.

In the case of the unit-distance conjecture, there were a lot of extraordinarily finicky details. Very often, when you’re doing mathematics, you’re gambling against the problem. You’re thinking, “Maybe I should try this approach, but it seems really unlikely and just not worth my time.”

The model, in several of these cases, both by combining what it knew and by having good taste, made the correct bet. You can see this in the summarized chain of thought we released. It’s reasoning like a mathematician, and because it knows a few very correct pieces, it makes the right decisions and is eventually able to prune the search tree.

It’s not really trying everything. It tries a lot of different things, and it’s extremely dogged, but it can’t try every idea. It has to try a limited set of ideas, and it’s able to use its knowledge and good mathematical judgment to find the right path. For me, that was especially interesting because this was a problem that a lot of people had thought about.

The fact that the idea isn’t so foreign probably indicates that a lot of people had tried it, or that at least a few very serious mathematicians had tried it. I think that’s what made it really interesting to see.

Something else I feel when I see these proofs is that, if I have an idea and I’m trying to execute it, I might have the wrong plan for how to make things work. As a human, if you go down the wrong path for a while, it can be hard to rewire your brain to start over and try a different path.

Your initial idea becomes linked in your brain with the other things that ended up not working. Your context window is a little polluted, and you can’t just make another clone of yourself from last week and say, “Don’t do this. Try something else. Build your intuition in another direction.” But it’s very easy to do this with an AI.

So I think this is another reason that getting the details right, once you have some good general direction, is much less of a barrier all of a sudden.

4. Reasoning Traces: Is It Lucky Sampling or Actual Backtracking?

And when you say it's much easier to do with AI, it's not actually being directed with human interference, either. As you were saying, in the reasoning traces, it's making these choices. Maybe it backtracks, but then it's able not to be distracted by the context in which it's thinking about the problem via this machinery. Do you see it going back as well, or is it just making good choices? Is it a lucky sample, or is it actually reasoning like a mathematician—where it doesn't do well on this path, so it goes back, but then it doesn't let that pollute the next path?

No, it definitely makes mistakes and then goes back and thinks about them. I think it's somehow very calculating, very correct.

As human mathematicians, you're not always perfect at making these decisions.

The first time something doesn't work, you automatically downgrade how likely this approach is to work, and you keep doing this a few times.

But I think even if it weren't for the fact that you could just start another model session over, it's always going to be the case that—

Got it. So in some sense, it is still leveraging the fact that you could run parallel agents on the problem. But if it were backtracking, that does make it seem much more like a human mathematician, and perhaps it is doing some of that stuff, too, because obviously we have to make mistakes in order to even gain intuition for why that solution space is not in the set of paths that it could be in.

I think this kind of thing happens with humans, too. If you get stuck on some approach, you might tell another human your general idea, and then they'll come back and figure out how to get it to work. It just—

Yeah.

It takes more time to do this with humans.

5. Why Math Papers Are a Bad Training Set for Real Mathematics

I wonder—maybe this gets to the extent that you can actually talk about. Obviously, don't talk about the training recipes or whatever, but it's interesting that if you're just studying, for instance, from math papers, it's a very poor training set, a priori, for math. Maybe math textbooks are an even purer example of this. They're really bad at actually reconstructing the motivation for why things were defined.

Don't learn real analysis from Rudin. It's very clean and crisp already, but it doesn't show the struggle that made us formulate definitions in a certain way. Why do we even need to define the real numbers in this super-abstract way?

I think papers are similar. Unless you're writing papers with the context of needing to educate somebody to be a mathematician, the actual curriculum of learning math is not inherent in a lot of our artifacts as mathematicians. Maybe another way to ask this question is: if the reasoning traces are producing things that are closer to mathematical thought, how does that arise?

I guess OpenAI has been the pioneer of reasoning models and of teaching AI to reason in this way. We're doing a lot of work in all possible directions on teaching models to reason better and for longer, in all kinds of different domains. I think we're training general-purpose reasoning models, and a lot of these behaviors that we're describing mathematically—backtracking or starting again—aren't really specific to mathematics. We're seeing them specifically in mathematics in these examples, but they're general-purpose tools for reasoning. If you work hard at reasoning, you should see these patterns eventually.

Mhm.

6. How Should the Math Community Adopt AI?

So is this emergent? I do think that's why the OpenAI approach—it's like, it doesn't rely on you doing auto-formalization in order to guide the reasoning. I think that's obviously more like us, but it's just not obvious that if you're training on, say, a corpus of math proofs, maybe auto-formalized in Lean, you get the projection of how to think well.

Put another way, maybe with code, code is such a good corpus to train on because it's one of the few datasets that has such large context. Maybe you see this with books, but they're less structurally interconnected. There's just less structure there, I think, on average in a book compared with a piece of code.

With math papers, I feel like the situation is similar. But maybe what we're still bad at with coding models is stuff that that dataset doesn't contain, which is the semantics. The syntax is there, but there's a little bit of the higher-level semantics of what produced it. Why do I have to write it this way? I'm getting too philosophical, but it is really interesting that it's still emergent that it's doing good mathematics.

We'll probably get into this in more detail if you want to talk about some of the problems. It's not just doing the expected thing, like pushing the brute-force approach. You're clearly impressed with some of the reasoning traces, and it's just not obvious that this is gleaned from what we would imagine would be the easy training set.

Yeah, absolutely. I think this kind of thing is one reason we decided it was important to release these summarized chains of thought for these kinds of results, because—

If you've never seen these and you just see all these proofs coming out, you're not sure what it means. Is the model just guessing in some insane way? Is it thinking in some totally foreign way? What's going on?

7. The Astra 10-Problem Set: Favorites & Deep Dives

Yeah. It's very much like reading a colleague's notes. It's a little more disorganized in some way. Especially when you work closely enough with collaborators, sometimes you'll just see them spill out their thoughts in an email to you, and it feels like reading a lot of those chained together. It's quite surprising the first few times.

Were you 2 very involved in choosing the problems to release in this last 10-problem set that Astra applied to? Which was your favorite?

Yeah, we were definitely involved. Do you want to start?

Yeah, I mean, packing maybe.

Yeah, I guess. My personal favorite among these problems is the following. It's an extremely simple question about how efficiently you can put a bunch of circles. My circles are not very good, and they're not all the same size, but—

But we're assuming they are.

So the question is: how densely can you place a bunch of spheres? You have a bunch of spheres of radius 1 in d dimensions. How densely can they pack?

In d = 1, this isn't an interesting question. It's just the real line, and you can cut it up. A sphere in dimension 1 is just a unit segment, so you can cover everything. In d = 2, it's the picture that everybody loves: a bunch of spheres that form a hexagonal lattice.

Hopefully I've drawn it well enough that I can draw the hexagon.

This is kind of betraying my naiveté on this problem.

Yeah, it's not so obvious that this should work. It was only proven in the '60s, I think. There's a short argument, but it's not easy.

Where's the intuition? What is the machinery of the argument?

It kind of—

It definitely looks like it should work. That's why we're—

Yeah. So I think—

But so did—

Yeah, I think this is the best part about this problem: nobody really has any idea about it. Honestly, the best intuition I have for this is that bees do this, and if there were a more efficient way, then probably bees would pack honeycomb some other way.

Evolution is efficient.

Yeah.

I think beyond that, I don't have a great argument. How little we know is demonstrated by the fact that in d = 3, the answer is just how you pack oranges in a grocery store. This was only proved by Hales sometime in the 2000s, and we don't have a short proof of this. I think the shortest proof is a few hundred pages.

What area does it draw from?

It’s a lot of linear programming arguments, and it’s very delicate geometry. It’s quite ugly, actually. This is a famously ugly argument.

Oh no.

And then the 2 most famous results are in dimensions 8 and 24.

8 and 24. There must be some weird subspace.

Yeah, exactly. So this was done in 2017.

Sounds slightly prettier, though. I hope.

The reason it works out in these 2 very special dimensions is that this is called a lattice packing. It’s very regular, and it turns out that in these 2 dimensions there are 2 very special lattices. They’re called the E8 lattice and the Leech lattice, and they’re very nice and unusually dense.

They’re also very pretty structures coming from other areas of mathematics, and it turns out that they’re the optimal structures.

But they’re still regular?

Yeah, they’re very regular. But beyond this, we don’t know any more exact dimensions. We know these 5 dimensions, and we don’t really know anything else.

To give an indication of how little we know, there are 2 very surprising things about this. You can define δd to be the densest sphere packing in dimension d. There’s an easy lower bound of 2⁻ᵈ. This is not so hard to show: basically, any packing where you can’t put in another sphere has to have at least this density.

It’s not ridiculously small, and we know that it has to decay exponentially. It has to decay like (1 − c)ᵈ for some constant c. So, in large dimensions, you can cover only a vanishingly small portion of space. But we know basically nothing else.

That’s just because of the high-dimensional sphere thing, where it occupies—yeah, the volume behavior is weird.

Yeah. Basically, the spheres don’t want to touch next to each other. I don’t think there’s a particularly short way to see that it’s exponentially small, but it’s known to be exponentially small.

For a long time, the best bound was something like this funny number: 2⁻⁰·⁵⁹⁹ᵈ. This was proved by 2 mathematicians in the 1970s, Kabatiansky and Levenshtein.

Okay, that’s a weird number. Where does that come from?

It’s the answer to some extremely ugly optimization problem.

There’s a nice underlying strategy.

Okay.

Yeah. I’ll say one last thing about this. These were 2 Russian mathematicians in the 1970s, and it’s actually very hard to find their paper. It’s 1 or 2 pages long, and they don’t write very many details because the paper was fairly terse.

Is 2⁻ᵈ just the square lattice, the dumb one?

It’s actually not so easy to see. The argument is as follows. Imagine that you have a set of spheres, and I tell you to construct a set of spheres such that you can’t put down another sphere. If you could put down an extra sphere, you would just keep putting them down until you couldn’t anymore.

Take any such packing. I claim that it has to cover at least a 2⁻ᵈ fraction of space. The reason is that if you blew up each of these spheres by a factor of 2, they would have to cover every point in space. Otherwise, if there were any empty space, you could put down another sphere there.

So I guess if you take the usual lattice, there are actually more places you can put things, kind of diagonally.

Yeah. That’s actually not the bound you want; it’s a worse bound.

Yeah, you can just keep plopping things in.

This is related to a really funny fact: if you put a sphere at every vertex of a cube in high dimensions, the volume covered is vanishingly small.

It’s vanishingly small.

It’s so small that you can put another sphere in the middle, and it fits.

High-dimensional sphere behavior is weird.

Yeah, very weird. The model shows the following. I’ll write 2 things. This is, I guess, probably the right way to refer to it.

I’m going to write something called the LP bound. I’ll explain this in a second. It shows that δd is smaller than this very nice number. It’s essentially e raised to a negative constant plus o(1), all to the d. You can work out what this number is; it’s roughly 2⁻⁰·⁶ᵈ.

Close.

Yeah, it’s surprising. With this one, you’re like, “Oh, maybe there’s some nicer kind of structure that fell out.” It’s at most roughly 2⁻⁰·⁶¹ᵈ.

That’s the numeric value. I thought it was 0.604.

Great.

Yeah, this shows mine. There are a couple of things to explain. First, what is this LP bound? Viazovska’s work actually builds on some earlier work. It turns out that there’s a way to attack sphere packing via what’s called a linear programming bound.

“LP” just stands for linear programming. Cohn and Elkies gave an approach to sphere packing based on linear programming. It’s a linear optimization problem over a convex set, but here it’s all infinite-dimensional.

Basically, this reduces to the following. You try to construct a function f in d dimensions, mapping to the real numbers, with 2 properties. First, f(x) is less than or equal to 0 whenever the norm of x is bigger than 1. Second, the Fourier transform of f is always nonnegative.

So you’re taking some arbitrary f that satisfies these properties?

Yeah, you can take any f that satisfies these properties. What they prove is that δd is bounded by the ratio f(0) over the Fourier transform of f at 0, multiplied by the volume of the ball of radius 1/2 in d dimensions.

This proof is not so short for an experienced mathematician. It took half a paragraph to prove, but it’s a little bit tricky.

The point is that this is a relaxation problem. There’s no guarantee that taking the optimal f will give you a good bound on δd. What Viazovska did—and this was a large part of the reason she won a Fields Medal in 2022—was construct a function in 8 and 24 dimensions such that this upper bound matches exactly the 2 very special lattices.

Those are kind of miracles of nature: both that you can construct this function and that it gives you the optimal bound. But this is a very natural problem. It’s a function with 2 very simple properties, and you just want to understand how it behaves in large dimensions d. That was a big mystery.

There was a numerical paper by Cohn and several others that conjectured, based on doing numerical calculations—extremely clever numerical calculations, but still numerical calculations—that this was the answer. They had no idea why this would be the answer.

The model shows that the linear programming bound in large dimensions has this extremely nice asymptotic behavior.

Yes. The proof explains where this is coming from. Because you understand this LP bound perfectly, it gives a better bound on δd. It turns out that the old bound can be reinterpreted in this framework, and what the model does is show you the best possible bound you can get from this framework.

So the model sort of made the connection?

Yes. The model gives a function f that first produces this bound, and then it shows that there’s no function f that can do any better. So it’s an equality, which is quite strong. We now understand this problem in high dimensions very well.

That’s pretty remarkable. The model was essentially told, “Analyze this linear program in high dimensions. Go have fun.”

Got it.

To give an indication of how little we understood this, the conjecture was based basically only on numerical work—extremely clever numerical work, but numerical work.

Yeah, you have to figure out why this is the right thing to aim for, and it does. That was pretty remarkable.

I had actually thought about this problem for about 6 months when I was a graduate student, and I remember making absolutely zero progress on it. So it was very nice to have it explained why it was true. That was a pleasant experience.

I think, in general, it was one of these solutions where I knew several people had tried the problem. It’s pretty remarkable because the model’s solution—especially the part showing that the LP bound can’t do better than this—was quite short.

It's a few pages of complex analysis, but it's exactly the right approach. Once you see it, it's unbelievable: why hadn't somebody done this before? There are many types of good mathematics, but one of them is seeing it and thinking, “Why didn't I think of this?” I knew, in a sense, why I hadn't thought of it, but it was quite nice to see, and it was fun. That's why I like this problem a lot.

Yeah. So this is the first of the 10 problems Astra saw. Mhm.

But the second is actually closely related. This was sphere packing. The second one is spherical and binary codes.

Mhm.

When you draw a code, you should draw a packing. You drew a packing; it's going to be the same picture. Okay, sure, sure.

Otherwise, we're going to have this picture of packing in our mind.

A spherical code is literally just a sphere packing, but on another sphere.

Yeah. I mean, a spherical code is basically just a sphere packing on the surface of another sphere.

Yeah, it looks like a sphere.

Yeah. Same picture as before, except you're on a curved surface.

Okay, okay.

Why is it called a code? I guess the reason is binary codes, which are the same sort of thing, but now on a cube. Let me draw a picture of a cube and the simplest possible code on it.

When you're sending something, this is really about error-correcting codes. I send you a string of bits, and maybe I'm worried that some of the bits I send you get corrupted. Maybe, because of some errors in my system, one of them gets changed, and we want a communication protocol so that you can decode this small amount of error and recover what I was trying to tell you.

Normal English language has this sort of property, right? If I make a few typos, you're going to be able to understand what I'm saying. But if we have a really brittle communication scheme, it's not going to work. Codes are the way you solve this. Mathematically, a binary string of fixed length is a point on some hypercube.

Mhm.

We want a dictionary of allowable code words that are separated from each other. If I don't want any two to be adjacent, I would take these four vertices—the even ones, if you sum up the digits. In this case, if I have an error, I guess you can't tell which one it's from, but at least you can tell there was an error.

Oh, I see. Because it's sparse; none of them are adjacent.

Right. You want a large Hamming distance between any two distinct words in your dictionary.

If you take two opposite corners, then with a single-bit error, I can always recover which point it came from—the one it's definitely closest to.

There's kind of the same question in both cases: in a very high-dimensional setting, what kind of rate can you get? For binary codes, it's an extremely practical question. If I send you an n-bit string and there's a 1% error rate, how much longer does my message have to be to tolerate that amount of errors?

Right. This is some fundamental information-theoretic limit on communication.

You can see that the spherical case looks very much like sphere packing. If you make all these little spheres really small, the curvature of the big sphere isn't going to matter so much, and it looks like just packing spheres in full space.

In fact, these problems turned out to be very related. There were similar bounds coming from the Kabatiansky–Levenshtein work, with one result for the sphere and one for the cube, but it's all kind of the same stuff.

Our models found better bounds for these cases as well.

Mhm.

The techniques look pretty different if you write them out. The full-space linear-programming analysis used complex analysis, but the method for these cases used representation theory.

Both the sphere and the cube have a lot of symmetry.

The idea of the proof was to really leverage that symmetry. There was some amount of this in the existing method, but the improvement was to lean into the representation theory really hard and make the algebraic symmetry enter in a more sophisticated way.

It turns out that, from the representation-theory formulas, if you take this small-sphere limit in the spherical-code case, you recover part of this result and recover this value. This result isn't a special case; you only went one direction of the bound from looking at it from the code's point of view. But there's a very close connection.

Okay.

Yeah.

Yeah. So you guys let this run in parallel. Is it kind of discovering this because you're not feeding it?

This was the one case where there was some interactivity involved. For all of them except for this pair, we had problems, fed them in, and the model came back with solutions.

What happened here was pretty interesting. We first asked it to improve the bound for the codes.

Mhm.

It came back with an improvement that used some amount of representation theory. Then we asked it, “Hey, can you push this further? What happens?” It came back with much more sophisticated representation theory, and it turned out that we got this conjectured value for full-space sphere packing out of that method by pushing it as far as it could go.

So then we asked it to directly analyze this case and try to complete the picture.

Okay.

Yeah.

8. The Harness vs the Model: What Actually Matters?

So the relationship isn't a coincidence.

Yeah, yeah.

It's interesting when you say the first prompt, which is maybe so basic—“Can you push this further?” It does require some judgment from mathematicians. Eventually, by scaling the models, you might imagine you don't need to do that. Or there's another view that the harness actually matters, and this is part of the harness apparatus. Do you have any views on that from working with Astra, especially across generations of models? How much do you have to input, and how much does the harness matter?

I guess there have been some funny quirks like this that come from exactly what you ask the model to do. In this case, what the model was originally asked to do for codes was improve the bounds by some exponential factor, so it really showed up in this leading constant up here.

It improved the bounds, and it didn't try to push things too much further. Sometimes you see it do that, but sometimes it just doesn't bother. You ask it again, and it goes further. It wasn't a capabilities issue; it just kind of didn't feel like it at the time.

Mhm.

I think models tend to be pretty task-oriented. If you tell it to do a task and it accomplishes the task, it's pretty happy.

The task-orientedness is interesting. Do we expect that level to ascend? Not that models will be less good at being task-oriented, but that they'll ascend to the level of, “No, let's go in this direction.” You'll have the judgment because you guys had the judgment. You said, “This is pretty promising. It looks like you're using a lot of representation theory, and there doesn't seem to be a limit so far.” But the model doesn't have that context yet.

What I'm trying to say is that, with previous generations, when you had to give it more prompting and more harness work, eventually you probably had to give it less. That gives you some confidence that there's this really fast ascension. Do you see somehow solving a harder math problem as requiring you to solve many smaller, somewhat less hard math problems, with the fact that the math problems are getting harder indicating that the model is able to take on more and more work in a single continuous unit?

I think that's the thing that looks very promising. With any of these solutions, it's not like there's just one idea and then you're home free. You need several pieces to interact and talk to each other.

The model doesn't come up with all the ideas at once, right? It doesn't pull everything out in an instant, given the fact that it needs to see how this piece interacts with another piece. That's kind of like solving a problem in itself, or piecing together many problems in itself.

It could just be that when you're telling it, “Push this even further,” that was of the same order of magnitude as all the smaller things it's solving in between. So you don't think that's kind of a privileged direction? It's just, “Hey, let's give it one more nudge”?

Or do you actually think that there's—I guess what I'm trying to get at is a bigger question—is there a good sense of taste? When people talk about how well the models are getting at doing research, for instance, that's what we want a little bit of recursive self-improvement. There are surprising things about how that improves, and then there's the question of whether, right now, it's still at the level of a junior researcher, not really asking the right problems.

9. What Even Is "Taste" in a Model?

I'm just trying to get a sense of where you're seeing that progress through the model advancements each generation. I mean, what is taste, even?

Yeah, I think I tend to be pretty utilitarian in my view of taste. If you're able to solve problems faster by making better judgments, I think that's the best general proxy I have for taste. Somehow, the fact that solving harder problems means it has, by definition, better taste.

I think occasionally, because they're task-oriented, you do get these symptoms of, “Oh, it clearly has made a breakthrough. It understands that it's made a breakthrough.” Then it doesn't push all the way to the limit because that's not what you asked. But that seems rather minor compared to the state of progress we've seen so far.

Okay, yeah, I think it's pretty clear—

I think maybe you're liable to get confused if you're trying to do a concrete, long-horizon task and show taste at the same time. But if you have one model that's responsible for taste and one model that's responsible for going out and working for a long time at solving a hard problem, as the underlying system of the supervising AI, I feel like that's going to be fine currently.

Oh, interesting. Because that is like saying that these two things are somewhat separate, or at least that they shouldn't pollute each other's contexts, which could potentially be a stronger statement.

No, it's just kind of interesting because, to your point, let's take the utilitarian answer: solving harder and harder problems. It's doing a lot more than just brute-forcing something. It's making choices. It's pruning a vastly large space of possible paths into something that's tractable, but that ends up being a vanishingly small path within that space.

Why would a separate model, a separate generation, or a different version of the model contribute to taste? Maybe that's too abstract and doesn't make any sense. Maybe we should just let the model do it.

The related question might be: What is the thing that gets us to a better version of intelligence—the harness and the model? Is it just the model? We see this in applied AI, or in startups, where there's a continual battle: You need the harness, but the harness adapts very poorly to a new model. Sometimes a very minimal harness is still the best way to expose the raw power of the model.

But now we also have these training regimes where we require the harness to be trained. Maybe part of this is to keep things more proprietary and harder for other people to use, but I think partially it's actually that it helps us have more control over the reasoning traces we care about.

It's a long, rambling way of saying that I don't actually know. It's so interesting to see how the models have gotten better at math, and maybe something that's very abstract and hard to describe, like taste, is a way to tease out what's actually necessary here.

My only nontrivial thought here is that when you're working—when you're doing any task—occasionally you get pigeonholed and work really hard. Just having a friend look over your shoulder and be like—

“What are you doing?” And then just having that one bit of stepping back for 10 seconds is often very useful.

Yeah, yeah. I mean, I see no reason why humans would be so different from models somehow.

Why would models be so different from humans? Having a few humans working together is often more powerful than just having one.

Yeah. It's like, in this kind of collaborative thing, you actually artificially created it, but it's very similar in dynamic.

But I think a lot of taste is also having a sense of what problems—or what method you have in mind—are going to be good at solving.

Mhm.

Like, it's—I mean, certainly there's some amount of absolute aesthetic point, right? But there's also just having a nose for what you might want to pursue because you'll be able to make progress. You would expect that, as a side product of being good at completing tasks, you would get there, right?

Let me know if we still want to do a section on sofic groups. I think it's definitely super interesting.

So maybe the first question is: What is a group? Let's remind ourselves. A group is a set of elements with some multiplication operation. Basically, this is how mathematicians think about symmetry.

If G and H are elements of your group, then GH is some other well-defined element of your group. You have associativity, and you have an inverse: for every G, there's some inverse. There's also a specific element in the group that is the identity.

It's an abstraction of composing operations. These could be numbers, multiplying matrices, or rotating something, which is a special case of multiplying matrices.

And a group is sofic. There's a precise definition, but roughly, it means it can be approximated by finite groups. We didn't know if there was a non-sofic group. The result that Astra proved—

—is simply that there exists a non-sofic group.

Yeah. Before going into that proof, I would love to hear the explanation of how it found a counterexample. Especially for the countable case, maybe you'll be relating it to the Aldous–Lyons thing. It helps anchor the picture: It seems like such a nice result if it were true, but it isn't, and it seems almost reasonable.

Yeah, I would say that the hope that there was no non-sofic group—that every group had this kind of approximation—was maybe people hoping that there was a miracle, because it turns out that groups like this have a lot of nice properties.

You can run certain proofs for finite groups and then approximate them in whatever way the definition of being sofic lets you approximate them, and get the result. There's this notion of being a surjunctive group. Any group that is sofic is also surjunctive. Surjunctivity is a property of dynamical systems on the group.

The original question was whether every group is surjunctive. This was a question of Gottschalk's from the '70s. The fact that follows this pattern—proving it for finite groups and then using this approximation—is what motivated the question of whether there is a non-sofic group.

Mhm.

Yeah, maybe I’ll say a little bit about the Aldous–Lyons conjecture.

Yeah, sure.

I guess I had heard of this a little bit beforehand because there’s a related, stronger conjecture in probability that was made popular by Aldous and Lyons. This conjecture roughly says that any infinite graph with a nice property called unimodularity—a unimodular random graph—can be approximated by large finite graphs. Maybe the way to explain what these kinds of things are trying to say, without getting into the technical weeds, is to say what they mean about the integers.

So, how would I draw the integers as a graph? This is called a Cayley graph: you’re just going to connect nearest neighbors. There’s some canonical way in which this is the graph that represents the integers. There’s some sense in which you can approximate this by finite graphs. Why? Well, if you look at the integers mod n, you get the same picture, but you have a big circle instead of an infinite line. The point is, if you look at any point here and any point here, nearby things look the same. You have to go very far away to see this global geometric structure—that you have a circle and not a line.

Mhm.

In fact, the integers and the integers mod n are both groups, just by adding numbers or adding numbers mod n.

So these integers mod n are sofic approximations for the full integers. This approximation is why the integers are a sofic group.

Soficity—the statement that every group is sofic—is sort of a generalization of the fact that you can do this approximation with groups. The Aldous–Lyons conjecture is a broader conjecture: any network can do this, and it doesn’t require as much algebraic structure, roughly. So it’s a broader conjecture.

This conjecture was disproved earlier, about 2 years ago, and it was really a tour de force. It was 250 pages, building on another 200 pages. It uses quantum complexity theory, so it really builds this—

You know, very complicated bridge, and I think not very many people could understand this.

Since this is a stronger conjecture, the disproof is weaker than disproving the statement that all groups are sofic. But it turns out that the direct proof that there’s a non-sofic group was much shorter and easier than this really amazing disproof of the Aldous–Lyons conjecture. It’s maybe 15 pages, and it doesn’t have any of this very complicated connection with quantum complexity; it stays in group theory. It uses some important existing results by other mathematicians, like Kun and Thom, but it’s a very reasonable, normal kind of proof.

Yeah. And, spelling out maybe the obvious, the connection between the sofic-group statement and Aldous–Lyons is just that you take the Cayley graph, and that’s the one they use for Aldous–Lyons, right?

Yeah.

Yeah. And so that’s why it’s a subset of the broader conjecture, right?

Right. Basically, for a group you can take exactly a Cayley graph: you take some elements that generate the group and connect elements that are adjacent.

Right. You just get a single graph after you fix a set of generators. So this conjecture is stronger, basically, because it allows a broader set of graphs that aren’t deterministic. It allows them to be random, but have some extra unimodularity property that constrains exactly how they can be random. But yeah, basically, that’s the difference. Here you have to give a deterministic network instead of a random one.

Anything interesting or surprising about the result? You mentioned that the techniques stayed within group theory.

I think maybe it’s a nice example of this general pattern: the theorems produced by AI have generally been pretty short. The proofs are generally pretty short, like with the counterexamples so far.

Yeah, but I mean this one is sort of a counterexample, but there’s some stuff you have to do to analyze things. The difficult part here is that the property of being a sofic group is not so easy to get your hands on. You have to find a concrete way of producing a way of showing that this group cannot be sofic. The proof is actually very short. It’s almost a combinatorics argument, but it’s a very, very delicate combinatorics argument. Somehow, the model needs to both have the right statement, know what pieces in the literature to use, and execute it correctly, and that’s very nice. The difficulty of this problem is that it’s just really hard to get your hands on what it means to be approximated by any possible finite object.

I was going to say: what is happening at that countable infinity that’s resisting this approximation? When you do a postmortem and say, “Okay, Astra, explain to me what is happening,” do you get a sense of that?

Oh yeah, we did that. All right, what was a good explanation you got out of it?

I think there’s some concrete combinatorial obstruction. Basically, it’s hard to explain, but there’s some concrete combinatorial obstruction which, if you read the previous papers, you realize is what they couldn’t rule out. Astra found a way to say, “No, if you add this one extra algebraic fact, this weird conspiracy can’t happen.” It’s very clearly trying to rule out a conspiracy that the previous authors had implicitly written about.

Yeah.

And those were the actual suspects, it turned out. So they were sort of on the right track, and then Astra did the last mile, or however you quantify that.

Yeah. About a year ago, I would have been very surprised to learn that all of these AI proofs are very short and elegant. You’re kind of afraid that they’re going to generate all these 1,000-page things and you’re never going to be able to understand them. But it’s been the opposite.

Yeah. Only humans can generate—

200-page proofs right now.

Well, I was asking: if you do that postmortem, it usually ends up engendering more mathematics, because when you do that with humans, that’s what breeds new mathematics. Maybe if you alter the prompt a little bit and say, “How would you generalize this?” I don’t know if that’s been a technique for you—to have it explore and exploit what it has already developed.

Well, there has been follow-up on this already, actually, by Kun and Thom, whose work this was built on.

The math community is coming along.

Which is kind of what we’re hoping for, right? We don’t want to be writing lots of follow-up papers ourselves, but if there’s some interesting follow-up, we’re very happy that there’s some follow-up building out these ideas more and giving more examples of non-sofic groups in this case.

Actually, maybe that’s a great segue into how this is being taken up by the math community. I feel like there’s a spectrum of answers from working mathematicians. Most, at this point, are probably like, “AI is obviously doing some nontrivial stuff. It would be a disadvantage not to admit that in my workflow.” I’ve definitely heard some stories where people find it hard either to take AI as a co-author or to figure out how to do attribution this way. I don’t know—maybe to paint the more optimistic picture: you’re saying you want mathematicians to be building on these results. It definitely generates a lot more results to be verified, so it puts pressure on the community and the profession. How do you expect the evolution of uptake and collaboration with mathematicians?

Given that models can produce sophisticated mathematics, they can help you understand sophisticated mathematics. Occasionally I enjoy looking at the arXiv and want to understand some proof. I could read the introduction, but in practice it’s much faster to take the PDF, put it into my favorite model, and get an output of what the rough proof strategy is. Of course, models are going to help us produce exponentially more mathematics, but they also make it much easier to absorb it. Right now, it’s still a bit of a back-and-forth challenge, but for me at least, it’s much, much faster to understand a piece of mathematics with a model than without it.

So it's helping solve the problem it creates, anyway.

Yeah, I feel like that, at least. I don't view it as creating much more of a problem, but again, I don't have such high stakes in whether I'm going to get tenure, et cetera. So I agree that making it more accessible is a good thing. If I'm not spending so much time absorbing an area, I can put it into ChatGPT.

10. Empirical vs Theoretical Math & the Positive Vision

You guys have an even more powerful model hopefully releasing for other people to enjoy as well. I think the positive version of that is that more people can participate in mathematics. People might be coming with other intuitions, and they could maybe generate good mathematics. Is that closer to the vision of what you're hoping this is pushing toward? Or what things do you think we should be wary of to adapt fast enough to take advantage of AI?

Yeah, I think there will certainly be a lot of changes. In math, there are a lot of things that are important for a given result, right? You need someone to come up with it, but you also need people to understand and absorb it and internalize it enough to do more with it and figure out where it fits into humanity's understanding.

A couple of years ago, proving the result was so hard that the other stuff was just coming along for the ride. If you managed to prove this thing yourself, you were automatically going to understand it quite well. You were responsible for maintaining it, in some sense, and explaining it to other people.

Now what was the main bottleneck before is much less of a bottleneck, and these other constraints come into play. So the optimal structuring for organizing knowledge could look rather different.

Yeah. How does that look? Does this make the field a lot more empirical? Will people do the hard thing—the first thing that was scarce, which is all the reasoning—and then more empirical work? Not that it's a bad thing to make it empirical, but it's almost like it functions as a very different discipline.

A lot of the fun stuff is understanding. Does understanding, communicating, and maybe assembling—while still having human taste—remain rarified? Is that how current mathematicians need to adapt and reward contributions, or is this too much of a caricature? Is it something else?

I think understanding how to put more and more mathematics into a proper framework, and being able to explain it to other humans so they can also appreciate it, will become important. Somehow, we implicitly valued this, but it was usually because you were the person proving the result, which gave everybody else the understanding.

Increasingly, it would be a function of helping—being the human who can give this understanding to other people and help them with it. I think more of that communal understanding will become an increasingly explicit and valuable part of the subject. It was much more implicit in how we view math in general, but I think it will become more explicit.

I mean, a nice thing about math is that the ceiling for the difficulty of a math problem is pretty high. So even if AI continues getting exponentially better at math, it's plausible we'll never solve something like P versus NP.

And it could be that the field becomes more attached to these big mysteries and less to smaller mysteries that are more routine.

Yeah, yeah. I think that's a positive vision.

Also, there are things I've spent months or years of my life wondering about without getting to know the answers, and I hope—

We get them—what a joy.

Yeah. Some portion of them, I'll get to know the answer to. I'm pretty happy about that.

No, exactly. I'm excited about this renaissance of results and understanding. I feel like this is such an infinite field—no pun intended—but there's just so much that you can create here.

Especially for somebody like me who's not going to have the time to practice mathematics, now there's a lot more that you can do in the activity of math.

Yeah. I think the ability of someone who's not working on math as their literal job all the time to understand what's going on and learn about some of the mysteries they might have wondered about will go up quite a lot.

Also, if you're working on something that requires some math, suddenly you don't need to find a world expert on this topic to be able to use it in your own work. You could—

Sorry, mathematicians. Yeah, yeah. No, it's true. I mean, there was just a dearth of actual people who could do that, so I think this is helpful. Maybe it's helpful for theoretical physics. We'll see. But a lot of other applied areas as well.

It'd be nice for the world if applied mathematics went a lot faster.

Yes. I'm of that opinion. Well, thank you guys for joining. This was a lot of fun, and I'm so excited for how much the models are advancing. Maybe we'll have you guys back soon.

Yeah, thanks so much for having us.

Yeah, thanks for having us.