{"id":"5209a611-a691-4513-b3f8-20416575dc14","slug":"chronokairo-axiom","kind":"mcp","name":"AXIOM","summary":"AXIOM — Mathematical Reasoning Engine: One MCP for mathematical computation, exploration, and independent verification.","owner":"chronokairo","repoUrl":"https://github.com/chronokairo/AXIOM","license":"MIT","licenseTier":"permissive","trust":"community","stars":0,"match":null,"fewStars":true,"format":"mcp","createdAt":"2026-01-29T19:15:15.000Z","addedAt":"2026-10-26T11:34:30.064Z","logoUrl":"https://avatars.githubusercontent.com/u/208986040?v=4","linkOnly":false,"collection":null,"skillPath":null,"categories":["utilities"],"tags":["education","latex","lean4","mathematics","offline-first","open-source","sympy","ai-agents"],"runtime":"python","local":true,"cloudCapable":false,"cloudCapability":"unknown","cloudReadyOnPlatform":false,"needsApiKey":false,"reviewed":false,"syncedAt":"2026-10-26T11:34:30.040Z","sample":false,"url":"https://conduits.dev/tools/chronokairo-axiom","language":"Python","transports":["stdio"],"install":{"pypi":"axiom-math"},"requirements":{"env":[],"upstreamMayCharge":false},"tools":null,"readme":"# AXIOM\n\n**Mathematical Reasoning Engine**\n\n*One MCP for mathematical investigation, computation, and verification.*\n\n**[Research Math for All Time by Chronokairo](https://chronokairo.com)**\n\n**English** · [简体中文](docs/readme/README_zh.md) · [繁體中文](docs/readme/README_zh-TW.md) · [日本語](docs/readme/README_ja.md) · [한국어](docs/readme/README_ko.md) · [Türkçe](docs/readme/README_tr.md) · [Русский](docs/readme/README_ru.md) · [Tiếng Việt](docs/readme/README_vi.md) · [ไทย](docs/readme/README_th.md) · [Deutsch](docs/readme/README_de.md) · [Español](docs/readme/README_es.md) · [Français](docs/readme/README_fr.md) · [Português (Brasil)](docs/readme/README_pt-BR.md) · [العربية](docs/readme/README_ar.md) · [فارسی](docs/readme/README_fa.md) · [Italiano](docs/readme/README_it.md) · [Ελληνικά](docs/readme/README_el.md)\n\nAXIOM is a computational mathematics infrastructure for AI agents, researchers, students, and developers. It connects any Model Context Protocol (MCP) client to specialized mathematics engines — **SymPy**, **mpmath / SciPy**, **SageMath**, **Julia**, and **Lean 4 / Mathlib 4** — through a unified contract, where every result carries structured evidence and is **independently verified**.\n\nIt is not an AI-powered calculator. It is not another Mathematica, SageMath, or Lean. It is the neuro-symbolic infrastructure that lets reasoning agents interact with all of them through a single verified interface.\n\n> Inspired by the philosophy of [REA](https://github.com/morluto/rea): *reverse engineer anything* → **investigate mathematics with agents**.\n\n---\n\n## Why AXIOM\n\nWhen an AI agent claims it solved an equation, standard tools take its word for it. AXIOM **requires independent mathematical verification** before a claim is accepted.\n\n```bash\naxiom solve \"x^2 - 5*x + 6 = 0\"\n```\n\n```text\n┌─ AXIOM · solve ───────────────────────────────────────────────────────────────────────┐\n│ Solve            x^2 - 5*x + 6 = 0                                                    │\n│ Result           ['2', '3']                                                           │\n│ LaTeX            2, 3                                                                 │\n│ Engine           sympy 1.14.0                                                         │\n│ Method           algebraic solve (sympy.solve + domain & solveset completeness audit) │\n│ Verification     exact-substitution: PASSED                                           │\n│ Detail           Both roots satisfy the equation by exact substitution                │\n│ Epistemic State  PROOF                                                                │\n│ Guarantee        [VERIFIED] VERIFIED-SUBSTITUTION                                     │\n└───────────────────────────────────────────────────────────────────────────────────────┘\n```\n\n---\n\n## The Four Epistemic States\n\nAXIOM strictly categorizes all mathematical reasoning and computational output into **four mutually exclusive epistemic states** ([ADR-0017](docs/adr/0017-four-epistemic-states-and-soundness-governance.md)):\n\n| Epistemic State | Underlying Guarantees | Epistemic Definition | Fail-Closed Verification Criteria |\n| :--- | :--- | :--- | :--- |\n| **Proof** | `formal-proof`, `exact-symbolic`, `verified-substitution` | Certified mathematical truth. An exact symbolic identity, machine-checked Lean 4 kernel derivation (`#print axioms`), or verified equation roots. | `Verification.passed == True`, exact symbolic residual $0$, no unverified axioms/hypotheses, congruent spec alignment. |\n| **Approximation** | `numerical-approximation` | Quantitative evaluation or bounded sequence probing within specified tolerance $\\epsilon$. Inexact float absorption is rejected. | Finite error $\\le \\epsilon$, `equivalent == False`, `approximately_equal == True`. Never granted `EXACT_SYMBOLIC`. |\n| **Refutation** | `[REFUTED] DISPROVEN` | The proposition is decisively proven false via a concrete counterexample ($f(x^*) \\neq 0$), contradiction, or non-zero residual. | Independent verification disproves the claim. `Verification.passed == False`, witness recorded in `detail`. |\n| **Inconclusive** | `[UNVERIFIED] UNVERIFIED` | Truth value cannot be established within available symbolic algorithms, branch bounds, or execution timeouts. | Fail-closed state. `guarantee == Guarantee.UNVERIFIED`. Never promoted to proof. |\n\n### Guarantee Hierarchy\n\nNot every computation carries the same logical strength. AXIOM separates **mathematical correctness claims** (`is_mathematical_claim == True`, requiring an executed `Verification(passed=True)`) from **operational states** (`is_mathematical_claim == False`):\n\n| Level | Category | Meaning |\n| :--- | :--- | :--- |\n| `formal-proof` | Mathematical Claim | Proof verified by the Lean 4 kernel (`#print axioms` confirmed, `sorry`/`admit` and trivial $X = X$ tautologies rejected) |\n| `exact-symbolic` | Mathematical Claim | Verified symbolic identity (canonical simplification, FTC antiderivative round-trip, symbolic L'Hôpital, with optional `assumptions`) |\n| `verified-substitution` | Mathematical Claim | Solution validated by independent substitution ($f(r)=0$, $A A^{-1}=I$, $\\nabla_\\lambda g_{\\mu\\nu}=0$) with pole & domain-error rejection |\n| `numerical-approximation` | Mathematical Claim | Arbitrary-precision evaluation, finite-difference check, adaptive quadrature, or two-sided sequence limit probe with declared `max_error` |\n| `structural-parse` | Operational State | Safe AST parse validated by canonical re-parse equivalence (`ast-roundtrip`) |\n| `catalog-lookup` | Operational State | Indexed declaration retrieved from the curated Mathlib 4 catalog or Loogle API |\n| `sampled-visualization` | Operational State | Sampled 1D curve coordinates rendered to vector SVG and ASCII preview |\n| `heuristic` | Operational State | Plausible pattern, exploratory summary, or open conjecture not yet verified |\n| `unverified` | Operational State | Refuted claim, interior pole / jump discontinuity failure, or inconclusive computation |\n\nEvery result carries structured `Evidence` metadata: `engine`, `engine_version`, `method`, `steps`, `limitations`, and `reproducible_with`.\n\n---\n\n## Architecture\n\n```text\n┌──────────────────────────────────────────────────────────┐\n│  AI Agents                                               │\n│  Antigravity · Codex · Claude Code · Cursor · Copilot    │\n└────────────────────────┬─────────────────────────────────┘\n                         │  MCP (29 tools) / CLI\n┌────────────────────────▼─────────────────────────────────┐\n│  AXIOM Core                                              │\n│  Safe AST Parser · Dispatcher · Engine Registry ·        │\n│  Evidence · Independent Verification · Research Sessions │\n└──┬──────────┬──────────┬──────────┬───────────────────────┘\n   │          │          │          │\n   ▼          ▼          ▼          ▼\n Symbolic   Numerical   Formal     Visualization\n SymPy      mpmath      Lean 4     Native Vector SVG\n SageMath   Julia       Mathlib4   ASCII Preview · Matplotlib\n```\n\n---\n\n## Quick Start\n\n```bash\n# Clone and install locally\ngit clone https://github.com/chronokairo/axiom.git\ncd axiom\npip install -e .\n\n# Run environment & verification diagnostics\naxiom doctor\n\n# Auto-configure Antigravity, Claude Code, Cursor, Gemini CLI, and Codex\naxiom setup --apply\n\n# Start the MCP stdio server\naxiom mcp\n```\n\n---\n\n## The Four Epistemic States in Action (CLI & MCP)\n\n### 1. Proof (Certified Mathematical Truth)\n\n```bash\naxiom solve \"x^2 - 5*x + 6 = 0\"\n```\n```text\n┌─ AXIOM · solve ───────────────────────────────────────────────────────────────────────┐\n│ Solve            x^2 - 5*x + 6 = 0                                                    │\n│ Result           ['2', '3']                                                           │\n│ LaTeX            2, 3                                                                 │\n│ Engine           sympy 1.14.0                                                         │\n│ Method           algebraic solve (sympy.solve + domain & solveset completeness audit) │\n│ Verification     exact-substitution: PASSED                                           │\n│ Detail           Both roots satisfy the equation by exact substitution                │\n│ Epistemic State  PROOF                                                                │\n│ Guarantee        [VERIFIED] VERIFIED-SUBSTITUTION                                     │\n└───────────────────────────────────────────────────────────────────────────────────────┘\n```\n\n### 2. Approximation (Bounded Numerical Evidence)\n\n```bash\naxiom compare \"pi\" \"3.141592653589793\" --tolerance 1e-12\n```\n```text\n┌─ AXIOM · compare ──────────────────────────────────────────────────────────────────────────────┐\n│ Compare          pi == 3.141592653589793                                                                       │\n│ Result           approximately equal within tolerance 1.0e-12 (max error: 2.33e-16, exact equality not proven) │\n│ LaTeX            \\pi \\approx 3.141592653589793                                                                 │\n│ Engine           sympy 1.14.0                                                                                  │\n│ Method           symbolic difference reduction + domain & multi-point sampling                                 │\n│ Verification     numerical-tolerance: PASSED                                                                   │\n│ Detail           numerical-tolerance: PASSED (error <= 1e-12)                                                  │\n│ Epistemic State  APPROXIMATION                                                                                 │\n│ Guarantee        [APPROXIMATE] NUMERICAL-APPROXIMATION                                                         │\n│ Invariant        equivalent=False, approximately_equal=True                                                    │\n└────────────────────────────────────────────────────────────────────────────────────────────────┘\n```\n\n### 3. Refutation (Active Counterexample Discovery)\n\n```bash\naxiom compare \"(x+1)*(x-2)*(x^2+1)*(x^2-2*x+2)\" \"0\"\n```\n```text\n┌─ AXIOM · compare ─────────────────────────────────────────────────────────────────────────────────────────────────┐\n│ Compare          (x+1)*(x-2)*(x^2+1)*(x^2-2*x+2) == 0                                                             │\n│ Result           not equivalent (counterexample: {'x': '-2'})                                                     │\n│ LaTeX            \\left(x - 2\\right) \\left(x + 1\\right) \\left(x^{2} + 1\\right) \\left(x^{2} - 2 x + 2\\right) \\neq 0 │\n│ Engine           sympy 1.14.0                                                                                     │\n│ Method           symbolic difference reduction + domain & multi-point sampling                                    │\n│ Verification     counterexample-search: FAILED                                                                    │\n│ Detail           counterexample found at {'x': '-2'} (|diff| = 2.000e+02)                                         │\n│ Epistemic State  REFUTATION                                                                                       │\n│ Guarantee        [REFUTED] DISPROVEN                                                                              │\n│ Invariant        equivalent=False, approximately_equal=False                                                      │\n└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘\n```\n\n### 4. Inconclusive (Fail-Closed Indecidability)\n\n```bash\naxiom integrate \"exp(-x^3)\" --variable x\n```\n```text\n┌─ AXIOM · integrate ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐\n│ Integrate        exp(-x^3)                                                                                                                     │\n│ Result           gamma(1/3)*lowergamma(1/3, x**3)/(9*gamma(4/3))                                                                               │\n│ LaTeX            \\frac{\\Gamma\\left(\\frac{1}{3}\\right) \\gamma\\left(\\frac{1}{3}, x^{3}\\right)}{9 \\Gamma\\left(\\frac{4}{3}\\right)}                 │\n│ Engine           sympy 1.14.0                                                                                                                  │\n│ Method           symbolic indefinite integration (sympy.integrate)                                                                             │\n│ Verification     differentiate-antiderivative: FAILED                                                                                          │\n│ Detail           d/dx(gamma(1/3)*lowergamma(1/3, x**3)/(9*gamma(4/3))) = x**2*exp(-x**3)*gamma(1/3)/(3*(x**3)**(2/3)*gamma(4/3)) != exp(-x**3) │\n│ Epistemic State  INCONCLUSIVE                                                                                                                  │\n│ Guarantee        [UNVERIFIED] UNVERIFIED                                                                                                       │\n└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘\n```\n\n---\n\n## 29 Composable MCP Tools\n\n| Category | Count | Tools |\n| :--- | :---: | :--- |\n| **1. Mathematical Computation** | 12 | `math_simplify`, `math_solve`, `math_differentiate`, `math_integrate`, `math_limit`, `math_evaluate`, `math_matrix`, `math_ode`, `math_number_theory`, `math_optimize`, `math_statistics`, `math_tensor` |\n| **2. Verification & Formal Proof** | 3 | `math_prove`, `math_verify`, `math_compare` |\n| **3. Structural & Diagnostic** | 3 | `math_parse`, `math_explain`, `math_explore` |\n| **4. Catalog Lookup** | 1 | `math_search_mathlib` |\n| **5. Visualization & Session** | 2 | `math_plot`, `math_session` |\n| **6. Mathematical Investigation Layer** | 8 | `math_investigate`, `math_analyze_claim`, `math_trace_dependencies`, `math_find_counterexample`, `math_compare_proofs`, `math_list_unknowns`, `math_get_evidence_bundle`, `math_export_investigation` |\n\n---\n\n## Mathematical Investigation Layer\n\nA CAS answers a question. An **investigation** pursues a claim: it formalises\nthe claim, decomposes it, tracks the lemmas it depends on, hunts for\ncounterexamples, compares proof routes, catalogues what remains unknown, and\nexports a reproducible dossier of evidence\n([ADR-0019](docs/adr/0019-mathematical-investigation-layer-rea-paradigm.md)).\n\n```bash\naxiom investigate \"(x^2 - 1)/(x - 1) = x + 1\"\naxiom analyze-claim inv-20261020-e6e353\naxiom trace-dependencies inv-20261020-e6e353 --lemma \"sin(x)^2 + cos(x)^2 = 1\"\naxiom find-counterexample inv-20261020-e6e353\naxiom list-unknowns inv-20261020-e6e353\naxiom get-evidence-bundle inv-20261020-e6e353\naxiom export-investigation inv-20261020-e6e353\n```\n\nEach dossier is a self-contained directory:\n\n```text\n.axiom/investigations/<id>/\n├── spec.json        # formalised statement and domain scope\n├── graph.json       # proof dependency graph (audited nodes and edges)\n├── unknowns.json    # Unknown Ledger: gaps, pending hypotheses, unproved lemmas\n├── evidence/        # per-step evidence artifacts\n├── bundle.json      # provenance package with SHA-256 digests\n└── REPORT.md        # reproducible dossier report (with a Mermaid graph)\n```\n\n> **Fail-closed by design.** An investigation orchestrates verified\n> computations but is never itself a proof: its results carry\n> `guarantee = heuristic` and `epistemic_state = inconclusive`, while every\n> individual claim inside the dossier keeps its own guarantee. A dependency\n> list certifies the *structure* of a derivation, never that a dependency\n> logically implies its dependant — only a kernel-checked proof does that.\n\n---\n\n## Scientific Research & Academic Foundation\n\nAXIOM operates as a rigorous neuro-symbolic research harness. For theoretical justifications, statistical bounds, literature positioning, and formal arithmetic proofs, see:\n\n- **[Scientific Research Whitepaper (`RESEARCH.md`)](RESEARCH.md)** — Core research document detailing:\n  - Epistemological taxonomy and proof theory foundations;\n  - Decidability bounds (Richardson's Theorem, Gödel Incompleteness, MRDP Theorem);\n  - **Benchmark EXP-0001 ($n=21$ targeted adversarial cases, 13 of them mathematically invalid)**: 0.0% False Positive Rate ($0/13$), 95% CI upper bound $\\approx 23.1\\%$ via Rule of Three (two-sided Clopper-Pearson: $[0.0\\%, 24.7\\%]$) vs 46.2% in the emulated naive CAS baseline;\n  - **Millennium Boundary Probes ($n=111$ criteria, 40 negative controls)**: 95% CI upper bound $\\le 8.8\\%$ (two-sided Clopper-Pearson);\n  - **Boundary Stress-Test Disclaimer**: Clarifies that AXIOM makes **no claim** of solving open Millennium Prize Problems (Poincaré is verified as solved by Perelman; Navier-Stokes validates known Taylor-Green analytical solutions while refusing to certify unproven regularity);\n  - **Versioned Arithmetic Corpus (`research/arithmetic/`)**: Machine-checked Lean 4 proofs (Bézout, Euclid's Lemma, Fundamental Theorem of Arithmetic Existence and Uniqueness, Euclid's Infinitude of Primes, Linear Diophantine Equations, and Modular Congruences) completing 100% of Abramo Hefez's foundational arithmetic curriculum.\n- **[Research Proposal (`proposal.md`)](proposal.md)** & **[Experimental Methodology (`methodology.md`)](methodology.md)**.\n- **[Curriculum Track (`curriculum.md`)](curriculum.md)** & **[Daily Research Log (`study-log.md`)](study-log.md)**.\n- **[Academic Citation (`CITATION.cff`)](CITATION.cff)**.\n\n---\n\n## Roadmap\n\n- [x] **v0.1.0 — Verified Foundation**: 21-tool MCP server, CLI, safe AST parser, fail-closed verifiers, Lean 4 `#print axioms` audit + Lake environment support, and 6/6 cross-platform CI matrix.\n- [x] **v0.1.1 — Verification Integrity**: Separation between `exact-symbolic` identities and `numerical-approximation` evidence, plus non-empty theorem confirmation in `#print axioms`.\n- [x] **v0.1.2 — Formal Integration**: Live Lean 4 + Lake formal verification in GitHub Actions CI (`formal-lean`).\n- [x] **v0.2.0 — Mathematical Coverage**: Operational states separation, domain `assumptions`, branch-cut counterexample generation, interior pole rejection, and Lean 4 tautology detection (`37` tests).\n- [x] **v0.2.1 — Domain Integrity**: Pre-evaluation AST denominator tracking ($\\frac{x-1}{x-1} \\neq 1$), complex Gaussian probes ($\\sqrt{x^2} \\neq |x|$ over $\\mathbb{C}$), and benchmark `EXP-0001` (`42` tests).\n- [x] **v0.2.2 — Adversarial Hardening**: Ternary equivalence semantics, adversarial polynomial refutation, relational assumption grammar, and system solvers (`45` tests).\n- [x] **v0.2.3 — Scientific Benchmark Integrity**: Taylor-Green analytical kinetic energy $E(t) = \\pi^2 e^{-4\\nu t}$, evidence isolation, and boundary stress probes across all 7 Clay Millennium problems (`49` tests).\n- [x] **v0.2.4 — Formal Specification Soundness**: Semantic alignment auditor, SymPy kernel validity gating, Navier-Stokes viscous dissipation $D(t) = 4\\nu\\pi^2 e^{-4\\nu t}$ derived from velocity gradients, and Lean 4 forced variant model (`51` tests).\n- [x] **v0.2.5 — Formal Statement Integrity**: Lean 4 binder and signature parsing, 4-state semantic alignment, and kinetic energy spatial integration derivation (`54` tests).\n- [x] **v0.2.6 — Four Epistemic States & Adversarial Soundness**: 4-epistemic-state separation, Lean sandbox with resource bounds, authorized path restriction, and zero-mock adversarial test suite ([ADR-0017](docs/adr/0017-four-epistemic-states-and-soundness-governance.md), `63` tests).\n- [x] **v0.2.7 — Evidence Integrity & Sandboxing**: Untrusted JSON session quarantine, sanitized process environment for Lean, and interface alignment ([ADR-0018](docs/adr/0018-evidence-integrity-sandboxing-and-interface-alignment.md), `73` tests).\n- [x] **v0.2.8 — CI Recovery, Tamper-Resistant Revalidation & Versioned Arithmetic Corpus**: Strict semantic value comparison for tamper detection across all operations, hypothesis downgrading on load, and the versioned Abramo Hefez Lean 4 arithmetic corpus in `research/arithmetic/` ([ADR-0026](docs/adr/0026-ci-recovery-tamper-detection-and-versioned-arithmetic-corpus.md)).\n- [x] **v0.2.9 — Exact Value Integrity, Refutation Evidence, Structured Witnesses & CI Full Pass**: 8/8 CI jobs fully green on all platforms; exact integer comparison in the tamper comparator (no float loss above $2^{53}$); `REFUTATION` strictly requires machine-readable structured witnesses with replay verification; mandatory value integrity gate in persisted evidence; positional assertions replaced by semantic identification; dual Lean 4.14/4.35 compatibility; consistent two-sided Clopper-Pearson bounds ([ADR-0031](docs/adr/0031-exact-value-integrity-refutation-evidence-and-statistical-corrections.md), [ADR-0032](docs/adr/0032-structured-falsity-witnesses-and-investigation-layer.md), `111` automated tests across 6 suites).\n- [x] **v0.3.0 — The Mathematical Investigation Layer (Porting REA to Mathematics)**: Mathematical Investigation Dossiers (`.axiom/investigations/<id>/`), Proof Dependency Graphs (DAG, with structural integrity kept separate from demonstrated logical implication), the **Unknown Ledger** (`math_list_unknowns`), Evidence Bundles with SHA-256 provenance hashes (`math_get_evidence_bundle`), the 8 high-level investigation primitives over MCP and CLI, and a reproducible dossier report with a Mermaid dependency graph ([ADR-0019](docs/adr/0019-mathematical-investigation-layer-rea-paradigm.md), [ADR-0032](docs/adr/0032-structured-falsity-witnesses-and-investigation-layer.md), `143` automated tests across 8 suites).\n\n---\n\n## Repository Layout\n\n```text\naxiom/\n├── README.md                  # Developer & user quickstart guide\n├── RESEARCH.md                # Academic research whitepaper, bounds & methodology\n├── TUTORIAL.md                # Comprehensive user tutorial & agent guide\n├── TODO.md                    # Gap audit & roadmap tracking\n├── LICENSE                    # MIT License\n├── CITATION.cff               # Academic citation metadata\n├── AGENTS.md                  # Multi-agent coordination & skills index\n├── curriculum.md              # Research study program & bibliography\n├── study-log.md               # Daily research log & Lean 4 cross-checks\n├── proposal.md                # Neuro-symbolic research proposal\n├── related-work.md            # Literature review & scientific comparison\n├── methodology.md             # Experimental methodology & invariants\n├── limitations.md             # Theoretical & implementation limitations\n├── pyproject.toml\n├── src/\n│   └── axiom/\n│       ├── core.py            # Mathematical core & dispatcher\n│       ├── contract.py        # MathResult, Evidence, Verification, EpistemicState, Guarantee\n│       ├── parsing.py         # Safe AST mathematical parser & relational assumptions\n│       ├── verification.py    # Independent verifiers & ternary equivalence\n│       ├── registry.py        # Multi-engine registry\n│       ├── mcp_server.py      # 29-tool MCP JSON-RPC 2.0 stdio server\n│       ├── cli.py             # CLI & Unicode evidence box renderer\n│       ├── session.py         # Reproducible research sessions\n│       ├── setup_agent.py     # Agent auto-config (setup) & diagnostics (doctor)\n│       └── engines/           # sympy, numeric (mpmath), lean, sagemath, julia\n├── experiments/\n│   └── exp-0001/              # Domain integrity & adversarial benchmark (n=21, results.json, REPORT.md)\n├── reports/                   # Boundary stress tests & epistemic sanity probes across Clay problems\n├── research/\n│   ├── arithmetic/            # Versioned, Git-tracked Lean 4 arithmetic corpus (Days 04-07)\n│   ├── conjectures/           # Working hypotheses & empirical claims\n│   ├── lemmas/                # Proven lemmas & Lean 4 kernel-checked proofs\n│   └── counterexamples/       # Systematically cataloged refutations\n├── benchmarks/\n│   ├── millennium/            # Consolidated Millennium Bench (111 criteria, 40 negative controls)\n│   └── run_benchmarks.py      # Execution time benchmarks\n├── skills/                    # Standardized GitHub Agent Skills\n├── examples/                  # Verified Lean 4 example proofs\n├── tests/\n│   ├── test_axiom.py          # 56 automated unit tests\n│   ├── test_adversarial.py    # 9 adversarial soundness & isolation tests\n│   ├── test_use_cases.py      # 10 end-to-end workflow tests\n│   ├── test_tamper_detection.py # 5 payload tamper detection & hypothesis integrity tests\n│   ├── test_skills.py         # 4 agent skill specification tests\n│   └── lean_project/          # Lake workspace for live Lean 4 formal CI tests\n└── docs/\n    ├── adr/                   # Architecture Decision Records (ADR-0001..0026)\n    ├── use-cases.md           # 10 end-to-end CLI & MCP workflows\n    ├── mcp-contracts.md       # JSON-RPC schemas & guarantee contracts\n    ├── analise-concorrencia-mcp-2026.md # Competitive landscape analysis\n    └── readme/                # 17 localized README translations\n```\n\n---\n\n## License\n\nMIT — **[Research Math for All Time by Chronokairo](https://chronokairo.com)**\n"}