深度分析 在 Isabelle/HOL 中最小化型別註記：Smolka–Blanchette 演算法與 LLM 代理人實作 背景：型別註記影響術語可重解析性與型別推斷。方法：在Isabelle上形式化rank-one多型λ演算之最小完整註記問題，分析Smolka-Blanchette反向貪婪刪除與覆蓋測試。結果：人類與LLM各自草擬證明，LLM再自動形式化並在人工提示下推廣，產生三套Isabelle形式化成果，示範AI輔助程式語言型態理論的可行性。
