可以直接投简历哇，数学&代码组也在招人~

divisionring (只有平凡理想) 在 ta 的帖子中提到：

请问贵司数学形式化数据（Lean代码等）收集得怎么样了？是否还有一部分资源聚焦在如何输出有形式化代码保证的数学推理上？之前贵司论文里用的是MCTS， 把所有已经得到tactics当作state。但好像确实有学习效率不高的问题？r1出来之后，利用形式化证明器的反馈来进行学习的算法/路线有没有有所改变？

真的对贵司的现有的成果和潜力感到十分的激动。希望有一天我们可以利用大语言模型的可复制性和低廉的推理成本（相对于人力成本）， 让所有人得到有形式保证（不存在幻觉， 起码幻觉可以被检测）的数学教育。