Skip to content

roadmap.md

Latest commit

 

History

History
107 lines (99 loc) · 3.73 KB

roadmap.md

File metadata and controls

107 lines (99 loc) · 3.73 KB
Raw

Roadmap

  • Mathlib Module Verification v0.2 project execution hardening: implemented/in progress.

Current Architecture

Existential Agent Ecology
  -> API / SDK / CLI
  -> Domain Claim
  -> Semantic / Natural-Language Intake
  -> Formal-World Adapter Registry
  -> Adapter Capability / Parse / Normalize / Validate
  -> Proof-System Project Registry
  -> Artifact Manifests / Import Graphs / Check Requests
  -> Continuation Actions
  -> Continuation Curriculum
  -> Verification Episode
  -> Verifier / Importer / Finite Validator / Chain Audit
  -> Proof Digestion
  -> Verifier Feedback / Repair
  -> Discovery Value
  -> Lawbook Acceptance
  -> Lawbook Query / Known Skip
  -> Structural Identity
  -> Habit Rules
  -> Reason Compression
  -> Process Memory
  -> Structure Registry / Typed Projection
  -> Role-Based Object Introduction
  -> Structural Analogy / Exposition
  -> Projection
  -> Telemetry

Implemented / In Progress

  1. M0 Closed-Loop Certificate Smoke
  2. M1 Agentic Alchemical Loop
  3. M2 Projection Engine
  4. M3 Root-Aware Constructors
  5. M4 TRUE-Side Proof Verification
  6. M4.5 Unified Verification Episode
  7. M5 Route Telemetry and Spectral H-Tilt
  8. M6 Domain-General Claim IR
  9. M6.5 Lean Adapter Hardening
  10. M6.6 Continuation Actions
  11. M6.7 Proof Digestion
  12. M6.8 Verifier Feedback / Repair
  13. M6.8.1 Verifier Feedback Boundary Hardening
  14. M6.9 Continuation Curriculum
  15. M6.9.1 Curriculum Hardening
  16. M6.10 Discovery Value
  17. M6.11 Lawbook Acceptance Boundary
  18. M6.11.1 Public Surface / Terminology Hardening
  19. M6.12 Lawbook Query / Known Skip
  20. M6.13 Structural Identity
  21. M6.14 Habit Rules
  22. M6.15 Reason Compression
  23. M6.16 Process Memory
  24. M6.17 Structure Registry / Typed Projection
  25. M6.18 Role-Based Object Introduction
  26. M6.19 Structural Analogy / Exposition
  27. M6.20 Documentation / Spec Synchronization and Publication Refresh
  28. M7 Richer Formal-World Adapters
  29. M8 Deeper Proof-System Integration
  30. M9 Semantic and Natural-Language Claim Handling with Strict Boundaries
  31. M10 API Service Hardening
  32. M11 Existential Agent Ecology
  33. Post-M11 Hardening and Evaluation
  34. External Verifier Execution Adapter and Full End-to-End Test Drive
  35. Richer Verifier Adapter + Real Fixture Expansion
  36. Verified Corpus Micro-Ingestion
  37. Lean Project Micro-Subset Pilot
  38. CLI Import-Path Hardening + Colab Test Drive Script
  39. Mathlib Micro-Subset Pilot
  40. Real Local Mathlib Allowlist Pilot
  41. Mathlib Local Declaration Discovery + Allowlist Manifest Builder
  42. Curated Proof-Library Demo Pack + Optional Real Mathlib Allowlist Example
  43. Public Demo Notebook + Release Readiness + Optional Real Mathlib Revision Demo
  44. v0.1 Release Candidate Hardening
  45. Curated Real Mathlib Manifest v0 Demo
  46. Real Mathlib Module-Aware Verification v0
  47. Mathlib Module Verification v0.2 project execution hardening
  48. M12 Persistent Mathlib Digest Lawbook

Future Work

  • real curated Mathlib allowlist examples
  • richer Lean parser / AST-backed extraction
  • full Lean proof-term dependency extraction
  • robust declaration-level dependency graph
  • real induction constructor synthesis
  • real leRecOn/order-recursion constructor synthesis
  • dependency extraction through Lean tooling
  • trusted importer policy for pinned external corpora
  • richer Lake-aware diagnostics without network or package-manager actions
  • API service endpoints over persistent Lawbook
  • model-trained route/constructor ranking
  • persistent Lawbook browser UI
  • larger fixture-driven release gates
  • persistent Lawbook storage workflow
  • package/release workflow

Only verifier, trusted importer, finite validator, and chain audit boundaries promote truth. Every other layer is advisory unless it reports already accepted boundary evidence.