Mathematician / Researcher: Often as a practicing mathematician you have an idea and then you kind of think it might work, then you try for a few hours, a few weeks, and at some point you give up.

Host / Interlocutor: Whereas for GPT, like, okay, a human told me to do this, let's just do this. And so that's why we're sort of in this renaissance of like reachable results.

Mathematician / Researcher: This is the best part about this problem, which is really nobody has any idea.

Host / Interlocutor: Is the model just guessing in some insane way?

Mathematician / Researcher: It doesn't seem like there's a limit so far, but it doesn't have that context yet.

Host / Interlocutor: It'd be nice for the world if applied mathematics went a lot faster. The ceiling for difficulty of a math problem is pretty high. Even if AI continues getting like exponentially better at math, plausible will never solve something like P versus NP.

Host / Interlocutor: What's the ideal way that this is being taken up by the math community? Probably most at this point are like, okay, AI is obviously doing some non-trivial stuff.

Host: 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, you know, get to both practicing mathematicians and who work at OpenAI to chat on some of these results. So, you know, we have with us Mark Sellke and Mahtab Sawhney. We're connected actually because Yufei was actually your adviser. And so both of you guys have worked much more deeply in math since I've quit over a decade ago. And so this is very exciting to kind of hear a download of your thoughts on how OpenAI has been sort of approaching this and also just like where you think math is going with the incredibly rapid advance of how AI has been helping. So yeah, I don't know, maybe we can start off with some very basic questions of like what do you do to the extent that you can of course share, and how did you come from being a practicing mathematician to working at OpenAI?

Mark Sellke / Mahtab Sawhney: Yeah, I mean I guess we both broadly got excited last year when the model started to really take off in math.

Mahtab Sawhney: Yeah. Um, so I joined a little bit before... I saw the IMO gold medal last summer basically and I thought, you know, this is amazing. I want to see what the heck they did. Let me go see. And then yeah, I guess in the fall Mark gave me a GPT-5 account and then I started playing with models and very quickly became convinced that yeah, it was extremely exciting to play with them. Yeah.

Host: You two were collaborating before this. Yeah, you've known each other for a while.

Mark Sellke / Mahtab Sawhney: Yeah, we had like one paper we actually wrote jointly.

Host: Yeah. So, GPT-5 was your conversion. What was the magic that sort of, I don't know, as you're doing, like what question do you throw at it? What process?

Mahtab Sawhney: Yeah. So, I think how this started was, at least for me, the starting moment was something like: there's a collection of problems called... so Paul Erdős is a very famous mathematician, posed a bunch of problems, and so they've now all been collected on this site. And so I specifically worked in combinatorics, and a lot of these questions are among the most important. So it's always fun to flick through the site, but one thing that often happened to me that was extremely frustrating was I would look at a question, see that it's marked as open, and then not actually know if it's correct, not actually know if it was still unsolved because the literature is often quite hard to search.

Host: Yeah.

Mahtab Sawhney: And in one instance I just plugged it into GPT-5, and like five minutes later it found a reference. And 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 I mean we had spent a few hours, wasn't clear if the problem was within reach. And it was just very nice, okay, to be told: yes, this is in reach, here's how you do it. And yeah, GPT-5 told me this, and then I told Mark about this, and this for me was quite a surprising moment. Yeah. And then we looked more into it and we found like 10 more cases sort of like this at the time.

Host: I feel like, you know, being better at maybe making connections between wide [fields] or even just like, as you're saying, the search for whether there's been a result or a related thing earlier is just kind of humanly hard, but maybe better for machine. But I imagine as the progress has happened in the last year, what has been impressive has kind of reached beyond that. And maybe through talking about it more abstractly, or if it's more natural to talk about it through like one of the problems that has been recently announced through, you know, Astra, you can kind of enlighten me as to how the recent progress has been a lot more than just searching through more areas, making these connections between the field, and perhaps just actually deeper, more mathematical reasoning that's similar to a working mathematician.

Mark Sellke: Yeah. I mean, I think this search point of being familiar with everything is still definitely like a relative strength that maybe informs the types of problems that AI is solving now.

Mark Sellke: Um, I think there are some other relative strengths and weaknesses. Another relative strength that's pretty noticeable is just like it's very good at executing on some idea once it has it. Whenever you have an idea, there's usually some amount of getting everything lined up, like is epsilon smaller than delta, this kind of thing, you have to get everything correct. And like for a human, it's easy to get lost in these kinds of details, and the AIs just kind of always nail these kinds of arguments, I find.

Host: Yeah. Is it usually just... I mean I feel like you guys will know more detail on this, but like for the unit distance problem, the approach there was definitely contributions from OpenAI, but like the approach perhaps was suggested even originally by Erdős, and then it's just that the actual reasoning was a very momentous feat. And so for a human, you're like: well, I only have a limited amount of time, and if after so many steps it is still not clear... I mean maybe you're like Andrew Wiles and you actually spend 10 years alone and do something, but if it's not clear, then it doesn't become... like the risk-reward is not good enough. Whereas for GPT, like okay, a human told me to do this, let's just do this. And so that's why we're sort of in this renaissance of like reachable results. Does that track? And did you feel like with the Astra results, is that sort of like where the strengths have been primarily, or there's an extra ingredient or magic here?

Mahtab Sawhney / Mark Sellke: I think the unit distance example is quite telling in the sense of maybe the exact construction you can make it look very similar to what people had tried before. But often as a practicing mathematician you have an idea and then you kind of think it might work, then you try for a few hours, a few days, a few weeks, and at some point you give up. And then a not so uncommon experience is that you find out a year or two later that somebody else got the idea to work that you thought didn't work. So somehow getting an idea to work can even be a large portion of the battle. And especially in the case of the unit distance conjecture, there's just a lot of extraordinarily finicky details. And very often when you're doing mathematics, you're kind of gambling against the problem. You're like: maybe I should try this approach, but it seems really unlikely and just not worth my time. And the model, I think, in several of these cases, both by combining what it knew and sort of having good taste, kind of made the correct bet. And you can kind of see...

Speaker A: ... this in, um, the summarized chain of thought we released. You can sort of look at it and it's reasoning like a mathematician, and because it knows a few very correct bits, 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. It's extremely dogged, but it kind of...

Speaker B: I mean it can't try every idea. It has to try a limited set of ideas and it's able to kind of use its knowledge plus good mathematical judgment and find the right path to go along. So I mean that for me was like because this was a problem which a lot of people had thought about and yeah.

Speaker A: I mean the idea, the fact that the idea is not so foreign probably indicates that a lot of people had tried it or at least a few very serious mathematicians have tried, and I think that's what made it really interesting to see. I think something else that like I feel when I see these proofs is like, if I have an idea and I'm trying to execute, it might be that I have some wrong plan for how to get things to work. And as a human, if you have some wrong path you go down for a while, it can be hard to rewire your brain to start over and try a different path. Your initial idea is linked in your brain with these other things that ended up not working. You know, it's sort of like your context window is a little polluted, and you can't just make another clone of yourself from last week and say, you know, don't do this, try something else, build your intuition in another direction...

Speaker B: ...but you know it's very easy to do this with an AI. So, I think this is another reason that it's like...

Speaker A: ...um it like getting the details right once you have some good general direction is like much less of a barrier all of a sudden.

Speaker B: And when you say it's much easier to do with AI, it's not actually being directed with human interference too. It's like, as you were saying in the reasoning traces, it's making these choices. Maybe it backtracks, but then it's able to not be distracted by maybe like the context in which it's thinking about the problem via these machinery, and it's like go back... do you see it kind of go back as well or is it just like making good choices? Is it a lucky sample or is it like actually reasoning like a mathematician where okay, it doesn't do well in this path, but it goes back, but then it doesn't let that pollute?

Speaker A: No, I mean it definitely makes mistakes and then it goes back and thinks about it. I think it's somehow very calculating, very correct. I mean, yeah.

Speaker B: As human mathematicians, you're not always perfect at making these decisions and like...

Speaker A: ...like the first time something doesn't work, you automatically kind of downgrade how likely this approach is to work and you keep doing this a few times. The model somehow is much better able to... it seems for several of the solutions we've seen, somehow it seems much better able to update how likely the path is to work versus rejecting a path versus a human doing it.

Speaker B: But I think even if it weren't, the fact that you could just start another model session over means that, you know, it's always going to be the case that...

Speaker A: Got it here. So in some sense it is still leveraging the fact that you could run parallel agents on the problem. But if it were kind of backtracking, then does make it seem much more like a human mathematician, and perhaps it is kind of 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.

Speaker B: I mean, I think this kind of thing happens with humans, too, where if you get stuck on some approach, you might tell another human your kind of general idea and then they'll come back and figure out how to get it to work and you know, it's just...

Speaker A: Yeah.

Speaker B: It takes more time to do this with humans. I wonder... I mean, you know, maybe this gets to the extent that you can actually talk about sort of like—obviously don't talk about the training recipes or whatever—but it's interesting that if you're just studying, for instance, math papers, it's a very poor training set a priori for math. Because, I mean, maybe math textbooks are even a pure example of this: it's really bad at actually reconstructing the motivation for why things were... I mean, maybe some people like it, but don't learn real analysis from Rudin! It's very clean already and crisp. And I think that's bad because it doesn't show the struggle that made us formulate definitions in a certain way. Like, why do we even need to have real numbers be defined in this super abstract way, etc.? And so, you know, I think papers also... I mean, most people don't write papers with the context of "I need to educate somebody to be a mathematician", and so the actual curriculum of learning math is not inherent in a lot of our artifacts as mathematicians. So maybe another way to ask this question is: if the reasoning traces are actually producing things that are more close to mathematical thought, how does that arise?

Speaker A: Um, I mean, yeah, I guess OpenAI has been the pioneer of reasoning models and, you know, teaching AI to reason in this way. So we're doing a lot of work in all possible directions on teaching models to reason better and for longer, and 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, like backtracking or kind of starting again... these are not really specific to mathematics. We're seeing them specifically in mathematics in these examples, but they're general purpose tools for reasoning. And I think if you work hard at reasoning, you should see these patterns eventually. Mhm.

Speaker B: So it's emergent? Because I do think that's why the OpenAI approach... it doesn't rely on doing autoformalization in order to guide the reasoning, and I think that's obviously more like us. But it's just so not obvious that if you're just training on say a corpus of math proofs, maybe autoformalized in Lean, that you get the sort of projection of how to think well. Put another way, 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 kind of with books, but they're less structurally interconnected, there's just less structure there on average in a book compared to a piece of code. And so with math papers, 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 why do I have to write it this way. I'm getting too much into the philosophical, but it is just really interesting how it's still emergent that it's doing good mathematics. And we'll probably get into this in more detail if you wanted to talk about some of the problems, which is not just doing the expected "let's push the brute force thing". You clearly are impressed with some of the reasoning traces, and it's just not obvious that's gleaned from what we would imagine would be the easy training set here.

Speaker A: Yeah, absolutely. I mean, I think this kind of...

Researcher A: ...thing is one reason we decided it was important to release like 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 kind of not sure what it means. Like is the model just guessing in some insane way? Like is it thinking in some totally foreign like what's going on? But actually it's reasoning kind of shockingly like an expert human would.

Host: Yeah. Yeah. Yeah, it's very much like reading a colleague's like notes. I mean, it's a little more disorganized in some way. Especially if you work close enough with collaborators, sometimes you'll just see them like spill out their thoughts in an email to you, and it kind of feels like reading a lot of those chained together. So, yeah, it's quite surprising the first few times. Were you two sort of very involved in choosing the problems to release in this like last 10 problem set that Astros applied to?

Host: Which was your favorite?

Researcher A: Yeah, we were definitely involved. Do you want to start on?

Researcher B: Yeah, I mean packing maybe.

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

Host: But we're assuming they are.

Researcher A: Yeah. So the question is just like how dense can you place a bunch of—so you have a bunch of spheres of radius one in $d$ dimensions. So the question is how densely can they pack? And so in two dimensions it's kind of like the—so for $d=1$, this is not an interesting question really, it's just the real line and you can cut it up, and a sphere in dimension one is just a unit segment so okay you can cover everything. So in $d=2$, it's kind of the picture that everybody loves, it's just a bunch of spheres which sort of form like a hexagonal lattice. Hopefully I've drawn it well enough that I can draw the hexagon.

Host: Kind of betraying my naivete on this problem. Is that like obvious? Is there like a very elegant proof that it's lattice?

Researcher A: 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 so easy.

Host: Yeah. Where's the intuition? Like what is kind of like the machinery of the argument?

Researcher B: I mean it definitely looks like it should work. That's why we're...

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

Host: Evolution is efficient.

Researcher A: Yeah. I think beyond that, I don't have a great argument. And I think how little we know is demonstrated by the fact that for $d=3$, the answer is just how you pack oranges in a grocery store. And 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 like a few hundred pages.

Host: And what area does it draw from in order to...

Researcher A: So it's a lot of linear programming arguments and it's very delicate geometry. It's quite ugly actually.

Host: This is like a famously ugly argument.

Researcher A: Oh no.

Researcher A: And then the two most famous results are $d=8$ and $24$.

Host: $8$ and $24$. There must be some like weird subspace.

Researcher A: Yeah, exactly. So this was done in 2017.

Host: Sounds slightly prettier though, I hope.

Researcher A: So the reason it works out in these two very special dimensions is that this is called a lattice packing. So it's very regular, and it turns out in these two dimensions there are two very special lattices. They're called the $E_8$ and Leech lattice, and they're very nice and unusually dense.

Researcher B: They're just very, very pretty structures coming from other areas of math, and it turns out that they're the optimal structures.

Host: But they're still like regular.

Researcher A: Yeah, they're very regular. But beyond this, we don't know any more exact dimensions. We know these five dimensions and we kind of don't know anything else.

Researcher A: And to give an indication of how little we know, there are two very surprising things about this. So you can define $\Delta_d$ to be the densest sphere packing in $d$ dimensions. There's kind of an easy lower bound of like $2^{-d}$.

Researcher B: This is not so hard to show. Basically, any packing where you can't put in another sphere has to have this density.

Researcher A: So, okay, it's not ridiculously small. And we know that it has to decay exponentially—so it decays like it grows like $1 - c$ for some constant. In large dimensions, you can only cover a vanishingly small portion. But we know basically nothing else.

Host: That's just because like the high dimensional sphere thing where it occupies—the volume behavior is weird.

Researcher A: Yeah. Basically they 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. And for a long, long time the best bound was something like this funny number, like $2^{-0.599 d}$. This was proved by two mathematicians in the 70s (Kabatiansky and Levenshtein).

Host: Okay, that's a weird number. Where's that spit out of?

Researcher A: It's the answer to some extremely ugly optimization problem.

Researcher B: There's a nice underlying strategy.

Researcher A: Yeah, I'll say one last thing about this. These were these two Russian mathematicians in the 70s. It's actually very hard to find their paper. It's like two pages long. They don't write very many details because the paper was short.

Host: $2^{-d}$ is just like the square lattice, like the dumb one, or is that...

Researcher A: It's actually not so easy to... The argument for this is as follows: basically imagine that you have a set of spheres and you construct a set of spheres so that you can't put down another sphere, because if you could put down an extra sphere, you just keep putting it down. So you have a set of spheres so that there's no other sphere which you can put down. Take any such packing.

Researcher A: And I claim that this has to cover at least $2^{-d}$ fraction. The reason is that if you blew up each of these spheres by a factor of two, then they have to cover every point in space. And the reason is otherwise if there was any empty space, you could put down a sphere there.

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

Researcher A: Okay. Yeah. So that's actually like a worse bound.

Host: Yeah. You can just keep plopping things in.

Researcher A: Yeah. This is related to this really funny fact where if you take a cube in high dimensions, you put a sphere on every point.

Host: It's like vanishingly small.

Researcher A: It's vanishingly small. It's so small you can put another sphere in the middle and it fits.

Host: High dimensional sphere behavior is weird.

Researcher A: Yeah, very weird. And so the great part is that the model shows the following. So I'll write two things. This is Astra, I guess probably the right way to refer to this. I'm going to write something called the LP bound. I'm...

Speaker A: ...not. I'll explain this in a second. And it shows that it's smaller than this very nice number. Do you want to say equals? Yeah, it's equal essentially to $(e / (2\pi) + o(1))^d$. And if you can work out what this number is, it's like...

Speaker B: It's like roughly something like $2^{-0.6...}$

Speaker A: Close.

Speaker B: Yeah, it's surprising.

Speaker A: But this one, you know, $e$ to... you're like, oh, maybe there's some nicer kind of structure there that fell out. It's at most... this is like roughly something like $2^{-0.61...d}$.

Speaker B: That's the numeric.

Speaker A: I thought it was 604.

Speaker B: Great.

Speaker A: Yeah, this shows mine. Yeah. So okay, so there are a couple of things. So first, what is this $\text{LP}(d)$? So 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. So LP just stands for linear programming. So Cohn and Elkies gave an approach for sphere packing based on linear programming. So it's like a linear optimization problem over a convex set, but it's all kind of infinite-dimensional here.

Speaker A: And basically what this reduces down to is you try to understand the following. So what you try to show is you basically construct a function $f$. So this is in $d$ dimensions and it's mapping to $\mathbb{R}$, and it has the following properties. So first, $f(x)$—this is a function in $d$ dimensions—is always less than zero if the size of $x$ is bigger than 1; and second, you have that the Fourier transform of $x$ is always non-negative. So this is just a linear program because the Fourier transform is a linear operator.

Speaker B: So you're taking just some arbitrary $f$ that satisfies this property.

Speaker A: Yeah. So you can take any $f$ that satisfies these properties. And what they prove is that $\Delta_d$ is bounded by the ratio of the Fourier transform at zero... of $f(0)$ over the Fourier transform at zero times the volume of the ball of radius $1/2$ in $d$ dimensions. And so, okay, this proof is not so short... for experienced mathematicians it took half a paragraph to prove it, but it's a little bit tricky.

Speaker A: And the point is, so it turns out this is a relaxation problem. There's no guarantee that taking the optimal $f$ will give you a good bound on $\Delta_d$. But what Viazovska did—and this was sort of the key, I mean a large part of the reason she won a Fields Medal in 2022 was that—she constructed a function in 8 and 24 dimensions such that this upper bound matches exactly these two very special lattices.

Speaker B: And these are kind of miracles of nature that both you can construct this function and that it gives you the optimal bound. But this is a very, very natural problem. I mean, it's a function with two very simple properties, and you just want to understand how this behaves for large dimensions $d$, and that was a big mystery. There was a numeric paper by Cohn and several others which conjectured that, just based on doing numerics, that this was the answer, but they had no idea why this would be the answer.

Speaker A: And what the model shows is that actually the linear programming bound in large dimensions has this extremely nice asymptotic behavior, and the proof kind of explains where this is coming from. And because you understand this LP bound perfectly, this actually just gives a better bound on $\Delta_d$. It turns out that this old bound can be kind of reinterpreted in this framework, and what the model does is it shows you the best possible bound you can get by this framework.

Speaker B: So the model sort of made the connection and...

Speaker A: Yes. The model gives a function $f$ which... so first it constructs a function $f$ which gives you this bound, and then it shows that there's no function $f$ which does any better. So it's an equality, which is quite strong. So we now understand this problem in high dimensions very well.

Speaker B: And that's pretty remarkable.

Speaker A: And the model was just kind of told like, "Analyze this linear program in high dimensions, you know, go have fun." And to give an indication of how little... I think this conjecture was based basically only by doing numerics—extremely clever numerics, but numerics—and so you have to kind of figure out why this is the right thing to aim for, and it does, and that was pretty remarkable.

Speaker A: Yeah, I mean, I had actually thought about this problem for about six months at some point when I was a graduate student and, yeah, just... I remember making like absolutely zero progress on it. So it was very nice to be explained why it was... yeah, why it was true. So that was a pleasant experience.

Speaker B: I think also in general it was one of these solutions which... I knew several people had tried the problem. It's pretty remarkable because the model's solution, especially for this being like that the LP can't do better than this, was quite short. It's a few pages of complex analysis, but it's kind of exactly the right approach. Like once you see it, it's unbelievable, like why hadn't somebody done this before? There are many types of good mathematics, but I think one of them is just like you see it and you're like, "Oh man, why didn't I think of this?" And it was really fun and... I mean, I sort of knew why I didn't think of it, but it was quite nice to see it and it was fun to see. That's why I like this problem a lot.

Speaker A: Yeah. So this is the first of the 10 problems that Astra saw. But the second is actually closely related.

Speaker B: So this was sphere packing. The second one is spherical and binary codes.

Speaker A: So what's... you should draw a code. You drew a packing. It's going to be the same picture. Okay, sure, sure.

Speaker B: Otherwise, we're going to have his picture packing in our mind.

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

Speaker B: Yeah. So, I mean, a spherical code is basically just a sphere packing on the surface of another sphere. So, yeah.

Speaker A: Yeah, it looks like a sphere.

Speaker B: Yeah. Okay. So, same picture as before, except you're kind of on a curved surface. Okay, okay.

Speaker A: Okay. So why is it called a code? Well, I guess the reason is because of binary codes, which is again the same sort of thing, but now it's on a cube. Okay. Yeah, fine. Let me draw a picture of a cube and some simplest possible code on it.

Speaker A: So like when you're sending... so this is really like about error-correcting codes. So what are error-correcting codes? So, you know, it's like I send you some string of bits, right? And maybe I'm worried that some of the bits I send you get corrupted, right? So maybe like just because of some errors in my system, like this one gets changed, and we want some communication protocol so that like you can decode this like small amount of error and like recover what I was trying to tell you.

Speaker A: And you know, like normal English language kind of has this sort of property, right? If I make a few typos, you know, you're going to be able to understand what I'm saying. But if we have some like really brittle communication scheme, it's not going to work. So codes are kind of the way you solve this.

Speaker A: And mathematically, it just means like, you know, what's a binary string like this of a fixed length? It's like a point on some hypercube.

Speaker B: Mhm.

Speaker A: And we want a dictionary of allowable codewords that are like separated from each other. So, like in this case, if I don't want any two to be adjacent, I would kind of take these four vertices, kind of the even ones if you sum up the digits, right? And like okay, I guess in this case if I have an error you can't tell which one it's from, but at least you can tell it's like not...

Speaker A: ...at least you can tell there was an error.

Speaker B: Oh I see. I see. Yeah. Yeah. Because it's like kind of sparse in the... Yeah. It's like it's not two adjacent. So that like is this is like when the Hamming distance is not...

Speaker A: Yeah. Yeah. Right. Right. You want Yeah. So you want like a large Hamming distance between any distinct in your in your dictionary.

Speaker B: And Yeah. I guess if you take two opposite corners then if I have like a single bit error I can always like recover which point it was coming from

Speaker A: the one that it's definitely closest to.

Speaker B: Yeah. So there's kind of the same question in both of these cases like in a very high-dimensional setting what kind of rate can you get?

Speaker A: And like for binary codes it's really like you know an extremely practical question. It's sort of like if I send you like an n-bit string and there's like 1% error rate, like how much longer does my message have to become to tolerate that amount of errors,

Speaker B: right this like some fundamental information theoretic limit of like communication. And you know, but you can see certainly this spherical case looks very much like sphere packing. For example, if you make all these little spheres really small, then the curvature of the big sphere is kind of not going to matter so much, and it looks like just packing spheres in full space.

Speaker A: Um, and in fact, yeah, like these problems turned out to be very related. So for these problems, there were similar bounds coming from these KL authors, and like there's like something for the sphere and something for the cube, but it's all kind of the same stuff. Mhm.

Speaker A: And our models found better bounds for these cases as well. And like the techniques look pretty different actually if you write them out. So this full space analysis of this linear programming was using like just complex analysis.

Speaker A: Um but the method for these cases were using representation theory.

Speaker B: Oh,

Speaker A: like both the sphere and the cube have a lot of symmetry and basically the idea of the proof was to really leverage this symmetry. Like there's some amount of this in the previous existing method and really the improvement is to lean into the representation theory like really hard and kind of make the algebraic symmetry enter in a more sophisticated way. And then it turns out that from the representation theory formulas, if you kind of take this small sphere limit in the spherical code case, you recover part of this result and you recover this value. So this result isn't a special case. You kind of only went one direction of the bound from looking at it from the code's point of view. But like there's like a very close connection.

Speaker B: Okay.

Speaker A: Yeah.

Speaker B: Yeah. Yeah. So you guys let this like run in parallel. So it's like kind of discovering, or because you're not sort of like feeding it.

Speaker A: So actually this was the one case where there was some interactivity involved. Interesting. So for all of, so except for this pair, it was just, you know, we had some problems, we fed them in, and the model came back with some solutions.

Speaker A: Um what happened here was actually pretty interesting. So we first asked it to improve the bound for the codes.

Speaker B: Mhm.

Speaker A: And it came back with an improvement that like used some amount of representation theory. And then we kind of asked it, hey, can you like push this further, like you know what happens? And then it came back with some like much more sophisticated representation theory, and it turned out that you got this conjectured value for full space sphere packing out of that method by pushing it as far as it can go. So then we kind of ask to directly analyze the sky and try to complete the picture.

Speaker B: Okay.

Speaker A: Yeah.

Speaker B: So the relationship isn't a coincidence.

Speaker A: Yeah. Yeah.

Speaker B: It's like interesting when you're saying the first prompt, which is you know maybe so basic, which is like 'can you push this further?' It does require some judgment from mathematicians. But like eventually you would imagine by scaling the models you don't need to do that, or there's another view that the harness actually does matter, and this is kind of part of the harness apparatus. Do you guys have any views on that with your working with Astra, especially generations of models and how how much you have to kind of input or how much the harness matters versus not.

Speaker A: I mean, yeah, I guess there have been some like funny quirks like this that just come from exactly what you asked the model to do basically. Like in this case, what the model was asked to do originally for codes was to improve the bounds by like some exponential factor. So it really shows up in this leading constant up here.

Speaker B: Mhm.

Speaker A: Um and you know it improved the bounds and it didn't try to push things too much further. Like sometimes you see it do but sometimes it just doesn't bother, but yeah you know you just ask it again and it goes further. So it wasn't like a capabilities issue. It just kind of didn't feel like it at the time.

Speaker B: Do you call that judgment or like what is the... because like there is a... Yeah. What do you call that?

Speaker A: 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.

Speaker B: So yeah, like the task orientedness it's like but do we expect that level to kind of ascend up to... it's not that they will be less good at being task oriented. It's like they'll ascend to the level of like okay no let's let's go in this direction. You'll have the judgment because you guys had the judgment. You're like okay this is pretty promising. Looks like you're using a lot of representation theory. It doesn't seem like there's a limit so far. Um, but it doesn't have that context yet. But like I guess what I'm trying to say is like this one it's hard to maybe extra harder to extrapolate. But from like previous generations when you had to give it more maybe prompting more of that harness work but eventually you probably had to give it less. So it probably gives you some confidence that there's this like really fast ascension. And do you see, yeah, somehow solving a harder math problem is like you have to solve many smaller like somewhat less hard math problems and the fact that the math problems are getting harder is kind of an indication that you're the model is able to take on more and more work in like a single continuous unit. Um and I think that's that's the thing that looks very promising somehow like any of these solutions it's not like one idea and then you're kind of home free. You need several pieces to kind of interact and talk to each other. And

Speaker B: the models I the model doesn't come up with all the ideas at once, right? It doesn't pull everything out of in in an instance of kind of the fact that it needs to sort of 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 okay when you're telling it okay push this even further that was of the same order of like magnitude as like all the smaller things it's solving as well in between and so you don't think that's kind of like a privilege direction it's just sort of like hey let's give it like one one more help or you actually think that there's I guess what I'm trying to get at a bigger question is like is there a good sense of like you know taste because like when people talk about for instance how well the models are getting at like um doing research for instance that's what we you know we want a little bit of RSI um and and sort of like there's surprising things about how that improves and then there's like the oh you know maybe right now it's

Speaker A: ...at a level of still like a junior researcher, it's like not really asking like the right problems. And so I'm just trying to get like a maybe a sense of like where you're seeing that progress through the model advancements each generation. I mean, what is taste even?

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

I think occasionally, because they are task-oriented, you do occasionally get these symptoms of like: "Oh, it clearly has made a breakthrough, it kind of understands it's made a breakthrough, and then it doesn't kind of 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.

Speaker A: Okay, yeah. I think it's a pretty clear...

Speaker B: Like, I think maybe you're liable to get confused if you're trying to like do a concrete long horizon task and show taste kind of at the same time. But like, you know, if you have like 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—kind of as the underling of the supervising AI—I feel like that's kind of going to be fine currently.

Speaker A: Oh, interesting. Because that is like saying that these two things are somewhat, if not separate, at least they shouldn't kind of pollute each other's contexts, which is a little bit... I mean it could be potentially like a stronger statement than I guess.

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

Um, but like why would a separate model, a separate generation, or something that's a different version of the model contribute to taste? Or maybe that's totally too abstract and doesn't make any sense, and we should just let the actual... This might lead to the related question: what is the thing that gets us to a better version of intelligence—the harness and the model, or is it just the model?

And it's like we see this, at least in applied AI or startups, where it's a continual battle: you need the harness, but then the harness adapts very poorly to a new model, because sometimes a very minimal harness is still the best way to expose the raw power of the model. But then now we also have these training regimes where we require the harness to be trained with it. I mean, maybe part of this is to keep things more proprietary and harder for other people to use, but I think partially it's maybe actually that it helps have more control on like the reasoning traces you care about.

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

I think my only like non-trivial thought here is that like when you're working—I mean just when you're doing any task—occasionally you get pigeonholed and you like work really hard, and just having a friend look over your shoulder and be like...

Speaker B: ...what are you doing? And then just having that one bit of like step back for 10 seconds—this is often very useful.

Speaker A: Yeah. Yeah. I mean, I see no reason why humans would be so different than models somehow.

Speaker B: Having—or models would be so different than humans.

Speaker A: Having a few humans working together is often more powerful than just having one.

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

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

Speaker B: Mhm.

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

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

Speaker B: So maybe the the first question is what is a group? Let's remind ourselves.

So uh a group is uh a set of elements with some multiplication operation. And uh basically this is how mathematicians think about symmetry. So, so you're like basically like if G and H are elements of your group, then GH has some is some other well-defined uh element of your group and you have like uh associativity uh and you have an inverse. So for every G there's some inverse uh and there's some like specific element in the group that uh is is kind of the identity.

Uh okay so you know it's it's some like abstraction of like uh composing operations. So these could be like numbers they could be like multiplying matrices they could be like like rotating something which is you know a special case of multiplying matrices.

Um and uh groups that can be finite or infinite. So like you know um if if you have like a square like all the rotations of it form a group with like four elements.

Speaker A: If you have like a circle then the rotations form a group with like uncountably many elements.

Speaker B: Um and uh so sofic groups are either finite or countable. You should think of them as being countably infinite. So there's like the same number of elements as like the integers.

and uh it's sofic if in some sense uh it can be uh approximated by finite groups. So we didn't know if there was a non-sofic group. So so the the the result that uh Astra proved...

Speaker A: ...is simply that uh there exists a non-sofic group.

Speaker B: Yeah. And without like I mean we can you know before going to to that proof it is like you know it's like I feel like a lot of the programs of math is like okay we are such finite creatures let's see how well our finite approximations are you know uh do.

and in this case especially for the countable case it's like maybe you'll be relating it to like the Aldous-Lyons thing. It's just like it helps kind of anchor the picture of like it seems like such a I mean it's a nice result if it were true, but it it's not and it seems almost like reasonable. And so yeah, I I actually didn't um didn't uh go I would love to hear the explanation of like how it it found a counter example.

Speaker A: Yeah, I mean I I would say that like you know the the hope that there was no non-sofic group so every group has this kind of approximation like maybe this is sort of like people hoping that there's a miracle

because uh it turns out that groups like this have a lot of nice properties um because uh you can run certain proofs for finite groups and then uh you know kind of approximate them in whatever way the definition of being sofic lets you approximate them and get the result.

So, so like um there's this notion of being a surjunctive group. So there's uh there's some fact that uh any uh group which is sofic is uh also surjunctive.

Speaker A: Surjunctive is some property of dynamical systems on the group. And I guess the original question was whether every group is surjunctive. This is some question of Gottschalk from the 70s. And this fact follows this pattern of: prove it for finite groups and then do this approximation. That is what motivated the question about whether there's a non-sofic group.

Speaker B: Mhm. Yeah, maybe I'll say a little bit about this Aldous-Lyons conjecture and...

Speaker A: Yeah, sure, yeah, yeah.

Speaker B: So 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 some nice property called unimodularity—a unimodular random graph—can be approximated by large finite graphs. So maybe the way to explain what these kinds of things are trying to say without getting into technical weeds is to say what they mean about the integers.

Speaker B: So how would I draw the integers as a graph? This is called a Cayley graph; you're just going to connect nearest neighbors. Okay, so there's some kind of canonical way in which this is the graph that represents the integers. And there's some sense in which you can approximate this by finite graphs. Why? Well, if you look at integers mod $n$, then you kind of get the same picture, but you have a big circle instead of an infinite line. And 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 kind of see this global geometric structure that you have a circle and not a line.

Speaker A: Mhm.

Speaker B: And in fact, the integers and 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 kind of why the integers are a sofic group. So the statement that every group is sofic is sort of a generalization of the fact that you can do this approximation with groups. And this Aldous-Lyons conjecture is kind of a broader conjecture that for any network you can do this, and you don't require as much algebraic structure, roughly. So it's kind of a broader conjecture.

Speaker B: So this conjecture was disproved earlier, like two years ago, and it was kind of a real tour de force work—like 250 pages building on another 200 pages. It uses quantum complexity theory, so it really builds this very complicated bridge, and I think not very many people could understand this. Right. So since this is a stronger conjecture, the disproof is weaker than disproving this statement that all groups are sofic.

Speaker B: 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 like 15 pages maybe, and it doesn't have any of this very complicated connection with quantum complexity. It just kind of stays in group theory land. I mean, it uses some important existing results by other mathematicians like Kun and Thom, but it's like a very reasonable, normal kind of proof.

Speaker A: Yeah. And kind of spelling out the obvious, but the connection between the sofic group statement is just you take the Cayley graph, and that's the one that they use for Aldous-Lyons.

Speaker B: Yeah.

Speaker A: Yeah. And so that's why it's like a subset of...

Speaker B: Right. So basically what happens is for a group you can take exactly a Cayley graph: you take some elements that generate the group and you kind of connect elements that are adjacent. So in this case, this is a Cayley graph of the integers. Right, so when you do that from a group you get a deterministic graph—you just get a single graph once you fix some 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 it can be random. But basically that's the difference. Here you kind of have to give a deterministic network instead of a random one.

Speaker A: Yeah. Anything kind of interesting or surprising about the result? I mean, you mentioned some things, which is like it stayed within group theory techniques.

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

Speaker A: Yeah.

Speaker B: Yeah, but I mean this one, it's 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. So you have to find a concrete way of producing a way of saying this group cannot be sofic. And the proof is actually very short. It's almost a combinatorics argument, but it's a very, very delicate combinatorics argument. And the model somehow needed to both have the right statement and know what pieces exist in the literature, and then execute it correctly, and that's very nice. The difficulty of this problem is that it's just very hard to get your hands on being approximated by any possible finite structure.

Speaker A: I was going to say, what is happening at that countable infinity that's resisting this approximation? Did it give a sense of that when you do a postmortem, when you're like, "Okay, Astra, explain to me what is the..."?

Speaker B: Oh yeah, we did that all right.

Speaker A: What was a good explanation you got out of it?

Speaker B: I think there's some concrete combinatorial obstruction. It's hard to explain, but there's some concrete combinatorics obstruction which, if you read the previous papers, you realize that that's what they couldn't rule out. And Astra found a way to say, "Okay, no, if you add this one extra algebraic fact, this weird conspiracy can't happen." It's very clearly trying to rule out conspiracy that the previous authors had implicitly written about.

Speaker A: Yeah.

Speaker B: And those were the actual suspects, it turned out. So they were sort of on the right track, and then this did the last mile of—well, however you quantify that. But I think, like 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 thousand-page things and you're never going to be able to understand it. But it's been kind of the opposite. Only humans can generate 200-page proofs right now.

Speaker A: Yeah. Well, and also doing that postmortem ends up usually engendering more mathematics because when you do that with humans, that's what breeds new mathematics. So maybe if you alter the prompt a little bit and be like, "How would you generalize this?" or something like that... I don't know if that's been a technique for you guys to have it explore and exploit what it has already developed.

Speaker B: Well, there has been followup on this already, actually by Thom, on whose work this was built. So they...

Speaker A: The math community is coming on.

Speaker B: Yeah, yeah, yeah. Which is kind of what we're hoping, right?

Speaker A: You know, we don't want to be writing lots of follow-up papers ourselves, but if there's some interesting follow-up building out these ideas more and giving more examples of non-systolic groups in this case, we're very, very happy that there's that follow-up.

Speaker B: Yeah. Well, actually maybe that's a great segue into what's the ideal way that this is being taken up by the math community. Because I feel like there's a spectrum of answers from working mathematicians. Some—probably most at this point—are like: "Okay, AI is obviously doing some non-trivial stuff. It would be a disadvantage not to admit that in my workflow." I've definitely heard some stories where people would find it hard to either take AI as a co-author, or like how do you even do kind of attribution this way? But to paint the more optimistic picture: you're saying you want the 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?

Speaker A: I mean, given the fact that the models can produce sophisticated mathematics means that they can help you understand sophisticated mathematics. Occasionally I enjoy looking at the arXiv and I want to understand some proof. I could read the introduction, but in practice it's just much faster to take the PDF, put it into my favorite model, and get an output of what the rough proof strategy is.

Speaker C: Of course, models are going to help us produce exponentially more mathematics, but they also make it much easier to absorb it. And right now, okay, it's still a bit of a challenge back and forth, but I think 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 anyways.

Speaker B: 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 like, okay, whether I'm going to get tenure, etc. So I agree with making it more accessible. If I'm not spending so much time absorbing an area, I can put it into ChatGPT and then expect to—I mean, you guys have an even more powerful model hopefully releasing for other people to enjoy as well. But the positive version of that is actually more people can participate in mathematics. People might be coming with other intuitions and they could actually maybe generate good mathematics. Is that sort of closer to the vision of what you're hoping this is pushing towards? Or what things do you think to be wary of to adapt fast enough to take advantage of AI?

Speaker A: Yeah, I think certainly there will be a lot of changes, right? In math, there are a lot of things that are kind of important for a given result, right? You need someone to come up with it, but you also need people to understand and absorb it, 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 kind of the other stuff was just coming along for the ride. If you manage to prove this thing yourself, you're automatically going to understand it quite well. You're kind of responsible for maintaining it in some sense and explaining it to other people. And now, what was the main bottleneck before is kind of much less of a bottleneck, and these other constraints come into play. So the optimal structuring for organizing the knowledge could look rather different.

Speaker B: Yeah. How does that look? Does this make the field a lot more kind of empirical? Will people do sort of the hard—the first thing that was scarce, which is like all the reasoning—and then... 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, and so understanding, communicating, maybe assembling, having still the human taste—does that sort of remain rarified, and is that how current mathematicians need to adapt and reward contributions? Or is this too much of a caricature and it's something else?

Speaker C: I think certainly understanding how to put—as we get more and more mathematics—put it in a proper framework, and being able to explain it to other humans so that they can also appreciate it. Somehow implicitly we valued this, but it was usually because you were the person proving the result that gave everybody else the understanding. But I think increasingly it would be a function of: you're the human who can sort of give this understanding to other people and help them with it. More of that communal understanding was much more implicit in how we view math in general, but I think it will be an increasingly more explicit and valuable part of the subject.

Speaker A: A nice thing about math is that the ceiling for 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.

Speaker C: And it could be that the field kind of becomes more attached to these big mysteries and less to smaller mysteries that are more like routine.

Speaker B: Yeah. I think that's a positive vision.

Speaker A: I mean also, there are things I spent like months or years of my life wondering about not getting to know...

Speaker B: What a joy when we get them!

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

Speaker B: Exactly. No, I'm excited about this renaissance of results and understanding. I feel like this is such an infinite field—no pun intended—there's just so much that you can actually create here. Especially for somebody like me who's not going to have the time to actually practice mathematics, now there's a lot more that you can actually do in the activity of math.

Speaker A: 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.

Speaker B: Sorry, mathematicians! Yeah, no, it's true. I mean, I think there was just like a dearth of actual people who could do that and 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.

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

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

Speaker A: Yeah, thanks so much for having us.

Speaker C: Yeah, thanks for having us.