ChatDB - Autonomous Proof Engine

Architecture

Three-Substrate Stack

Rust orchestrates the hot path. Python validates with CAS and Lean 4. React observes. SQLite is the single source of truth.

FrontendReact + TypeScript

57 components · Zustand stores · Tauri event listeners · DAG visualization, obligation lanes, proof tree, token streaming · Observes. Never mutates.

BackendRust + Tauri 2

Loop engine with solver, critic, auditor, reviewer · Multi-model orchestrator (Anthropic, OpenAI, OpenRouter) · Obligation queue with satisfaction tally · Worker pool with parallel fan-in

SidecarPython + FastAPI

SymPy algebraic validator · Pint dimensional validator · Lean 4 persistent REPL with Mathlib · Multi-agent council, scout, librarian, adversary · MCP server for Claude Desktop

DatabaseSQLite + WAL

17 tables · Event-sourced DAG · Obligation lifecycle (open → assigned → closed/demoted) · Full training data provenance · The database is the memory.

// The core loop: solve → validate → record → audit → repeat
while step_number < max_steps {
    let obligation = obligation_queue.select_next(&attempt_id);
    let proposal  = solver.call(&prompt, &obligation).await;
    let result    = sidecar.validate_step(&proposal).await;

    if result.verified {
        db.record_step(&step);           // steps table
        db.create_node(&proof_node);     // DAG dual-write
        satisfaction_tally(&obligation);   // 4-voter quorum
    }

    if all_obligations_closed && budget_gate >= 3 {
        force_conclude();                 // anti-redundancy gate
    }
}
  

Core Innovation

Separation of Storage from Attention

The DAG persists everything. Agents are stateless functions. The orchestration layer decides what each agent sees. Context is curated, not accumulated.

💾

Database Is Memory

Every step, decision, and verdict recorded in SQLite. No ephemeral in-memory state. Full audit trail from problem to proof to training data.

👁

Curated Context

Each agent call receives only the relevant slice of the DAG. No context window bloat. Fresh perspective on every branch.

⚖

Obligation-Driven Search

Proof can't conclude until all obligations close. Four-voter satisfaction tally (mechanical, solver, reviewer, adversary) with quorum gating.

🛡

Three-Level Verification

Syntactic checks → CAS validation (SymPy/Pint) → Lean 4 kernel verification. Effort matches obligation criticality.

🤖

Multi-Model Orchestra

Solver, reviewer, adversary on independent models. Council deliberation after failed attempts. Orchestrator routes by capability.

📊

Budget-Aware

Token accounting per attempt. Anti-redundancy budget gate forces conclusion after all obligations satisfied. Plateau detector triggers branching.

Design Philosophy

The Four Irreducibilities

Proven impossibility theorems that shape every architectural decision. You can't engineer around physics — but you can build systems that respect the bounds.

Obligation Opacity

Complete obligations can't be enumerated before exploration (Cut-elimination blowup, Rice's theorem)

Response: Three-layer obligation parsing. Obligations mutable at every DAG node. Completeness invariant gates termination.

Solver Opacity

Verification of outputs doesn't predict process (77% of reasoning tokens are causally decorative)

Response: Never trust process; verify only outputs. Separate solver from verifier. Stateless agent calls.

V-E Tradeoff

Verification depth and exploration breadth trade off on concave Pareto frontier

Response: Make allocation visible and auditable. Syntactic → CAS → Lean formalization, chosen per obligation.

Strategy Interference

Pursuing one proof path forecloses alternatives (switching cost regret bounds)

Response: Fresh context for new branches. Plateau detector triggers mode transition. Technique taxonomy prevents tunnel vision.

Output

Seven Training Data Layers

Every agent produces mechanically verified, structured training data. Not just the proof — the entire search trajectory, deliberation, and meta-reasoning.

Layer	Source	Signal	What Makes It Unique
1	Solvers	Step-level PRM (goal → proposal → verdict)	Verified in real-time by CAS + Lean
2	Solvers	Full attempt trees with backtracks	Complete search trajectories, not just solutions
3	Orchestrator	Routing decisions, worker states	Multi-agent coordination traces
4	Council	Deliberation, consensus, dissent	Metacognitive reasoning about reasoning
5	Scout	Research gap → query → result → impact	When-to-research decision signal
6	Critic	Prediction vs actual outcome	Evaluation calibration data
7	Librarian	Curation decisions, downstream impact	Knowledge management traces

Roadmap

From First Proof to Full Pipeline

Milestone 1 — Complete

First Verified Proof

Linear step chain with CAS validation, event streaming, dual-write to proof nodes. 19 steps, 44.7K tokens, 100% mechanical validation.

Milestone 2 — Complete

Pattern Extraction

Technique library from solved proofs. Success/failure tracking per pattern. Injection into solver prompts.

Sprint 1 — In Progress

Obligation Parsing Pipeline

Three-layer obligation detection. Pre-solve intelligence briefing. Merge pipeline with dedup and confidence scoring. Anti-redundancy budget gate. Technique family taxonomy.

Sprint 2

Obligation Engine + Completeness Invariant

Obligations drive the loop. Completeness invariant gates termination. Full DAG branching.

Sprint 3

Multi-Model + Adversary + Librarian

Parallel agent orchestra. Escalation ladder. Pattern curation and coverage monitoring.

Sprint 4

Registry Learning + Safety

Self-modification tracking. Death spiral detection. Technique taxonomy with success rate learning.

Sprint 5

API + Formalization + Polish

HTTP API for external consumers. Full Lean 4 formalization pipeline. MCP server for Claude integration.

Stack

Built With

Rust + Tauri 2

Backend orchestration, async loop engine, SQLite bindings, LLM client with streaming + thinking support.

React + TypeScript

Zustand state management, Tauri IPC event listeners, DAG visualization, proof tree rendering.

Python + FastAPI

SymPy and Pint validators, multi-agent sidecar, MCP server, Lean REPL management.

Lean 4 + Mathlib

Persistent REPL with warm Mathlib environment. Kernel verification in <1s after warmup. Claim-type-aware tactic dispatch.

SQLite + WAL

17-table schema. Event-sourced DAG. Full training data provenance. Schema-as-architecture philosophy.

Multi-LLM Support

Anthropic (with thinking), OpenAI (with reasoning), OpenRouter. Independent solver, reviewer, and adversary models.

ChatDB Autonomous Proof Engine