AtpMcp MCP server
Provides an MCP server that bridges automated theorem provers to agents. It exposes four backends: SystemOnTPTP, StarExec, Isabelle, and LocalExec, allowing agents to perform automated reasoning tasks using tools like E prover or Isabelle/HOL.
Package and access
Local package with source-attributed installation metadata. Koskamo does not execute packages during review.
What you can do with it
- Query automated theorem provers via SystemOnTPTP
- Run local theorem proving with E prover
- Execute proofs using Isabelle/HOL backend
- Submit problems to StarExec for distributed solving
Source and maintenance
- Last repository push
- Latest release
- v0.8.1
- Maintenance checked
Packages and installation
Source-provided package data. Koskamo has not executed or live-probed this package.
ghcr.io/jcschuster/atp_mcp:0.8.1
{
"transport": "stdio",
"identifier": "ghcr.io/jcschuster/atp_mcp:0.8.1",
"registryType": "oci"
}Tools
Reported by the attributed source; not independently observed by Koskamo.
Maintenance history
Public check and source-refresh events. Editorial and ownership records remain private.
- · repository · passed · metadata changed · updated
- · backfill · recorded · Pre-expansion baseline; unobserved rich metadata remains unknown
Connect from your client
Each snippet configures the same source-provided package; replace placeholders before use.
Cursor
{
"mcpServers": {
"atpmcp": {
"command": "docker",
"args": [
"run",
"-i",
"--rm",
"ghcr.io/jcschuster/atp_mcp:0.8.1"
]
}
}
}Cline
{
"mcpServers": {
"atpmcp": {
"command": "docker",
"args": [
"run",
"-i",
"--rm",
"ghcr.io/jcschuster/atp_mcp:0.8.1"
]
}
}
}VS Code
{
"servers": {
"atpmcp": {
"type": "stdio",
"command": "docker",
"args": [
"run",
"-i",
"--rm",
"ghcr.io/jcschuster/atp_mcp:0.8.1"
]
}
}
}Claude Desktop
{
"mcpServers": {
"atpmcp": {
"command": "docker",
"args": [
"run",
"-i",
"--rm",
"ghcr.io/jcschuster/atp_mcp:0.8.1"
]
}
}
}Let your agent find its tools
Find servers like AtpMcp from your agent. Add Koskamo once to search the index for endpoints, access requirements, and client setup. Public discovery needs no key.