lean数据实习生

【工作内容】

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

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

【岗位要求】

1、数学/理科相关专业优先，参加过数学竞赛且获奖者优先；精通初高中数学竞赛知识和相关运算，成绩优异;

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

3、扎实的数学基础，精通形式化定理证明语言Lean4，具备出色的Lean4编程能力，能够熟练运用Lean4进行数学定理的形式化工作；

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

【工作说明】

实习薪资：600-800元/题；

工作时间：6月底前每天能有固定的时间参与做题，每天至少3-4小时；

工作地点：支持线上沟通，试标通过后方可进入作业

联系方式：王 18101673033