A proof-driven approach to machine intelligence where every self-improvement must be formally verified.
An AI framework that combines:
- Go for the core engine (~90 source files)
- Lean 4 for mathematical proofs (~70 theorem files)
- LLM integration for candidate generation
The system only accepts changes to itself that come with machine-checkable proofs of correctness.
| Component | Purpose |
|---|---|
| E-graph Engine | Equality saturation for term optimization |
| CEGIS Synthesis | Counterexample-guided program synthesis |
| Rewrite Engine | Verified term transformations |
| Knowledge Graph | Compositional knowledge representation |
| Lean 4 Bridge | Exports to proof assistant for verification |
| Anti-hack Verification | Dual validation to prevent reward hacking |
internal/
├── egraph/ # E-graph equality saturation
├── synthesis/ # CEGIS loop implementation
├── rewrite/ # Term rewriting rules & engine
├── knowledge/ # Knowledge graph with query system
├── lean/ # Lean 4 code generation & runner
├── verify/ # Anti-hack dual validation
├── evolution/ # Genetic operators for improvement
├── category/ # Category theory abstractions (functors, transfer)
├── llm/ # LLM candidate generation
└── pipeline/ # Orchestration layer
validation/ # Lean 4 proofs (lake project)
# Run all tests
go test ./...
# Validate Lean proofs
cd validation && lake buildE-graph saturation with union-find for efficient equivalence class management.
CEGIS loop that iteratively refines candidates against counterexamples until a provably correct solution is found.
Category-theoretic transfer for moving proofs between equivalent domains.
Tamper-resistant audit trail with cryptographic hashing for improvement history.
Active research implementation. Core components are functional with tests. The Lean 4 validation layer successfully verifies generated proofs for arithmetic operations.
See docs/svm-paper-alignment-report-3.md for detailed alignment analysis.
Current State (63 benchmark specs):
- Domains: nat (50), list (5), pair (3), bool (5)
- Anti-hack mechanisms: 5 rules implemented with template-matching empirical signal
- Selection: Combined tournament + novelty (70/30 default)
- Architecture: Full adapter chain validated by integration tests
Remaining Gaps:
| Gap | Priority | Status |
|---|---|---|
| Top-level evolution runner executable | High | Adapter chain exists, needs wiring |
| Medium/hard boolean specs | Medium | Only easy bool specs exist |
| Behavioral novelty in fitness | Medium | Computed but not used |
| Rule set implementations | Low | Genome references missing modules |
| Evaluation result artifacts | Low | No committed results/plots |
docs/init/mathematical-machine-intelligence-framework.md- foundational conceptsdocs/architecture-brief.md- system designdocs/implementation/- implementation detailsdocs/svm-paper-alignment-report-3.md- paper ↔ code alignment status
AGPL-3.0 - Open research, non-commercial focus.