mathlas
本地Airtight math tools an AI uses over MCP — 3.7M-theorem search, PSLQ constant ID, OEIS, real Lean kernel checks, applicability checklists. No LLM inside, no API key.
安装配置
{
"mcpServers": {
"mathlas": {
"command": "npx",
"args": [
"mathlas-mcp"
]
}
}
}