jacobian

<p align="center"> <img src="docs/assets/jacobian-hero.jpg" width="100%" alt="一位数学家在黑板前工作的存档风格黑白照片，具有恒定的雅可比行列式和三个映射到一个输出的不同输入。"> </p> <h1 align="center">雅可比</h1> <p align="center"> <strong>面向智能体的可执行数学。独立检查者可以复现的证据。</strong> </p> <p align="center"> 一个MCP服务器、命令行界面和Python库，用于猜想、反例、精确计算和形式化证明。 </p> <p align="center"> <a href="https://github.com/morluto/jacobian/actions/workflows/ci.yml"><img src="https://github.com/morluto/jacobian/actions/workflows/ci.yml/badge.svg" alt="持续集成"></a> <a href="https://pypi.org/project/jacobian/"><img src="https://img.shields.io/pypi/v/jacobian" alt="PyPI"></a> <a href="https://www.npmjs.com/package/jacobian"><img src="https://img.shields.io/npm/v/jacobian" alt="npm"></a> <a href="https://pypi.org/project/jacobian/"><img src="https://img.shields.io/pypi/pyversions/jacobian" alt="支持的Python版本"></a> <a href="LICENSE"><img src="https://img.shields.io/github/license/morluto/jacobian" alt="MIT许可证"></a> </p> <p align="center"> <a href="#快速入门">快速入门</a> · <a href="#验证机制">验证机制</a> · <a href="#功能">功能</a> · <a href="#文档">文档</a> · <a href="#贡献">贡献</a> </p> 雅可比为智能体提供小型、可组合的数学运算，而不是一个不透明的求解器。智能体可以构建对象、计算不变量、搜索见证并向独立检查者提交精确证据。每个步骤都作为类型化结果或工件可见。 信任边界是刻意的：搜索结果、求解器状态、模型答案、超时或分数从不直接提升到`已验证`。只有操作员授权的检查者才能发出绑定到精确声明、候选者、范围、语义、证书格式和检查者身份的已验证记录。 ## 快速入门 npm启动器安装雅可比并配置支持的MCP客户端： ```sh npm install -g jacobian jacobian setup jacobian doctor ``` 启动器支持Claude、Codex、Cursor、Gemini和OpenCode。它需要Node.js 18或更新版本、Python 3.12和[`uv`](https://docs.astral.sh/uv/)。运行`jacobian mcp`可以直接启动服务器。 <details> <summary><strong>从源代码安装</strong></summary> ```sh git clone https://github.com/morluto/jacobian.git cd jacobian uv sync --dev uv run jacobian --state-dir .jacobian init ``` 使用`uv run jacobian --help`检查命令行界面，或使用`uv run jacobian-mcp`启动MCP适配器。 </details> ## 验证机制 雅可比将寻找证据与确定证据证明的内容分开。假设智能体正在测试声明 **“`F` 是单射的。”** <p align="center"> <img src="docs/assets/verification-flow.jpg" width="100%" alt="声明F是单射的导致候选碰撞、精确独立检查和验证记录。缺少见证、超时、取消和错误仍然未知。"> </p> **声明 → 候选见证 → 独立检查 → 验证记录** | 阶段 | 输出 | 确立内容 | | --- | --- | --- | | 声明 | `F` 是单射的 | 调查声明；尚未信任 | | 搜索 | 候选见证 `(F, p, q)` | 可检查的证据，而不是结论 | | 独立检查 | 确认 `p ≠ q` 和 `F(p) − F(q) = 0` 精确 | 候选者是真正的碰撞 | | 记录 | 绑定检查的碰撞到原始声明和检查者身份 | 单射声明是 `FALSE · VERIFIED` | > **没有见证不是证明。** 搜索失败、超时、取消或错误使声明保持`UNKNOWN`。 在介绍性教程中，相同的边界出现为： ```text evaluate.batch → FALSE · HEURISTIC witness.find → 精确见证工件 witness.verify → FALSE · VERIFIED ``` `FALSE · HEURISTIC` 是评估。`FALSE · VERIFIED` 是由独立检查的证据支持的结论。参见[查找和验证反例](docs/tutorials/first-verified-result.md)获取可运行的示例。 ## 功能 功能在运行时通过 `capability://catalog` 发现，通过 `capability.describe` 描述，并通过 `capability.invoke` 执行。已安装的目录是事实来源，因为可用性取决于本地后端。 | 领域 | 智能体可见的结果 | | --- | --- | | 多项式映射 | 评估映射、计算雅可比、搜索碰撞、独立验证碰撞 | | 多项式代数 | 归一化类型表达式、分解单变量多项式、验证恒等式、验证精确系统解 | | 精确线性代数 | 计算行列式、秩、核和整数行赫尔米特范式；查找和验证 `Ax = b` 的有理解 | | 图 | 构造和检查图、枚举路径、实现度序列、测试同构、搜索着色 | | SAT 和 SMT | 查找模型或证明工件；独立重放赋值、DRAT证明和Alethe证明 | | 泛代数 | 评估有限 magma 律并搜索反模型 | | 多面体 | 计算凸组合和线性分离 | | Lean | 发现声明、检索前提、检查证明状态并在固定环境中检查证明 | | 研究内存 | 存储修订后的草稿工作、发现、尝试、焦点和依赖链接上下文 | 参见[工具参考](docs/reference/tools.md)获取公共接口和[原子能力投资组合](docs/contributing/atomic-capability-portfolio.md)获取投资组合设计和评估门槛。 ## 设计 雅可比保持四个职责分离： - **智能体拥有策略。** 内核提供数学运算，而不是预先规定的研究工作流程。 - **能力暴露一个连贯的结果。** 有用的中间对象、失败和证明义务保持可见。 - **工件携带上下文。** 结果报告执行状态、来源、范围、完整性、精确度和可用证书。 - **检查者拥有信任。** 插件和搜索代码不能授权检查者或更改验证策略。 公共MCP表面保持较小：能力目录加上`capability.describe`、`capability.invoke`和三个直接工作区工具。`workspace.open`、`workspace.write`和`workspace.query`管理持久的智能体作者状态；工作区条目保持`UNVERIFIED`。 ## 文档 | 开始这里 | 当你需要详细信息 | | --- | --- | | [文档首页](docs/index.md) | 教程、操作指南、参考和解释 | | [架构](docs/explanation/architecture.md) | 系统形状和独立验证边界 | | [产品模型](docs/explanation/product-blueprint.md) | 能力合同、所有权、工件和保证 | | [产品目标](docs/explanation/goals.md) | 活动优先级和研究方向 | | [工具表面](docs/reference/tools.md) | MCP资源、工具和调用合同 | | [提供者运行时](docs/reference/provider-runtime.md) | 后端可用性、兼容性和身份 | | [v0.2 规范](docs/reference/specifications/v0.2.md) | 支持的发布行为和一致性 | | [测试策略](docs/reference/testing-strategy.md) | 验证层、命令和CI职责 | 专业合同涵盖[SAT工件](docs/reference/sat-artifacts.md)、[SMT/Alethe工件](docs/reference/smt-artifacts.md)、[精确有理解](docs/reference/linear-rational-solutions.md)、[整数矩阵HNF](docs/reference/matrix-hermite-normal-form.md)和[Lean声明发现](docs/reference/lean-declaration-discovery.md)。架构决策记录在[ADR索引](docs/explanation/adr/index.md)中。 ## MCP客户端和部署 `jacobian setup` 将本地服务器注册到一个或多个支持的客户端。服务器宣传能力入口点和直接工作区工具；具有MCP资源支持的客户端还可以读取`capability://catalog`。 远程客户端可以通过Streamable HTTP或SSE与带有持有者令牌身份验证和主题绑定租户状态的SSE连接。参见[部署远程MCP服务器](docs/how-to/deploy-remote-mcp.md)。静态令牌用于受控部署，而不是作为托管身份系统。 ## 可选后端 一些功能使用默认情况下未安装的后端： - CaDiCaL 查找SAT模型和不满足证明工件。 - cvc5 生成SMT不满足证明；Carcara独立检查Alethe。 - `flint` 额外功能加速精确有理线性代数和整数行赫尔米特范式。 - 固定的Lean `CORE` 和 `MATHLIB` 环境检查正式证书。 后端可用性不是验证权限。提供者输出在适当的独立检查者接受其绑定见证或证书之前保持未验证状态。 <details> <summary><strong>Lean证书</strong></summary> `lean.check` 能力将精确的命题和证明体绑定到其结果。捆绑环境固定Lean、导入和允许的信任基；模型提供的导入和包被拒绝。 使用以下命令准备固定的运行时： ```sh elan toolchain install leanprover/lean4:v4.31.0 cd lean lake update lake build ``` 证明状态交互和前提检索是探索辅助工具。它们的输出在没有成功的`lean.check`的情况下不能成为`VERIFIED`。参见[引导式声明发现教程](docs/tutorials/lean-declaration-discovery.md)。 </details> <details> <summary><strong>macOS 和 Z3</strong></summary> 锁定环境使用`z3-solver` 4.16.0.0。其上游macOS轮子针对Apple硅和Intel上的macOS 15或更新版本。对于较旧的版本，`uv` 退回到需要CMake、`make`和C++20编译器的源代码构建。 在重试`uv sync --dev`之前安装Xcode命令行工具和CMake。这些命令在不更改环境的情况下报告相关环境： ```sh sw_vers -productVersion uname -m xcode-select -p clang++ --version cmake --version make --version ``` 参见PyPI上的[`z3-solver` 4.16.0.0文件](https://pypi.org/project/z3-solver/4.16.0.0/#files)获取上游轮标签。 </details> ## 状态 雅可比处于预稳定状态。实验性合同可能在版本之间更改；版本规格描述了支持的快照，而不是正在进行的能力研究的顺序。 Python发行版包含数学内核、命令行界面和MCP服务器。npm包是一个薄的启动器和MCP客户端安装程序，用于相同的实现；它不是一个单独的JavaScript API。 <details> <summary><strong>关于英雄图像</strong></summary> 视觉主题来自雅可比猜想的三个维度的反例：一个精确的常数雅可比行列式与三个具有相同输出的不同有理输入。这些方程是不寻常的雅可比目的的简写——令人惊讶的候选者很有价值，但精确的计算和独立的检查确定了什么可以信任。 Terence Tao 提供了一个[易懂的数学解释](https://terrytao.wordpress.com/2026/07/21/a-digestion-of-the-jacobian-conjecture-counterexample/)。行列式恒等式和碰撞也在Isabelle/HOL中[被独立形式化](https://isa-afp.org/entries/Jacobian_Counterexample.html)。二维猜想仍然是开放的。 </details> <details> <summary><strong>项目边界</strong></summary> 雅可比不旨在将通用数学本体、自然语言到形式数学的转换器、分布式搜索基础设施或不透明的通用求解器放入内核。它不重新实现定理证明器或SAT/MIP求解器，不接受任意模型提供的可执行包，不将浮点分数、超时和求解器标签视为证明。 </details> ## 贡献 雅可比使用Python 3.12、`uv`和一个小的`Makefile`： ```sh make setup make test-fast make check ``` 在更改代码之前阅读[CONTRIBUTING.md](CONTRIBUTING.md)。它记录了聚焦的测试命令、验证规则、文档位置和拉取请求期望。 ## 许可证 [MIT](LICENSE)