Comment by sashank_1509

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.