Lean4-IMO数学研究员

【工作内容】
1. 使用Lean4形式化IMO级数学题，确保形式化结果清晰易懂、符合逻辑并通过Lean验证。
2:学习最新形式化方法和工具，提升技能，协作解决形式化中的技术难题。
【岗位要求】
1.扎实的基础数学基础，精通形式化定理证明语言Lean4，具备出色的Lean4编程能力，能够熟练运用Lean4进行数学定理的形式化工作;
2. 熟悉Lean语言元编程
3. 985/211学校及以上毕业
3. 有数学竞赛经验
【薪酬福利】
IMO级能力时薪：500~1000元/小时
工作地点: 线上办公

全部评论

推荐最新楼层

牛客506437692号

北京大学机器学习

现在还缺人吗

点赞回复分享

发布于 2025-04-08 01:18 北京

01-04 17:49

思摩尔国际（SMOORE）_研发工程师(准入职员工)

思摩尔内推，思摩尔内推码

思摩尔结构工程师一面一面技术面，面试官比较年轻，共23min1、面试官上来要求先说说你对思摩尔的了解2、自我介绍3、针对第一个项目的提问：项目背景？你承担的工作？你在项目中遇到的问题？你最大的收获？这些项目中设计的产品有在企业中应用过吗？没有应用的原因你觉得是什么？4、针对第二个项目的提问：在项目中成员有分歧怎么办？有人不配合怎么办？5、除了学校学习和项目科研的内容，你最近有学习过什么新技术吗？6、反问环节（最长的一次）面试官详细介绍了工作内容后续流程，还有总部的一轮面试思摩尔国际2026全球校园招聘倒计时❗还没拿到offer的同学抓紧时间⏰【急招岗位】①技术研发类硕士（24-30W）：产品企...

点赞评论收藏

2025-12-30 20:55

蚌埠坦克学院嵌入式软件开发

嵌入式面试中遇到过的最刁钻问题

做嵌入式久了会发现，真正让人难受的面试问题，往往不是“会不会用某个外设”，而是那些一听就知道没做过项目根本答不上来的问题。下面这些，就是我遇到过、也确实很刁钻的嵌入式面试问题。1.「这个问题你是怎么复现出来的？」不是问怎么改，而是先问你怎么复现。这类问题在考：你有没有构造测试条件是靠偶然撞到，还是系统性定位有没有复现思路和手段如果项目里没被 bug 折磨过，很难答清楚。2.「设备跑三个月后死机，你会从哪几步开始查？」这是典型的工程经验题，涉及：内存泄漏、堆碎片任务栈溢出看门狗、日志、异常捕获重点不是点名技术，而是你有没有长期运行的意识。3.「中断里能不能用 malloc？你项目里怎么处理的？」...

面试官问过你最刁钻的问题...

点赞评论收藏

01-04 07:53

门头沟学院 C++

😭😭

心愿便利贴：工作了以后回头再看待这个问题，从客观的视角来讲是因为每个人对自己的要求不同，学习好的人对自己的要求很高，所以觉得考不好就天塌了，认为自己学习好并且值得一份好工作的人也是一样，找不到符合自己预期的工作肯定也会觉得是侮辱，牛客上有很多名校大学生，肯定会存在这种好学生心态啊，“做题区”从来都不是贬义词，这是大部分普通人赖以生存的路径，这个有什么好嘲讽的，有“好学生心态”没有错，但是不要给自己太大的压力了

点赞评论收藏