com.axiomatic-ai/prover
AI 与智能体by axiomatic-ai
Lean 4 MCP server：可编译代码、证明定理，并借助 Mathlib 完成数学形式化工作。
什么是 com.axiomatic-ai/prover？
Lean 4 MCP server：可编译代码、证明定理，并借助 Mathlib 完成数学形式化工作。
README
Axiomatic Prover — MCP Server
Lean 4 MCP server: compile and prove theorems with Mathlib.
Connect
Add to your MCP client (e.g. Claude Desktop claude_desktop_config.json):
{
"mcpServers": {
"ax-prover": {
"type": "streamable-http",
"url": "https://prover.axiomatic-ai.com/mcp/"
}
}
}
Authentication uses OAuth 2.1 via GitHub — your MCP client handles the flow automatically.
Tools
Submit (async — returns a job_id)
| Tool | Description |
|---|---|
lean4_build | Compile Lean 4 source code in a Mathlib-enabled sandbox. Code is sent to external cloud services for compilation; if proving, also for AI processing. |
lean4_prove_theorems | Automatically prove Lean 4 theorems that contain sorry. Code is sent to external cloud services for compilation and AI proving. |
Poll
| Tool | Description |
|---|---|
lean4_get_job_status | Poll for the status and result of any ax-prover job. |
All submit tools are asynchronous — they return a job_id immediately.
Poll with lean4_get_job_status(job_id) until status is completed or failed.
Links
常见问题
com.axiomatic-ai/prover 是什么？
Lean 4 MCP server：可编译代码、证明定理，并借助 Mathlib 完成数学形式化工作。
相关 Skills
Claude接口
by anthropics
面向接入 Claude API、Anthropic SDK 或 Agent SDK 的开发场景，自动识别项目语言并给出对应示例与默认配置，快速搭建 LLM 应用。
✎ 想把Claude能力接进应用或智能体，用claude-api上手快、兼容Anthropic与Agent SDK，集成路径清晰又省心
智能体流程设计
by alirezarezvani
面向生产级多 Agent 编排，梳理顺序、并行、分层、事件驱动、共识五种工作流设计，覆盖 handoff、状态管理、容错重试、上下文预算与成本优化，适合搭建复杂 AI 协作系统。
✎ 帮你把多智能体流程设计、编排和自动化统一起来，复杂工作流也能更稳地落地，适合追求强控制力的团队。
提示工程专家
by alirezarezvani
覆盖Prompt优化、Few-shot设计、结构化输出、RAG评测与Agent工作流编排，适合分析token成本、评估LLM输出质量，并搭建可落地的AI智能体系统。
✎ 把提示优化、LLM评测到RAG与智能体设计串成一套方法，适合想系统提升AI开发效率的人。
相关 MCP Server
知识图谱记忆
编辑精选by Anthropic
Memory 是一个基于本地知识图谱的持久化记忆系统，让 AI 记住长期上下文。
✎ 帮 AI 和智能体补上“记不住”的短板，用本地知识图谱沉淀长期上下文，连续对话更聪明，数据也更可控。
顺序思维
编辑精选by Anthropic
Sequential Thinking 是让 AI 通过动态思维链解决复杂问题的参考服务器。
✎ 这个服务器展示了如何让 Claude 像人类一样逐步推理，适合开发者学习 MCP 的思维链实现。但注意它只是个参考示例，别指望直接用在生产环境里。
PraisonAI
编辑精选by mervinpraison
PraisonAI 是一个支持自反思和多 LLM 的低代码 AI 智能体框架。
✎ 如果你需要快速搭建一个能 24/7 运行的 AI 智能体团队来处理复杂任务（比如自动研究或代码生成），PraisonAI 的低代码设计和多平台集成（如 Telegram）让它上手极快。但作为非官方项目，它的生态成熟度可能不如 LangChain 等主流框架，适合愿意尝鲜的开发者。