Jacobian's documentation follows the Diátaxis framework, organized by what the reader is trying to do. Start with a tutorial when learning the system, use a how-to guide for a specific task, consult reference material for exact contracts, and read the explanations for design rationale.
Jacobian exposes composable mathematical capabilities through an MCP server, CLI, and Python library. Capabilities have mathematically atomic, agent-visible outcomes; agents compose them into research strategies. Optional workflows preserve intermediate artifacts, and only operator-authorized independent checkers may promote exact evidence to a verified result. The product model defines the capability contract and ownership boundaries.
The current 0.6 architecture is pre-stable. Current reference documents and the installed catalog define the supported capabilities and interfaces. Evaluations guide portfolio behavior and maintenance; they do not grant verification authority.
These documents track the current product contract and its ongoing evolution:
| Question | Document | Status |
|---|---|---|
| What product is Jacobian building? | Product model | Active product direction |
| What does the system currently look like? | Architecture | Current implementation and trust boundaries |
| What direction is the project taking? | Product goals | Rolling goals pursued in parallel |
| What is installed now? | Tool surface and runtime capability://catalog |
Current interface rules and installation-specific inventory |
Tutorials are guided learning paths. They assume no prior Jacobian experience and build toward a complete result.
- Find and verify a counterexample shows the boundary between an unverified evaluator result and independently verified evidence.
- Retrieve a Lean theorem and check a proof composes computed declaration retrieval with independent Lean replay.
How-to guides assume you already understand Jacobian's basic model and need to complete a specific task.
- Discover, invoke, and verify domain capabilities
- Configure an agent from a source checkout
- Install optional backends
- Troubleshoot Z3 installation on macOS
- Run the Codex visibility evaluation
- Deploy the remote MCP server
- Author a Harbor benchmark task
- Migrate the benchmark portfolio
- Run agent evaluations
Reference documents define exact interfaces, records, gates, and test expectations.
Cross-cutting references:
- Tool surface — MCP resources, tools, and invocation contracts
- Domain operation library — built-in producer, bounded-search, artifact, and exact-replay contracts
- Native Python API — supported native-value modules
- Provider runtime — backend availability, compatibility, and identity
- Plugin conformance — plugin contract and conformance gates
- Persistent state format — supported migration floor and fresh-store transition
- Testing strategy — validation layers, commands, and CI responsibilities
Domain-owned references: Capability references grouped by owning domain (graphs, matrix, polynomial, Lean, SAT/SMT, finite math, number theory, linear algebra, topology, geometry). Adding an operation or provider does not require editing a central list; each domain owns its own subdirectory.
Evaluation references: Benchmark contracts and evaluation methods — Harbor task contracts, dataset inventory, validation gates, workflow observation, performance measurement, and regression policy.
Reference scenarios: Worked cases — mathematical scenario catalog and certified-homology case.
Use the runtime capability://catalog and math.find for the
installed capability inventory and exact operation schemas.
Explanation documents describe why Jacobian has its current boundaries and how its major parts fit together.
Read CONTRIBUTING.md before changing code or public documentation. The atomic capability portfolio records the formal-first backend research, ordering, installation tradeoffs, and evaluation gates used to decide which mathematical slices to build next.
Harbor benchmark authoring and verifier work is encoded in the repository-local
harbor-benchmarks skill. Use
the exact task gate for routine benchmark changes; control/treatment model runs
are explicit operator-run evidence exercises. For hosted operation, follow
Deploy the remote MCP server; ignored tmp/
records are evidence from one host, not maintained instructions.
When adding a document, place it according to the reader's need:
tutorials/for a guided learning experience;how-to/for completing one task;reference/for contracts and lookup material;explanation/for design context and decisions; andcontributing/for maintainer-facing research and planning records.
Do not mix active direction with supported behavior. Product goals guide priorities; only an applicable specification or conformance document defines a release contract.