橡实MCP
一种模型上下文协议（MCP）服务器，用于通过直观的web界面管理数学定理和定义。
布局
acorn_mcp/：用于MCP服务器、API服务器、数据库访问和语法检查器的Python包static/：由API服务器提供服务的前端资产docs/：橡实背景和简明语法参考tests/：简单的数据库烟雾测试acornlib/：已签出Acorn标准库（未被此服务器修改）
特性
- 定理数据库：使用名称、语句和证明存储和管理定理
- 定义数据库：存储和管理数学定义
- MCP服务器：为法学硕士提供与知识库互动的工具
- web界面：美观、响应迅速的用户界面，用于查看和添加定理和定义
- RESTful API：FastAPI驱动的后端，用于前端后端通信
建筑
该项目由三个主要部分组成：
- 数据库层 (
acorn_mcp/database.py)：SQLite数据库，对定理和定义进行异步操作 - MCP服务器 (
acorn_mcp/mcp_server.py)：LLM可用于访问知识库的模型上下文协议服务器 - API服务器 (
acorn_mcp/api_server.py)：FastAPI后端为web界面提供REST端点 - 前端 (
static/index.html)：用于查看和管理内容的交互式web界面
安装
- 克隆存储库：
git clone https://github.com/AIxMath/Acorn-MCP.git
cd Acorn-MCP- 安装依赖项：
pip install -r requirements.txt用法
运行Web界面
启动FastAPI服务器：
python -m acorn_mcp.api_server然后打开浏览器 http://localhost:8000 访问web界面。
运行MCP服务器
MCP服务器允许LLM与定理和定义数据库交互：
python -m acorn_mcp.mcp_serverMCP服务器通过stdio通信，可以与支持模型上下文协议的LLM客户端集成。
将Acorn标准库导入数据库
全部解析 .ac 文件在 acornlib/src 并插入发现的定理/定义：
python -m scripts.import_acornlib添加 --dry-run 不用写字就能看计数。
端到端设置（详细）
- 安装依赖项（可选地在virtualenv中）：
python -m venv .venv
source .venv/bin/activate
pip install -r requirements.txt- （可选）从捆绑的数据库中预填充数据库
acornlib结账：
python -m scripts.import_acornlib --dry-run # inspect counts
python -m scripts.import_acornlib # write to acorn_mcp.db- 启动web/API服务器（在
/JSON在/api/*):
python -m acorn_mcp.api_server访问 http://localhost:8000 添加/列出定理和定义。
- 如果要集成MCP，请在另一个终端中启动MCP服务器（stdio）：
python -m acorn_mcp.mcp_serverMCP服务器向客户端公开下面的工具列表。
运行MCP服务器
MCP服务器允许LLM与定理和定义数据库交互：
python -m acorn_mcp.mcp_serverMCP服务器通过stdio通信，可以与支持模型上下文协议的LLM客户端集成。
将Acorn标准库导入数据库
全部解析 .ac 文件在 acornlib/src 并插入发现的定理/定义：
python -m scripts.import_acornlib添加 --dry-run 不用写字就能看计数。
可用的MCP工具
MCP服务器为LLM提供以下工具：
add_theorem：添加一个新定理（需要：name、theorem_head、证明、raw）get_theorem：按名称检索定理list_theorems：列出所有定理add_definition：添加新定义（要求：名称、定义）get_definition：按名称检索定义list_definitions：列出所有定义get_acorn_syntax：返回压缩的Acorn语法引用check_acorn_syntax：验证Acorn代码片段并报告问题
进口商覆盖范围
这 scripts/import_acornlib.py 解析器导入：
- 定理：
theorem块（语句+可选by证明）和axiom块（被视为没有证明的定理）。 - 定义：
define,inductive,structure，以及typeclass块（与其标头和正文一起存储）。归纳类型被视为定义。
API终点
FastAPI服务器提供以下端点：
定理：
GET /api/theorems：列出所有定理（通过分页page/page_size，过滤器q)GET /api/theorems/{name}：得到一个特定的定理POST /api/theorems：创建新定理
定义：
GET /api/definitions：列出所有定义（通过分页page/page_size，过滤器q)GET /api/definitions/{name}：获取具体定义POST /api/definitions：创建新定义
数据库模式
定理表
id：自动递增主键name：唯一定理名称theorem_head：定理的陈述proof：定理的证明created_at：创建时间戳
定义表
id：自动递增主键name：唯一定义名称definition：定义文本created_at：创建时间戳
示例用法
通过API添加一个定理
curl -X POST http://localhost:8000/api/theorems \
-H "Content-Type: application/json" \
-d '{
"name": "Pythagorean Theorem",
"theorem_head": "In a right triangle, the square of the hypotenuse equals the sum of squares of the other two sides",
"proof": "Let a and b be the legs and c be the hypotenuse. Then a² + b² = c²"
}'通过API添加定义
curl -X POST http://localhost:8000/api/definitions \
-H "Content-Type: application/json" \
-d '{
"name": "Prime Number",
"definition": "A natural number greater than 1 that has no positive divisors other than 1 and itself"
}'发展
该项目使用：
- Python 3.7+
- 快速API：用于构建API的现代web框架
- MCP（模型上下文协议）：用于LLM集成
- aiosqlite：异步SQLite数据库操作
- Uvicorn：ASGI服务器
许可证
有关详细信息，请参阅LICENSE文件。