上海交通大學“AI4Math：Lean4與數學形式化”暑期學校報名通知

發布時間：2025-05-23 編輯：保研喵

添加上海交通大學學姐微信，或微信搜索公眾號“保研喵”，關注[保研喵]微信公眾號，在保研喵微信號輸入[上海交通大學保研夏令營條件、上海交通大學保研加分細則、上海交通大學保研群、上海交通大學保研學姐微信、上海交通大學保研真題、上海交通大學夏令營]即可在手機上查看相對應上海交通大學保研信息和免費資源。
回復[夏令營信息][保研去向][保研來源][入營名單]即可查看蕞新蕞全的保研數據。

上海交通大學“AI4Math：Lean4與數學形式化”暑期學校報名通知內容如下，更多考研資訊請關注我們網站的更新！敬請收藏本站，或下載我們的考研派APP和考研派微信公眾號。

上海交通大學“AI4Math：Lean4與數學形式化”暑期學校報名通知 正文

 

近年來，大語言模型的推理能力，尤其是在數學問題求解和證明中的應用成為一大研究熱點。然而，數學對推理的嚴謹性要求極高，單純依賴語言模型極易出現幻覺等錯誤。如何將數學的知識與邏輯融入大語言模型，以消除幻覺、提升推理能力和保證嚴謹性受到日益增加的關注。過去幾年，數學形式化逐漸成為一個被廣泛采用的可行途徑。目前，數學形式化的主要工具為Lean4等，該語言功能強大，但入門門檻較高，限制了它的普及度。
基于上述背景，上海交通大學數學科學學院機器學習研究所、自然科學研究院，北京大學國際數學研究中心和國際機器學習研究中心擬聯合舉辦“AI4Math：Lean4與數學形式化”暑期學校，以推廣Lean4語言和數學形式化，推動AI4Math的發展。本次暑期學校將包含兩個專題，分別為專題一：Lean4基礎和專題二：數值代數形式化。
組織者：
羅濤，上海交通大學數學科學學院副教授
梁經緯，上海交通大學自然科學研究院副教授
董彬，北京大學國際數學研究中心教授
文再文，北京大學國際數學研究中心教授
專題一： Lean4基礎
時間：2025年7月14 - 20日
規模：計劃招生人數為25人。
一、報名條件
1.數學或計算機科學等相關專業的本科生或低年級研究生。
2.具有較強的數學素養，對數學形式化感興趣。
3.具備一定編程基礎的學生優先考慮。
二、食宿安排
為非上海地區的學生提供住宿補助1000元，為所有同學提供餐費補助300元。
三、課程安排
完成分組課題，并進行展示。在學員的意愿基礎上，擇優選擇部分學生進入專題二繼續學習。
專題二：數值代數與形式化
時間：2025年7月14日 - 2025年8月3日
規模：招生人數為20人。
一、報名條件
1.數學或計算機科學等相關專業的二三年級本科生優先考慮。
2.有編程基礎、數值代數相關基礎的學生優先考慮。
3.有數學或相關競賽經歷的學生優先考慮。
4.結課后仍能持續投入時間和精力：積極參與交流討論，聽從導師與助教的安排和指導。
二、食宿安排
為非上海地區的同學提供免費住宿，為所有同學提供餐費補助300元/周。
三、課程安排
1.第一階段（7月14-20日）：進行Lean4的學習，完成Lean提供的Mathematics in Lean中10道練習題。
2.第二階段：
a.（7月21-27日）協助整理數學定理證明的自然言語版本；完成導師指定的數值代數相關的形式化證明。
b.（7月28日-8月3日）進行數值代數的形式化。
3.第三階段：我們將從完成第二階段的學員中擇優選擇10名同學，于8月底集中進行數學形式化工作。具體細節將另行通知。
注：前兩周都設有考核，不達標的同學不能繼續下一階段的學習。
報名材料與方式
一、報名材料
1.成績單（教務部門出具）。
2.競賽獲獎證書等補充材料。
3.個人簡歷和陳述。
二、報名方式
1.網上報名：
通過網址https://wj.sjtu.edu.cn/q/bKSvNqG5填寫在線報名表。（注：交大學生也要報名）
2.將報名材料按照報名材料順序合并轉成一個PDF文檔，文檔命名格式為：“專題一/二+學生姓名+學校名稱”（如專題一+張三+上海交通大學）。將電子文檔發送至郵箱：AI4MathSJTU@163.com，郵件主題命名格式為：`專題一/二+學生姓名+學校名稱`。
注：以郵件收到的報名材料為準，僅在網上報名而不按照要求發送電子材料視為報名無效。
3.報名截止日期為2025年6月15日。
結業形式

1.兩個專題的學生完成相應的課程任務后可獲得結業證書。
2.表現優異的學生將獲得組委會頒發的榮譽證書。
聯系方式

郵箱：AI4MathSJTU@163.com
課程大綱

課程時間：2025年7月14日 - 2025年8月3日
專題一： 2025年7月14日 - 2025年7月20日
 
專題二： 2025年7月14日 - 2025年8月3日
數值代數授課老師：羅濤，梁經緯
 

上海交通大學相關保研資源下載：

上海交通大學歷年保研筆試/面試真題匯編.pdf
上海交通大學保研夏令營信息匯總表.xls
上海交通大學預推免信息匯總表.xls
上海交通大學保研生源分析表.xls
上海交通大學本科生保研去向分析表.xls
各重點院校保研夏令營信息匯總表（報名截止時間）.zip
各重點院校推免生條件及要求匯總表.zip

上海交通大學

添加上海交通大學學姐微信，或微信搜索公眾號“保研喵”，關注【保研喵】微信公眾號，在保研喵公眾號輸入【上海交通大學保研夏令營條件、上海交通大學保研加分細則、上海交通大學保研群、上海交通大學保研學姐微信、上海交通大學保研真題、上海交通大學夏令營】即可在手機上查看相對應上海交通大學保研信息和免費資源。
回復【夏令營信息】【保研去向】【保研來源】【入營名單】即可查看蕞新蕞全的保研數據。
上海交通大學保研


本文來源：http://www.btfokj.cn/shanghaijiaotongdaxue/byxly_960508.html

推薦閱讀