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.
01:50:34 · Ken Ono, Carina Hong, John Coogan
[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. [01:50:56] S6: The psychology behind the scene was, I think, in February, we tried having Axiom Prover tackle research conjectures in fields that are pretty deep, have a lot of theoretical literature. And that was that was successful. So Axiom Prover was able to put on archive a few researched open problem solutions completely automated and also fully in lean without human intervention. That's in February. Immediately, at the beginning of March, we were setting more North Star visions. As Ken said, there's a list of targets that we were excited to go after. The problem of bounded gaps in crimes is a particularly beautiful one. It is a lot of people's childhood dreams. So I think yesterday, I saw Wei Jie Su, an OpenAI researcher, post that when he was nine. He knew about the problem. For me, I was I was 12 years old. I I knew about Itau [01:51:49] S0: Jong. Success. Yeah.
01:51:49 · John Coogan, Carina Hong, Jordi Hays, Ken Ono
[01:51:49] S0: Jong. Success. Yeah. [01:51:51] S6: So so it was Itau Jong's, like, solution of pushing that to the finite balance, 70,000,000, which is a very, very large number compared to today, the new world record. But that is a problem that's very fond to a lot of our hearts. So it's very natural that a lot of people are working on it. Mhmm. I think no one has ownership of any problem, and the word of scientific discoveries is pretty infinite, so you have a lot of problems to go after. We think we will probably enter similar races like the one with OpenAI we just had yesterday in the future. And, also, we are formalizing big problems, so we just saw anthropic announcement on formalization of Fermat's Last Theorem. [01:52:27] S0: Sure. [01:52:27] S6: We have been working on similar things. So we're excited to continue to go head to head with OpenAI and with Anthropic. [01:52:33] S0: I love it. [01:52:34] S6: We are a thirteen month start up, and we we sometimes could be disappointed by, you know, being beaten the world record in a few hours, but we'll keep trying. And I think you're [01:52:44] S1: very much in the game. [01:52:45] S0: In the game. [01:52:46] S4: Yeah. Another thing I wanted to say though is among the problems that are our favorites, there are community so last week, we set a world record on a problem called the parity of the partition function. Mhmm. It's not as famous as as bounded gaps and primes. Sure. But for those communities, it set a world record. So Mhmm. Our portfolio is vast.