公司简介 我们是一家处于创业初期的美国公司，专注于 AI for Math、形式化验证，以及面向数学与证明系统的专用小模型训练 我们希望找到对数学推理、机器证明和机器学习有持续兴趣的伙伴，与创始团队直接合作，共同推进研究与工程实现 岗位职责 根据候选人的研究背景和能力，参与以下工作内容 围绕数学命题与证明开展形式化研究，使用 Lean 4 等工具构建、验证和维护形式化证明 参与数学