1、使用Lean4形式化数学竞赛题目的解题过程，确保形式化结果清晰易懂、符合逻辑并通过Lean验证2、学习最新形式化方法和工具，提升技能，协作解决形式化中的技术难题。
【岗位要求】1、数学/理科相关专业优先，参加过数学竞赛且获奖者优先;精通初高中数学竞赛知识和相关运算，成绩优异;2、熟练应用Lean数据编程语言，能依据国际奥赛的解题步骤答案，输出Lean语言的推理步骤，并验证无误;3、扎实的数学基础，精通形式化定理证明语言Lean4，具备出色的Lean4编程能力，能够熟练运用Lean4进行数学定理的形式化工作;
4、优先考虑具有以下经验者:参与过形式化证明项目对Mathlib有commit经历，熟悉Lean语言元编程，具备训练或部署LLM辅助自动定理证明的经验。