應屆畢業生
學歷不限
2025-09-03 15:59:22
1367人關注
職位描述
該職位還未進行加V認證，請仔細了解后再進行投遞！
【工作內容】
1、使用Lean4形式化數學競賽題目的解題過程，確保形式化結果清晰易懂、符合邏輯并通過Lean驗證
2、學習最新形式化方法和工具，提升技能，協作解決形式化中的技術難題。
薪資面議，可談 ！ 【崗位要求】 1、數學/理科相關專業優先，參加過數學競賽且獲獎者優先;精通初高中數學競賽知識和相關運算，成績優異; 2、熟練應用Lean數據編程語言，能依據國際奧賽的解題步驟答案，輸出Lean語言的推理步驟，并驗證無誤; 3、扎實的數學基礎，精通形式化定理證明語言Lean4，具備出色的Lean4編程能力，能夠熟練運用Lean4進行數學定理的形式化工作; 4、優先考慮具有以下經驗者:參與過形式化證明項目對Mathlib有commit經歷，熟悉Lean語言元編程，具備訓練或部署LLM輔助自動定理證明的經驗。
注：聯系我時，請說是在辛集人才網上看到的。
工作地點
地址：北京海淀區北京海淀區清華大學1
求職提示：用人單位發布虛假招聘信息，或以任何名義向求職者收取財物（如體檢費、置裝費、押金、服裝費、培訓費、身份證、畢業證等），均涉嫌違法，請求職者務必提高警惕。
職位發布者
田女士HR
悠派才選(上海)人力資源有限公司
-
咨詢（財會·法律·人力資源）
-
51-99人
-
私營·民營企業
-
五角場街道雙陽北路363號(黃興公園地鐵站2號口步行430米)
