Skip to content

README.md

Latest commit

 

History

History
189 lines (147 loc) · 8.75 KB

README.md

File metadata and controls

189 lines (147 loc) · 8.75 KB

Lean-Agentic Documentation

Complete documentation for the Lean-Agentic formally verified agentic programming language with state-of-the-art theorem proving capabilities.

📚 Documentation Structure

🎯 Quick Start

🧮 Theorems (theorems/)

Novel Contributions:

Church-Rosser Confluence:

Planning & Research:

🗃️ AgentDB (agentdb/)

Reinforcement learning database with vector embeddings and memory systems:

📖 Implementation Guides (guides/)

Step-by-step implementation documentation:

📊 Status Reports (reports/)

Implementation progress and summaries:

✅ Validation & Verification (validation/)

Formal verification and proof attestations:

🏗️ Architecture Details

Core Architecture:

Decisions:

Diagrams:

🎯 Navigation Guide

For Users

Start here:

  1. Project README - Overview and installation
  2. guides/PRODUCTION_EXAMPLES.md - Example usage
  3. guides/RUNBOOK.md - Operations guide

For Contributors

Start here:

  1. ARCHITECTURE.md - High-level architecture
  2. architecture/ - Detailed design docs
  3. reports/SWARM_IMPLEMENTATION_COMPLETE.md - Implementation details

For Researchers

Start here:

  1. theorems/NEW_THEOREM_ACHIEVEMENT.md - Latest theorem contribution
  2. theorems/FORMAL_PROOF_HASHCONS_CONFLUENCE.md - Rigorous proof
  3. architecture/02-proof-kernel.md - Formal verification kernel
  4. theorems/THEOREM_ROADMAP.md - Future research directions

🏆 Notable Achievements

Novel Theorem (October 2025)

Hash-Consing Confluence Preservation Theorem

  • First formalization connecting hash-consing with confluence properties
  • Rigorous proof with 8 academic citations
  • 705.6x measured speedup (exceeds theoretical 100x!)
  • Complete Rust implementation with 100% test success
  • See theorems/NEW_THEOREM_ACHIEVEMENT.md

AgentDB v1.6.0

📊 Documentation Statistics

  • Total Files: 34 organized documentation files
  • Theorems: 10 files (including novel contributions)
  • AgentDB: 5 validation documents
  • Guides: 5 implementation guides
  • Reports: 12 status reports
  • Validation: 2 verification documents
  • Architecture: 9 detailed architecture files
  • Total Size: ~350KB of comprehensive documentation

🔧 Building Documentation

# Generate API documentation
cargo doc --workspace --no-deps --open

# View architecture locally
mdcat docs/ARCHITECTURE.md

# Generate PDF (requires pandoc)
pandoc docs/ARCHITECTURE.md -o architecture.pdf

# View theorem proofs
mdcat docs/theorems/FORMAL_PROOF_HASHCONS_CONFLUENCE.md

📝 Documentation Conventions

  • All code examples are tested and working
  • Performance numbers are from actual measurements
  • Architecture diagrams follow C4 model
  • ADRs document major design decisions with rationale
  • Theorems include rigorous proofs and empirical validation
  • All documentation is kept up-to-date with code

🤝 Contributing to Documentation

When adding documentation:

  1. Follow the existing structure (use appropriate subdirectories)
  2. Add entries to this README
  3. Use Markdown with GitHub-flavored syntax
  4. Include code examples that compile
  5. Measure and verify performance claims
  6. Update diagrams if architecture changes
  7. For theorems: include formal proofs and citations

Directory Guidelines

  • theorems/ - Theorem statements, proofs, and implementations
  • agentdb/ - AgentDB validation and version reports
  • guides/ - User-facing implementation guides
  • reports/ - Status reports and implementation summaries
  • validation/ - Formal verification and proof attestations
  • Root - Core architecture and high-level overview docs

🔗 Publishing

See PUBLISHING.md for npm publishing guidelines.

Last Updated: 2025-10-25 Documentation Version: 2.0.0 Notable: Hash-Consing Confluence Preservation Theorem (World's First)