F4: functional thursday 社群活動 ▶︎主題：用 LLM 生成形式證明經驗談

連結

• https://www.facebook.com/groups/functioanl.thursday/posts/4447561422225517

共筆上的原文

8/13 週四晚上 F4: functional thursday 社群活動 ▶︎主題：用 LLM 生成形式證明經驗談
- 近年來 AI/LLM 發展迅速，不僅能生成文字和圖片，還能穩定生成程式碼。幾個月前，GPT 5.4 和 Claude Opus 4.6 等前沿模型開始能生成相對複雜的形式化數學證明，甚至複雜如編譯器中介表示轉換的正確性，只需提供類似的證明「範本」即可生成相近敘述的形式證明。
- 本次分享將探討使用 GPT 5 系列與 Agda 撰寫依值型別程式和形式定理證明的經驗，並說明語言模型如何透過定理證明器的保證，生成正確性近乎無懈可擊的數學證明。
- ▶︎分享者：陳亮廷
    - 在中央研究院擔任助理研究員，喜歡嘗試各種新事物。最近的興趣是型別論、範疇模型，還有具備計算意義的證明。
- https://www.facebook.com/groups/functioanl.thursday/posts/4447561422225517