Short answer: Carina says compute is not the bottleneck; data is. There are over 1 trillion tokens of Python code but only about 10 million of Lean, a 100,000 times gap, so Axiom generates synthetic data and auto-formalizes existing math.
Watch this answer from Episode 22 (starts at 11:14) · Episode 22 notes and transcript
From Episode 22: Let's do the Math!, starting at 11:14.
Carina [11:14]: I think it's a it's it's it's close. Well, I think we use, a lot of both GPU and CPU in our engineering effort. There's, obviously, the large language models part run on the GPU and the LIMPod, currently compiles through CPU. And there's interesting engineering problem as to how to maximize utilization because there is some sort of dragging it down, in fact, because CPU generally, could work a little bit challenging with the GPU. But I wouldn't say that the compute part is kind of the bottleneck. I think the difficult part is the data scarcity, which is there isn't there that much lean. There just isn't that much lean. And there are more than 1,000,000,000,000 tokens of Python code, only about, like, 10,000,000 tokens of lean code. That's a 100,000 times data gap. So that's, I think, what is really, really hot.
Jordan Metzner [12:08]: Yeah. So, speaking of that, how I guess, like, artificial data becomes much more important in generating artificial lean problems
Carina [12:16]: 100%.
Jordan Metzner [12:16]: If that becomes, more critical in sourcing the data because you can't just go to a library and buy, a nineteen twenties book on lean. Right?
Carina [12:24]: Well, I guess a lot of the companies I know, especially some Chinese companies working on this, are having a massive number of, like, lean data labelers, lean programmers to try to generate human data. Of course, that's very expensive. Doesn't scale as well. We have where both database own synthetic data generation, both by converting the informal data that already exist, scrape them, and, really augment them in a way that makes sense to convert to lean, auto formalization. We also have other efforts. So given formal data, formal math data already in lean and that's your seed data, how do you make that 101,000 times Williams larger?
