来自 Carina Hong（@CarinaLHong）的推文线程

Axiom的目标是打造一位人工智能数学家。 我们是弱势一方。 公司成立仅 4 个月，比竞争对手晚了 2 年进入市场，员工人数不足 10 人（最近增长到 17 人），融资额和估值只有竞争对手的 1/5。 今天，AxiomProver 用 Lean（一种 100% 可验证的语言）解决了 Erdos 问题 #124 和 #481。 前进！