【岗位描述】：

1、能够使用Lean4等形式化数学竞赛题目的解题过程，确保形式化结果清晰易懂、符合逻辑并通过Lean验证；

2、协助产研团队，验证算法链路的准确性，提升大模型自动化数据加工链路的效率；

3、学习最新形式化方法和工具，提升技能，协作解决形式化中的技术难题。

【岗位要求】 ：

1、数学/理科相关专业优先；精通初高中数学竞赛知识和相关运算，成绩优异；

2、熟练应用Lean数据编程语言，能依据国际奥赛的解题步骤答案，输出Lean语言的推理步骤，并验证无误;

3、扎实的数学基础，精通形式化定理证明语言Lean4；

4、优先考虑具有以下经验者：参与过形式化证明项目对Mathlib有commit经历，熟悉Lean语言元编程，具备训练或部署LLM辅助自动定理证明的经验。