一、项目简介 本项目旨在使用 Lean4 工具对抽象代数中的数学定理进行形式化证明，构建可读、可验证、可复用的数学知识体系。我们将提供培训内容，帮助参与者快速掌握相关技能，并与团队协作解决形式化建模问题。 二、工作内容 1. 学习并掌握 Lean4 形式化工具及方法； 2. 使用 Lean4 对抽象代数中的定理与概念进行形式化编码； 3. 阅读、理解并标注已有数学定理及其证明过程，确保形式化逻辑严谨、清晰、可验证。 三、人员要求 专业背景： 1. 数学或计算机相关专业（方向为代数/形式化方法优先）； 2. 本科为 985/211 院校优先，或普通高校的研究生； 技术能力： 1. 熟练掌握 Lean4，有扎实的抽象代数基础； 2. 有 Lean4 实际项目经验者优先，特别是对 mathlib 有 commit 记录的同学； 3. 熟悉 Lean 元编程或有 LLM（大语言模型）辅助定理证明经验者优先； 其他：有充足时间参与项目（可远程/线上实习）。 四、项目情况 项目规模：共约 3000 道数学题/定理 项目周期：即日起启动，至少持续至 6 月底，可能延长至 8 月底 项目形式：线上为主，提供必要培训及技术支持 五、薪酬安排 培训考核期间：100 元/天 考核通过后：450～500 元/天（需完成测试） *按八小时工作时间计算，不满一天按时薪折算