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.
ai-toolsclaudeformal-verificationlean4mathmcp-serverretrievaltheorem-search
安装
$
claude mcp add mathlas -- uvx mathlas-mcp