在这场名为《Carina Hong: Frontiers of AI for Mathematical Research》的演讲中，Axiom 的创始人兼 CEO Carina Hong 详细分享了 AI 在数学研究领域的最新前沿进展、所面临的挑战以及他们团队取得的突破性成果。

以下是演讲内容的详细梳理：

一、 Axiom 的愿景与技术路线

团队与目标： Axiom 是一个位于帕罗奥图（Palo Alto）的 40-45 人团队，专注于推进形式化数学（Formal Mathematics）以及可验证推理（Verified Reasoning）的前沿 [00:00]。

核心理念： 团队相信，如果在数学推理任务上取得重大进展，其成果将 100% 形式化并基于 Lean 语言 进行验证，这可以无缝迁移到软件和硬件验证等对安全性要求极高的重要领域 [00:13]。