AI数学全职工程师招聘

职位亮点

• 参与清华大学交叉信息研究院相关科研项目。
• 聚焦AI + Math前沿方向，接触数学形式化、Lean、自动证明与Agent系统。
• 提供充足的模型、token与研发资源支持。
• 适合基础扎实、成长快、愿意啃难题的年轻全栈工程师。

职位描述

我们正在招聘一批全栈工程师，参与清华大学交叉信息研究院相关的AI+Math科研项目。项目聚焦于借助大模型与智能体系统，推动数学内容的形式化表达、自动证明与可理解化。具体来说，我们主要做三类事情：

• 翻译：将数学教科书、数学论文中的定义、定理、证明和论证过程翻译成Lean等形式化语言。
• 证明：面向具体数学问题，构建能够寻找证明、补全证明并生成Lean证明的系统。
• 解释：帮助人类理解Lean证明背后的思路、结构和关键想法，让形式化证明重新变得可读、可学习、可交流。

这是一个非常偏工程落地的岗位。我们希望你真正参与系统搭建、工具开发、流程打通、数据建设和效果迭代，把研究想法变成可运行、可持续演进的工程系统。这个岗位不参与训练或者微调模型。

智能体系统是一个发展很快、也需要持续积累的方向。我们希望加入的工程师能够在这个岗位上稳定投入，原则上至少工作2年。

岗位要求

• 计算机相关专业，本科及以上学历。
• 编程基础扎实，具备较强的工程实现能力。
• 数学基础较好，逻辑能力强，对抽象问题不排斥。
• 学习速度快，执行力强，愿意处理高难度、非标准化问题。
• 有责任心，能够在前沿方向上持续投入并推进落地。
• 能够与研究团队高效协作，完成系统实现与工程支撑工作。

应聘方式

如果你对这个方向感兴趣，欢迎发送简历或个人介绍至 yuanyang@tsinghua.edu.cn。邮件中可以简要说明你的工程经历、数学或形式化相关背景，以及你希望参与这个方向的原因。