Specifications¶
Design specifications for the erdos-banger CLI toolkit.
Version Roadmap¶
v1.0 (DONE) Foundation: CLI, data loading, search, Lean integration
v1.1 (DONE) Literature: Ingest + RAG Q&A
v1.2 (DONE) Iteration: Loop + logging + OpenAlex metadata
v1.3 (DONE) Enhancement: Vectors + batch ops
v1.4 (DONE) Integration: Formal conjectures + MCP
v2.0 (DONE) Expansion: PDF conversion (Marker + LLM)
v2.1 (DONE) Architecture: MetadataProvider abstraction
v3.0 (DONE) Research: Workspace + campaign memory
v3.1 (DONE) Verification: v3 integration tests
v3.2 (DONE) Data sync + Research APIs: Unified sync + Exa integration
v3.3 (DONE) Research APIs: Semantic Scholar integration
v3.4 (DONE) Research APIs: zbMATH integration
v3.5 (DONE) Architecture: Multi-model routing
v4.0 (DONE) Lean: Lean Copilot integration
v4.1 (DONE) UX: Progress dashboard
v4.2 (PLANNED) Integration: Lead enrichment pipeline (discovery → manifest)
v4.3 (PLANNED) Exploration: Math CLI (SymPy/NetworkX computational tools)
Active Specs¶
| ID | Title | Status | Target | Description |
|---|---|---|---|---|
| 036 | Lead Enrichment Pipeline | Draft | v4.2 | Bridges discovery (Exa/zbMATH/S2) and enrichment (OpenAlex) |
| 037 | Math Exploration CLI | Draft | v4.3 | SymPy/NetworkX CLI for computational exploration |
Design Documents¶
Research-backed design decisions for complex specs.
| ID | Title | Status | Prerequisite For |
|---|---|---|---|
| RSM-001 | v3 Research State | Implemented | SPEC-023 → SPEC-027 |
Deferred Specs¶
Specs designed for future versions.
| ID | Title | Status | Target | Description |
|---|---|---|---|---|
| (none) |
Archived Specs¶
Completed specs that are fully implemented.
| ID | Title | Location |
|---|---|---|
| 001 | Dev Environment & Tooling | archive |
| 002 | Testing Strategy | archive |
| 003 | Domain Models | archive |
| 004 | CLI Architecture | archive |
| 005 | Problem Loader | archive |
| 006 | Search Index | archive |
| 007 | Lean Integration | archive |
| 008 | Test Fixtures | archive |
| 009 | Architecture Cleanup | archive |
| 010 | Ingest Command | archive |
| 011 | Ask Command | archive |
| 018 | DevX Makefile | archive |
| 013 | Logging & Evaluation | archive |
| 020 | OpenAlex Integration | archive |
| 021 | Aristotle Integration | archive |
| 012 | Loop Command | archive |
| 012-DESIGN | Loop Command Design | archive |
| 016 | Formal Conjectures | archive |
| 014 | Vector Embeddings | archive |
| 015 | Batch Operations | archive |
| 017 | MCP Server | archive |
| 019 | PDF Conversion | archive |
| 022 | MetadataProvider Orchestration | archive |
| 023 | Research Workspace (Filesystem SSOT) | archive |
| 024 | Research Records (Leads/Attempts/Hypotheses/Tasks) | archive |
| 025 | Index Research Artifacts into Search DB | archive |
| 026 | Deterministic Research Synthesis | archive |
| 027 | Loop → Research Integration | archive |
| 028 | v3 Integration Verification | archive |
| 029 | Exa Research Integration | archive |
| 030 | Semantic Scholar Integration | archive |
| 031 | zbMATH Integration | archive |
| 032 | Multi-Model Routing | archive |
| 033 | Lean Copilot Integration | archive |
| 034 | Progress Dashboard | archive |
| 035 | Unified Problem Data Sync | archive |
Next Spec ID: SPEC-038
Dependency Graph¶
v1.0 Foundation (DONE)
├── 001 Dev Environment
├── 002 Testing Strategy
├── 003 Domain Models
├── 004 CLI Architecture
├── 005 Problem Loader
├── 006 Search Index
├── 007 Lean Integration
├── 008 Test Fixtures
└── 009 Architecture Cleanup
v1.1 Literature (DONE)
├── 010 Ingest Command ────────────┐
└── 011 Ask Command ←──────────────┘ (uses the local search index; ingested extracts become usable once indexed)
v1.2 Iteration & Metadata (DONE)
├── 012-DESIGN Loop Design ←── research (approved SSOT)
├── 012 Loop Command ←── 012-DESIGN + 011 Ask + 007 Lean
├── 013 Logging ←── all commands (tracks progress)
└── 020 OpenAlex Integration ←── augments 010 Ingest
v1.2+ Optional Proving Backend (DONE)
└── 021 Aristotle Integration ←── 007 Lean
v1.3 Enhancement (DONE)
├── 014 Vector Embeddings ←── 006 Search Index (DONE)
└── 015 Batch Operations ←── 010 Ingest + 007 Lean (DONE)
v1.4 Integration (DONE)
├── 016 Formal Conjectures ←── 007 Lean (DONE)
└── 017 MCP Server ←── all CLI commands (DONE)
v2.0 Expansion (DONE)
└── 019 PDF Conversion ←── 010 Ingest (Marker + LLM enhancement)
v2.1 Architecture (DONE)
└── 022 MetadataProvider Orchestration ←── Resolves DEBT-038, enables pluggable sources
v3.0 Research (DONE)
├── 023 Research Workspace ←── Filesystem SSOT for campaign memory
├── 024 Research Records ←── Leads/Attempts/Hypotheses/Tasks CRUD
├── 025 Index Research Artifacts ←── RAG integration
├── 026 Deterministic Synthesis ←── SYNTHESIS.md rendering
└── 027 Loop → Research ←── Attempt records from loop
v3.1 Verification (DONE)
└── 028 v3 Integration Verification ←── Horizontal + vertical tests
v3.2 Data Sync + Research APIs (DONE)
├── 035 Unified Problem Data Sync ←── 028 (verified v3 foundation)
└── 029 Exa Research Integration ←── Agentic literature synthesis
v3.3 Citation Context (DONE)
└── 030 Semantic Scholar Integration ←── Citation context
v3.4 Math Metadata (DONE)
└── 031 zbMATH Integration ←── Math-specific metadata
v3.5 Architecture (DONE)
└── 032 Multi-Model Routing ←── Task-level LLM routing (external commands)
v4.0 Lean Enhancement (DONE)
└── 033 Lean Copilot Integration ←── 032 (needs model routing)
v4.1 UX (DONE)
└── 034 Progress Dashboard ←── 028 (verified v3 foundation)
v4.2 Integration (PLANNED)
└── 036 Lead Enrichment Pipeline ←── 022 (FallbackProvider) + 024 (Leads) + 029 (Exa)
v4.3 Exploration (PLANNED)
└── 037 Math Exploration CLI ←── Issue #32 (SymPy/NetworkX extras)
Master Documents¶
- Master Vision - Full design & build plan
- Master Qualifications - Project scope & requirements
Spec Lifecycle¶
- Draft - Initial design, open for discussion
- Pending - Approved, awaiting implementation
- Ready - Fully specified and implementable, scheduled for a later version
- Deferred - Intentionally postponed (may require more design work)
- Active - Implementation in progress
- Complete - Fully implemented and tested
- Archived - Completed, locked in
- Blocked - Cannot proceed due to external dependency
Writing a New Spec¶
Each spec must be:
- Self-contained - Clear scope, explicit dependencies
- Vertical slice - Testable end-to-end
- Independently verifiable - Tests don't require unimplemented specs
Template sections: - Scope (in/out) - CLI - Output Schema (JSON) - Implementation (modules to create/modify) - Verification (testable claims) - References - Changelog