蚂蚁星助理研究员-AI+Math-Lean语言形式化验证（实习）
Source: https://talent.antgroup.com/campus-position?positionId=26042309773877
Snapshot
- 岗位：【蚂蚁星】助理研究员-AI+Math-Lean语言形式化验证（实习）
- 类别：技术类
- 招聘批次：蚂蚁星- Plan A人才计划实习
- 地点：北京、上海、杭州
- 面试地点：远程
- 发布时间：2026-04-23
- 毕业时间要求：2026-11-01 至 2031-10-31
Why it might matter
- 方向与 Lean / formal verification / theorem proving 直接相关。
- 工业侧目标是把形式化验证迁移到 Rust 程序验证、具身智能体可靠性验证等场景，强调轻量化、规模化和可落地 Demo。
- 可能值得从 PLT / proof engineering / Lean 生态角度看看：他们关心的是数据生成、Rust 验证，还是更 general 的 machine-checkable proof pipeline。
Job description excerpt
部门介绍：通过形式化验证，让安全攸关的软件模块更加 Sound，尽可能消除 bug / 漏洞 / 故障；使形式化验证更“轻量化”和“规模化”，能真正从理论研究走进工业应用。
职位描述：
- 将 Lean 语言的形式化验证技术迁移到 Rust 程序验证，或具身智能体可靠性验证等领域，研究大幅提升形式化验证“轻量化”和“规模化”的方法；
- 基于 Lean 语言的验证框架，产生高质量的数学证明、程序验证类数据，用于基模训练；
- 探索形式化方法，发表高水平论文或专利，提升蚂蚁集团在该领域的业界影响力，与国内外一流机构交流合作。
Requirements excerpt
- 博士生，特别优秀的硕士生亦可；有相关研究背景、成果和经验，在高水平国际会议或者学术期刊发表过相关论文；
- 具备发现问题、提出问题的能力和开发实现能力，能够把研究想法转化为 Demo 应用；
- 良好的表达沟通能力及协作精神，工作认真严谨，有热情和挑战困难的决心；
- 熟悉 Lean。
Suggested links
Follow-up
- 有空时打开原链接，判断是否值得联系/投递/转发给 Lean 或 PLT 相关同学。