Axiom sets out to build an AI mathematician.
We are the underdog.
4 months old, 2 years late to the game, under 10 FTEs (recently grew to 17), and had 1:5 in funding and in valuation to our competitor.
Today, AxiomProver solved Erdos Problems #124 and #481 in Lean, a 100% verifiable language.
Onwards!