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.
01:52:46 · Ken Ono, John Coogan, Carina Hong
[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. [01:53:06] S0: Does a, does math exhibit the same slop problem that you see in text and code generation? You know how like you can go to a deep research report, it can write a really, really solid history paper that might be PhD level, no hallucinations. But the experts and people who know this will just say, ah, just the flavor is not quite there or it has it has it has AI written all over it. Does that exist in the lean that is produced like formal proofs? People are like, ah, yes, it works. Congratulations. But it's still a little sloppy. [01:53:45] S6: Three layers. One is correctness. So a lot of in in the past, we'll be worried about correctness. [01:53:50] S0: Sure.