Project Orion

First End-to-End Result

Target: Graded Order Combinatorics — level sets, rank-generating polynomials, and saturated chains over graded posets.

Metric	Value
Definitions	2
Theorems proved	16
Lean 4 source	250 lines, 3 files
sorry / axiom	0
Automated cost	~$15.80
Wall time	1h 10m

The output compiles cleanly against Lean 4 v4.29.0-rc2 and Mathlib.

Architecture

The system is organized into five pillars, each an independent Python module:

1. Edge Finder — Identifies underdeveloped “pockets” in Mathlib by combining LLM concept generation, LeanExplore search, and algorithmic scoring.
2. Proof Oracle — Proves individual lemmas by spawning fresh Claude Code sessions equipped with lean-lsp-mcp (compiler diagnostics) and LeanExplore (Mathlib search) via MCP. Every proof is hard-gated: lake env lean must report zero errors, zero sorry, zero axiom.
3. Library Architect — Decomposes a mathematical theme into a dependency-ordered blueprint. Uses a two-pass pipeline: skeleton pass for mathematical intent, then a grounded expansion pass using LeanExplore to anchor every signature against real Mathlib declarations.
4. Library Weaver — Walks the dependency DAG in topological order, accumulates Lean source files, and invokes the Proof Oracle for each entry.
5. Proof Foundry (future) — Assembles verified proofs into Mathlib-conformant pull requests.

Key Design Decisions

• Hard verification gate. Every proof is verified by lake env lean — the actual Lean compiler, not an LLM self-report.
• Grounded signatures. Library Architect searches real Mathlib declarations before generating Lean 4 signatures, eliminating hallucinated API names — the #1 failure mode in LLM-generated formal math.
• Docs-first development. Every subsystem has a design document written before implementation and a walkthrough written after.