Skip to content

ROADMAP.md

Latest commit

 

History

History
126 lines (114 loc) · 6.99 KB

ROADMAP.md

File metadata and controls

126 lines (114 loc) · 6.99 KB
Raw

Roadmap

Now

  • M1 agentic/alchemical alignment layer: first-class AlchemicalTrace, lightweight AgentProfile / AgentExperience / AgentBiography, H-tilt-lite advisory taste scoring, and in-memory roadmap alignment checks.
  • M2 Projection Engine: lawbook entries can create known skips, chain-safe derived certificate results, advisory residual splits, projection traces, and compounding metrics without treating projection pressure as truth.
  • M3 Root-Aware Constructors: advisory roots, residual basins, obstruction pressure, and projection pressure compile into narrow constructor plans and safe attempts while candidate tables remain non-terminal until importer verification.
  • M4 TRUE-side proof verification scaffold: proof motifs, lemma/cut candidates, theorem schemas, and Lean skeletons enter a replayable verifier/importer/ chain-audit lifecycle without treating sketches as truth.
  • M4.5 Unified Verification Episode Orchestrator: projection, root-aware constructors, TRUE-side proof verification, alchemical traces, agent experiences, and alignment checks compose into one replayable episode.
  • M5-prep Route Telemetry Ledger: unified episodes emit advisory route, outcome, transition, kill, cost, and gain telemetry for future spectral H-tilt without treating route scores as truth.
  • M5 Lightweight Spectral H-Tilt Estimator: route telemetry now yields advisory estimates of L, V, K = L - V, h, q, pi*, and mu_beta for scheduling pressure without verifier authority.
  • M6 Domain-General Claim IR / Formal World Registry: raw claims can be parsed, normalized, classified by formal world, and routed into existing episode or proof scaffolds while parsing remains advisory.
  • M6.5 Lean Adapter Hardening: Lean files/skeletons can be represented, checked when Lean is available, imported with verified provenance, and bridged into proof/alchemy/agent traces without treating Lean text as truth.
  • M6.6 Continuation Action Registry: advisory continuation actions can produce candidate claims, proof tasks, countermodel tasks, projection tasks, episode inputs, and obstruction candidates without treating generated moves as truth.
  • M6.7 Proof Digestion / Assimilation Layer: verified and unverified proof artifacts can be dependency-mapped, step-classified, compressed into key idea/schema candidates, exposition notes, projection hints, and lawbook assimilation candidates without treating digestion as verification.
  • M6.8 Verifier Feedback / Repair Loop: verifier failures are classified into minor repairable flaws, structural gaps, critical invalidations, or unknowns and converted into advisory repair, reroute, obstruction, or residual tasks.
  • v16.12 metabolic cycle testbed for one executable local frontier -> lawbook -> verifier -> derived closure -> residual -> next-frontier loop.
  • v16.11 LogiKEy-style meta-logical workbench and faithfulness layer.
  • v16.11 proof motif atlas and lemma candidate substrate for TRUE-side proof shaping.
  • v16.10 typed predication kernel and theory objectification substrate.
  • v16.9 DomainKernel registry, including AOT/Isabelle metadata registration.
  • v16.8 persistent LawbookStore / Artifact Warehouse for external v16.6.2 and v16.7 artifacts.
  • Keep trust/provenance separate from terminal truth.
  • Keep encoding distinct from exemplification.
  • Keep denotation/free-logic and artifact-risk guardrails explicit.
  • Store object-language IR, theory declarations, proof-method metadata, and advisory AOT scanner output without treating them as verification.
  • Track L0/L1/L2/L3 formal-world layers, embedding strategies, faithfulness assessments, backend profiles, benchmark metadata, correspondence claims, and interpretation choice points.
  • Store proof motifs, lemma candidates, and Lean artifact metadata without treating sketches as verification.
  • Measure residual compression, derived amplification, route yields, and better-shaped unknowns in a synthetic SAIR/ETP-like episode.
  • Preserve derived-false replay semantics: logical rows are not finite certificates until table/witness replay succeeds.
  • Maintain root, reason, and obstruction schemas for v16.7 artifacts.
  • Consolidate root aliases into canonical root families.
  • Keep all generated artifacts outside Git.

Next

  • Connect the metabolic cycle runner to larger imported certificate rows and constructor backends.
  • Root-aware oracle advice backed by typed predication and lawbook metadata.
  • Real faithfulness links from imported proof artifacts to semantic embeddings.
  • Workbench-driven constructor/verifier routing that still leaves truth to verifiers.
  • Full Lean project integration for generated lemma/cut candidates.
  • Real Isabelle session importer for AOT metadata and proof dependencies.
  • Richer domain adapters beyond conservative magma, Lean-skeleton, and advisory-only parsing.
  • Richer action policies, learned discovery value, and action ranking over the continuation registry.
  • Lawbook hardening for accepting proof digestion links separately from truth certificates.
  • Continuation curriculum and discovery value evaluator over repair outcomes.
  • Host/object theorem transport validation for scanned/imported AOT artifacts.
  • Constructor pressure from the Obstruction Atlas.
  • Larger canonical root consolidation over full external v16.7 artifacts.
  • Reason compression and root/reason/obstruction query UX.
  • Lean proof constructors behind the verifier boundary.

Later

  • Richer spectral H-tilt math beyond the lightweight pure-Python estimator.
  • Full Lean/Isabelle integration remains future work beyond the M4 scaffold.
  • M5 full spectral H-tilt remains future work beyond H-tilt-lite route pressure.
  • M6 follow-on domain-general claim expansion remains future work beyond the lightweight IR and registry.
  • M7: Existential Agent Ecology as an optional higher layer above the verification kernel.
  • Domain-agnostic GeneralClaim expansion beyond SAIR magma equations.
  • LOGOS middleware API for model proposal / MathGraph verification.
  • Real Isabelle session importer, AOT theorem/dependency extraction, and cross-domain root/reason atlas.

M7: Existential Agent Ecology

This is future roadmap only, not live implementation. The kernel is immortal and audit-stable. Agents may become mortal and biography-bearing. Truth remains verifier-bound. Discovery may become biography-bound.

Future concepts include irreversible mortality policy, agent wounds, self-forged values, narrative identity, HeldInChora / strategic non-verification, resource economy, and lineage / inheritance rules.

Hard guardrail: no agent wound, value, narrative, reputation, mortality status, lineage, or scar may promote a claim across the verifier boundary.

MathGraph should not become a self. It should become the world in which selves can risk themselves without corrupting truth.

Final death matters because agent death turns search into commitment. Without irreversible loss, agents have memory but not biography, cost but not sacrifice, preference but not value, exploration but not courage.