English Français العربية

com.axiomatic-ai/prover

السجل الرسمي أخرى

Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.

الشيفرة المصدرية التوثيق

التثبيت

أضف هذا إلى إعدادات MCP في عميلك (Claude Desktop: claude_desktop_config.json، وCursor: ‏.cursor/mcp.json، ويستخدم VS Code وغيره الصيغة نفسها «mcpServers»).

Remote (streamable-http)
Claude Code 
claude mcp add --transport http prover 'https://prover.axiomatic-ai.com/mcp/'
إعداد JSON (Claude Desktop وCursor وVS Code) 
{
    "mcpServers": {
        "prover": {
            "type": "http",
            "url": "https://prover.axiomatic-ai.com/mcp/"
        }
    }
}

التوثيق

مأخوذ من ملف README للمشروع على GitHub ويُحدَّث أسبوعيًا. تفتح الروابط على GitHub.

المحتويات
  1. Axiomatic Prover — MCP Server
  2. Connect
  3. Tools
  4. Links

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)
ToolDescription
lean4_buildCompile 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_theoremsAutomatically prove Lean 4 theorems that contain sorry. Code is sent to external cloud services for compilation and AI proving.
Poll
ToolDescription
lean4_get_job_statusPoll 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.

الأسئلة الشائعة

ما هو com.axiomatic-ai/prover؟

Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.

كيف أثبّت com.axiomatic-ai/prover؟

يعمل كخادم بعيد. في Claude Code: claude mcp add --transport http prover 'https://prover.axiomatic-ai.com/mcp/'. وفي العملاء الآخرين، الصق إعداد JSON من هذه الصفحة في إعدادات MCP الخاصة بهم.

هل يحتاج com.axiomatic-ai/prover إلى مفتاح API؟

لا يذكر إدراجه في السجل أي مفتاح أو سر إلزامي. قد تتطلب بعض الميزات حسابًا لدى الخدمة التي يتصل بها.

هل com.axiomatic-ai/prover مفتوح المصدر؟

شيفرته علنية على GitHub، لكن المستودع لا يعلن ترخيصًا قياسيًا.

من يصون com.axiomatic-ai/prover؟

ينشره Axiomatic-AI. يدرجه AI.tn لكنه لا يصونه ولا يوصي به.

من سجل MCP الرسمي. الإدراج ليس توصية: راجع شيفرة الخادم وصلاحياته قبل منحه الوصول إلى بياناتك.