深度分析 利用 Model Context Protocol 的多代理 LAMP 框架，在 Lean 4 中首次形式化詞組合學 大型語言模型在數學推理上進步，但 Lean 4 受限於 Mathlib 領域。LAMP 框架利用 MCP 即時接入詞組合學 (CoW) 本體知識，透過 Planner、Builder、Verifier 產生核查過的證明。實驗顯示在 90 項 CoW 定理測試中，LAMP 驗證率 96.7%，遠超未加工具基線與現有專門化證明器。
