01:43:27 · John Coogan, Ken Ono, Carina Hong
[01:43:27] S0: Yeah. Everybody. Everybody is working on this. But do you see these particular challenges as good benchmarks, or is there a more a more broad overarching vision? Or or or is it worth focusing on these specific things like the Riemann hypothesis? [01:43:45] S4: Well, just very quickly, I'm a pure mathematician, so I don't think in the world of benchmarks. Yeah. The problems are there, and I love the problems. Some of the problems get solved, but every time you solve a problem, there are new problems. So I think it's an exciting time. It's very disruptive for the community. Mhmm. It's let's face it. But moving forward, six to eight months from now, I think I think scientific research will be thriving. [01:44:09] S0: Yeah. I think Yeah. Please. [01:44:10] S6: Yeah. The history, I think, has been that every mathematical discovery, like, unlocks, like, either an applied like, an actual real world application, like, hundreds of years down the road, or it even starts, like, new fields in science. So we're very excited about all these mathematical discoveries happening. Mhmm. For the audiences who don't know what's new, we had an exciting week. The very long, astonishingly, notoriously hard problem bounded gap in primes have been the world record has been updated three times this week. First by Julia Stalman, the human mathematician, getting two forty down from two forty six, and then by Axiom Math at two twelve, and then by opening at Astra at one eighty six. So it's a Wow. [01:44:56] S0: Yeah. I'm looking forward. [01:44:57] S4: I I have a blitz.
01:44:57 · Ken Ono, John Coogan, Carina Hong
[01:44:57] S4: I I have a blitz. [01:44:59] S0: Is it ever like this in math? This is this is No. [01:45:01] S4: No. Yesterday. [01:45:02] S0: A football game. [01:45:04] S4: Yeah. That that is all new. There's an analogy, if I could just very quickly say, Freeman Dyson was a very famous mathematician and physicist. And he described mathematics mathematics as mathematicians could be the birds or a mathematician could be a frog. And right now, right now, we're in a position where we're amplifying the flyers. Sure. The ones with vision. [01:45:25] S0: Yeah. I like that. What else can you tell me about reaction from the mathematics profession and also what the role of the mathematician was in the pre AI era and what it might look like in the post AI era because I know a lot of very successful mathematicians who have had full careers as professors and proving theorems and working on these hard problems wasn't something that was really on their resume necessarily. Like they they contributed so much else to the world and they lived full lives and had wonderful careers And it wasn't purely about the the gamesmanship, although we're now it's game on. [01:46:05] S6: Proof Olympics time. [01:46:06] S0: Yeah. Proof Olympics. So [01:46:09] S4: so like I said, I think the questions that we that that I wake up in the morning thinking about Yeah. They're still there. It's just the paradigm. It's the the tools that we use that didn't exist before are amplifying us. Yeah. I think that's where we are. It's a great time.
01:46:09 · Ken Ono, Carina Hong, Jordi Hays
[01:46:09] S4: so like I said, I think the questions that we that that I wake up in the morning thinking about Yeah. They're still there. It's just the paradigm. It's the the tools that we use that didn't exist before are amplifying us. Yeah. I think that's where we are. It's a great time. [01:46:26] S6: So so to track kind of like the the community of mathematicians, but also the community of researchers working on AI for math, Pat Shafto, who is a program manager at DARPA Mhmm. Organizes this sort of meetup every every two months or every three months. And we just went to the last edition of that. It was, like, two weeks ago in Seattle. Terry Tau was there. Alice was there. Boris Alexi from OpenAI was there. A lot of the academics who are working on harness engineering that are great mathematicians are there. A lot of industry AI researchers are there, including people from OpenAI. We were there, and AWS was there. The the energy is incredible. I think it's like the it was like a three day, like, research program. Everyone was reporting their newest, the open source model. Godo Prover has version three. That's Princeton Labs, Sanjeev Arora's. The community is thriving. I think we're, like, seeing these incredible number of open problems that suddenly become attainable because of the technology advancing. [01:47:33] S1: How do how do you guys make money? Yeah. [01:47:37] S6: That's a great question. I think the word is going [01:47:39] S4: She paged me. [01:47:45] S1: Oh,
01:47:45 · Jordi Hays, Carina Hong, Ken Ono, John Coogan
[01:47:45] S1: Oh, [01:47:46] S6: wow. The word the word is going to, I think, run on a different kind of flywheel of generation and verification. So we don't really think of formal verification as kind of, like, guarding or, like, capping the downside. We think of it in terms of performance, and we think of it as optimization. So by having the cost of proof reduced to zero, you can generate new algorithms. You can make new scientific discoveries. It's going to have important implications in the world of coding, in the world of AI for science, and other, like, physical engineering disciplines that we couldn't think of in the past. [01:48:23] S4: So put another way, the world runs on code that people don't understand, many people haven't even read. So software verification, hardware verification, as Carina says, is kind of the challenge for the future and that's really like doing math. [01:48:39] S0: So lean startup of the future. All code written in lean or something like that. Formal verification coming to all software for with cyber security benefits potentially. Is that the idea? [01:48:52] S6: Are a lot of different viewpoints on this. So, I've met researchers who think that, all the word software should be rewritten. [01:48:58] S1: Yeah.
01:48:58 · Jordi Hays, Carina Hong
[01:48:58] S1: Yeah. [01:48:58] S6: There are other people who believe, wow, we should formally verify everything. Yeah. The truth is, I think, somewhere in the middle. Mhmm. People traditionally think of formal verification as something that you get zero credit for if you don't formally prove everything. Mhmm. We think partial verification has a lot of value. By decomposing or refactoring, each word has its own, like, loaded meaning Yeah. A very difficult problem into subproblems, a very difficult coding challenge, coding task into different modules. You can get assurance in certain parts and try to, just lock in and optimize because you now have that formal guarantee. Yeah. So it's, again, this idea of verification for better performance. [01:49:37] S1: I love it. Can you can you guys walk me through your your basically psychology when you're working on some of these open problems and you know that there's a bunch of different teams that are also working on the same set of problems. And it it feels like one of those things like where there's insane urgency because you could spend three weeks Yeah. Working with models and your own harness and tools like trying to solve something and then someone comes out with it and it's like, you know, the whole the you you don't get any credit for for your work because someone beat you to it. But do you are you feeling that pressure right now or is there are there enough like sort of disparate problems that Yeah.
01:49:37 · Jordi Hays, Ken Ono, John Coogan
[01:49:37] S1: I love it. Can you can you guys walk me through your your basically psychology when you're working on some of these open problems and you know that there's a bunch of different teams that are also working on the same set of problems. And it it feels like one of those things like where there's insane urgency because you could spend three weeks Yeah. Working with models and your own harness and tools like trying to solve something and then someone comes out with it and it's like, you know, the whole the you you don't get any credit for for your work because someone beat you to it. But do you are you feeling that pressure right now or is there are there enough like sort of disparate problems that Yeah. [01:50:15] S4: That that's a great question. So the way we do it here Acxiom, we have little team called the a team, small but mighty. We have a list of problems that are our favorites. And on that list, there are some big problems like bounded gaps and primes, which we know the whole world of mathematics cares about. [01:50:34] S0: Yeah. [01:50:34] S4: So to tell you the truth, I'm not in a race with them until we get the idea that we're all onto the same problem. And recently, Julia Staubman's paper that came out a few days ago was a landmark moment. When that appears on the archive, you know that everyone in the world and the community is trying to optimize that. So there was crazy urgency the last couple of days. Sure.