cameronfreer/lean4-skills

解決的問題

提供一個結構化的工作流程，讓 AI 編碼代理能使用 Lean 4 語言執行形式化驗證與定理證明。它彌補了非形式化數學主張與已認證證明之間的差距，為代理提供系統化的方法來起草、證明、審查與優化 Lean 程式碼。

如何運作

本專案實作一組與主機無關的「技能」（工作流程），可整合至各種 AI 代理（如 Claude Code、Codex、Cursor 或 Gemini CLI）。這些工作流程遵循共享的證明循環：規劃 → 工作 → 檢查點 → 審查 → 重規劃 → 繼續/停止。

主要功能包括：

• 形式化：將非形式化主張轉換為 Lean 宣告的骨架。
• 證明：包含 mathlib 搜尋與策略嘗試的引導式或自主式定理證明循環。
• 驗證：公理檢查與安全防護機制，確保證明的完整性。
• 優化：對證明進行「高爾夫化」，以提升簡潔性、清晰度與效能。
• 整合：可選地與 Lean LSP MCP 配合使用，實時檢視目標並獲得更快的回饋。

適用對象

使用 AI 編碼代理撰寫形式化證明、驗證軟體，或在 Lean 4 生態系中探索數學的開發者與研究人員。

特色

• 主機無關：可在 Claude Code、Codex、Cursor 等多個代理平台中運作。
• 全面的工作流程：包含專用指令用於起草、自動證明、反證與重構。
• 認證反證：專用的 disprove 工作流程，用於搜尋反例。
• 穩健的工具鏈：包含主機無關的命令驗證解析器與 CI 保護的執行時測試。