洪乐潼从 MIT 数竞少年到 AI 数学创业者，其路径充满反常规张力：她不靠功利驱动学数学，却在失败中重塑认知 —— 大一期中考得低于 5 分仍坚持重学实分析；她将‘对苦难上瘾’转化为创业韧性，在签证限制与学术惯性中果断启动 Axiom。公司以 Lean 形式化为核心，突破 auto formalization 瓶颈，实现普特南满分与 20 页自动证明等超人类成果。小野肯教授放弃终身教职加入，印证 AI 并非取代数学家，而是推动人类转向更高阶猜想与抽象。她坚信数学是验证最严苛的‘沙盒’，终将催生可自我验证的推理系统，而人类的好奇心、直觉与跨域协作，永远不可替代。