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

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

victorchen (天使在云端) 在 ta 的帖子中提到：

【发帖背景】

大概一年多前的时候，我发过一个数据招百晓生的帖子，但是现在时间过去了太久可能大家以为失效了，最近又是公司发展比较快的时候（晚上看群里，DAU已经有4kw了）衷心希望有更多热爱AI、愿意参与AI浪潮的学弟学妹们加入我们~

如果要我说我对于这个岗位的理解，

……