职位描述：我们现在在做使用Lean形式化证明IMO题目，目前情况是我们实现了大部分框架的证明，但技术细节处理耗费了太多时间，所以想找个小伙伴一起做
岗位要求:熟悉Lean4语言，可以很好的使用mathlib解决问题，可以远程情况下高效解决问题
业务产品:IMO题目的lean形式化证明
薪资范围:技术细节实现单题目600 根据实现难度可浮动，题量很大，长期合作
公司介绍：太和软件开发工作室
面试方式:微信沟通
欢迎大家，我们现在在做使用Lean形式化证明IMO题目，目前情况是我们实现了大部分框架的证明，但技术细节处理耗费了太多时间，所以想找个小伙伴一起做，绝对真诚，欢迎联系，希望对mathlib熟悉，环境我这边可以提供，欢迎沟通
招聘类型:
职业:
工作方式:
城市:
领域:
8
