Axiom Math

“If you have more structured and formal data, it's going to be a lot more horizontal than the specific vertical we are tackling.”

“I expect fragmentation to start to happen as Axiom and Harmonic establish category leadership.”

“So actually what happened was our competitor, Harmonic, decided to publicize that they have solved unsolved problems, Erdos number one two four and four 81, and then we trusted their literature review, believing that these problems are really, truly unsolved. …”

“We have good performance, you know, having solved open research questions and number theory, commutative algebra, algebraic geometry, some discrete math that come into Rx and probability.”

“I think that we found scaling inference to have almost no wall recursively decomposing you know, approved goal into many sub goals and then learning to backtrack as well.”

“The DNA of the company is math. We think that verification is the best first market.”

“We are like a seven, eight months old company, so it definitely means a lot to us. It's a really cool milestone. We're currently about like 30 people now, right?”

“At one point we're gonna get to there because, you know, I think the conjecture will probably depend on what, you know, will probably depend on what we mean by taste, elegance. Feels like an alignment problem to me, you know? Like, you know, who gets to say wh…”

“And we actually recently, with no modification to the Putnam system, we saw a 99% out of the 189 problems, we saw a 187, we missed only two code-wisp-proof.”

“Because when we realize the dream, the company's gonna be worth ten billion.”

“And without it, we couldn't have solved it with I think the eight problems within the time limit. Definitely not, not within the time limit.”

“I think this is the future of coding. Yes, I think this is the future of coding. And I think this is where, you know, this is where I think even if we are supposed, like given the assumption that everything can be formally verified, you know, like studying sor…”

“We have some major news in the coming weeks, basically open sourcing entire code bases of mathematical discovery coming up.”

“So we just released AXLE, A-X-L-E, stands for Axiom Lean Engine. And it's really a set of, kind of, proof validation and manipulation tools that are built for Lean in the language of Lean. So it's a bunch of metaprogramming tools.”

“Francois Charton, a member of technical staff at Axiom, and he previously have done Patent Boost and End-to-end, you know, settle this proof, a thirty-year-old conjecture by finding a counterexample found the solution to a one-hundred-and-thirty-year-old probl…”

“No, that's not the TEM. The TEM is all code. The TEM is a right of first refusal on all AI-generated code. Like, right of first refusal, meaning, you know, you get to choose whether you want to verify it.”

“Potentially trying to prove commercial value is going to distract significantly from the core capability improvement.”

“We have seen it scale from 40 notes to 4000 notes.”

“Currently, actually, you know, for each line of code written, there could be like 20 lines of proof.”

“I think a Lean-based system will struggle in those very creative places, which is why we at Axiom actually also invest on something called mathematical discovery.”