I’m not sure what axiom maths business model is, seems like excesses of AI boom era.
No one’s gonna care for formalizing a 10,000 page math proof with 46M lines of Lean code, unless it is very cheap to do, which seems unlikely.
No one’s gonna care for formalizing a 10,000 page math proof with 46M lines of Lean code, unless it is very cheap to do, which seems unlikely.
Making it cheap to do is probably exactly what they're trying to do. Formal proofs for verification take 10-20x as many lines as the core functional code being verified. Nobody's going to want to pay for 10-20x as many tokens at frontier pricing for verification unless they have to or it yields tremendous benefits. So getting the token price down as low as possible for a prover is probably a core part of the value proposition.
Like, proving that in the absence of hardware faults, some optimizer for JavaScript can never result in arbitrary memory accesses.
Or that some database doesn't violate data semantics under ANY condition.
Or that as long as not too many sensors fail, a plane autopilot will not go and do anything that would lead the plane to exceed safe speeds and forces/accelerations. (Won't just go crash the plane or drop it from the sky in one or more pieces just because some few sensors froze or caught lightning or something.)