What is Axiomatic Prover?

Axiomatic Prover is an AI-powered server designed for the Lean 4 ecosystem, enabling users to build, prove, and formalize mathematical theorems and code using Mathlib.

How does Axiomatic Prover assist in formalizing mathematics?

It helps by generating structured formalization plans from mathematical text and converting plan items directly into compilable Lean 4 code, streamlining the formalization workflow.

Does Axiomatic Prover offer automated theorem proving?

Yes, it leverages AI to automatically prove Lean 4 theorems that contain the 'sorry' placeholder, completing proofs efficiently.

How do I connect to Axiomatic Prover?

You integrate it as an MCP server within your MCP client (like Claude Desktop) by adding its URL. Authentication uses OAuth 2.1 via GitHub, handled automatically by your client.

Axiomatic Prover

Name: Axiomatic Prover
Author: Axiomatic-AI

byAxiomatic-AI

Developer Tools

Data Science & ML

Learning & Documentation

Facilitates building, proving, and formalizing mathematical theorems and code within the Lean 4 ecosystem using Mathlib.

About

The Axiomatic Prover acts as a powerful Lean 4 MCP server, enabling users to compile Lean 4 source code within a Mathlib-enabled sandbox and leverage AI-powered services for advanced tasks. It provides tools for automatically proving theorems that contain 'sorry', generating structured formalization plans from mathematical text, and converting these plans into compilable Lean 4 code. All compute-intensive operations are handled asynchronously via external cloud services, allowing users to submit jobs and poll for their completion status.