NexusAgent is a graph-augmented Lean 4 verification pipeline for evaluating, filtering, and indexing formally verified proof artifacts from the Formal Conjectures benchmark corpus (arXiv:2605.13171).
Independence notice: This is an independent research project by Nasser Towfigh. It is not affiliated with, endorsed by, or derived from Google DeepMind or any of its products. It uses the Formal Conjectures benchmark (arXiv:2605.13171) released by Google DeepMind under Apache 2.0.
Lean 4 Proof Parts
│
▼
NexusAgent Pipeline
│
┌────┼────────────┐
▼ ▼ ▼
Axiom Holdout Neo4j
Check Filter Fossil Vault
│
▼
Verified Benchmark Results
| Document | Audience | Purpose |
|---|---|---|
docs/CONCEPTS.md |
New readers — start here | The mental model: the two modes (verification + proof search), the four subsystems, what NexusVerifier is not. |
docs/GETTING_STARTED.md |
New users | Real setup: clone with submodule, build formal-conjectures (~20 min), Neo4j, .env, first dry-run. |
docs/CLI_REFERENCE.md |
All users | All 8 commands (solve, bench, schema, stats, probe, ingest-hg, scan-hg, ingest-parts) with flags and outputs. |
docs/architecture.md |
Contributors | The unified internal picture (Lean oracle + agent pipeline + Neo4j + Topos), replacing the older 61-line stub. |
docs/CONFIGURATION.md |
Operators | The full env-var surface (~19 vars) and three README-vs-code discrepancies worth knowing. |
docs/TOPOS_INTEGRATION_REPORT.md |
Contributors | The Topos integration: what was built, the 12-test suite, Neo4j parity. |
docs/FC100_GAP_SET_METHODOLOGY.md |
Reviewers | The benchmark-corpus error writeup — read before citing any benchmark number. |
docs/hypergraph-engine.md |
Researchers | The Lean-native hypergraph (Phase 1/2 — orthogonal to Topos). |
SPEC.md |
Contributors | The original design spec (May 2026; some sections predate recent pipeline hardening). |
SOLVED_PROBLEMS.md |
Reviewers | Per-problem mathematical descriptions of highlight results (see the FC100 correction above). |
This repository is an experimental research infrastructure project.
The FC100 benchmark corpus contains previously solved, non-open mathematical results with existing Lean formalizations. NexusAgent evaluates verification policy, axiom provenance, holdout isolation, and reusable proof indexing over this corpus.
This repository does not claim novel proofs of open Erdős problems.
Running FC100 problems through NexusProverSubagent surfaced and fixed four
real false-positive/reward-hacking gaps in the prover pipeline itself:
- A
LeanOraclecompile check that could reportCompiled=trueon output Lean had actually rejected (||vs&&logic error, plus a stale error regex against a newer Lean diagnostic format). - A
SketchValidatorstructural gate that could be defeated by substring name matching or shadowing the original declaration with a newdef. - Sorry-citation-laundering: citing an already-
sorry'd declaration compiles clean withSorryCount=0and no warning at the citing site — only#print axiomsreveals the inheritedsorryAx.LeanOraclenow runs that check whenever a sketch looks fully proved. - A stale DeepSeek model-name mapping causing silent API failures.
A follow-up audit found a fifth, distinct issue — not a pipeline bug, but a
corpus-selection error in the ad-hoc "gap-set" experiments used to test
whether multi-sample search helps solve rate: the candidate problems were
built from FC100SolvedSet1 (upstream's curated already-solved corpus)
instead of FC100OpenSet1 (the actual open-problems corpus). Because the
reconstructed sketches still import the original file, the complete
upstream proof stays in scope and citable by name — sound (#print axioms
clean) but not novel. Full write-up, evidence, and a citation-vs-independent
classification of every solve: docs/FC100_GAP_SET_METHODOLOGY.md.
Corrected rerun, against the actual FC100OpenSet1 corpus: most of it
(60/94 found declarations) turned out to use formal-conjectures'
answer(sorry) idiom — the statement itself embeds an unknown-answer
placeholder, so no proof of it can ever be sorryAx-free by construction,
independent of prover capability. Filtering to the 34 fully-specified "plain"
open problems and preflighting left 23 genuine famous open conjectures
(smooth 4D Poincaré, Mandelbrot local connectivity, Littlewood, Gilbreath,
Selfridge, Grimm, the class number problem, transcendence of π^π^π, …).
Result: 0/23 solved — the correct, expected outcome, not a failure.
This is the number that should be cited for this pipeline's actual
proof-search capability, not the 28% figure above. Details in the same doc.
Large language models can generate syntactically valid Lean proofs that rely on weakly trusted native compilation paths, or leak benchmark information through related declarations from the same problem file.
NexusAgent addresses this by:
- Mechanically verifying proof artifacts using
lake env lean+#print axioms - Filtering by axiom provenance — rejecting proofs that depend on native compilation (
Lean.ofReduceBool,Lean.trustCompiler) - Enforcing declaration-family holdout isolation — when one declaration from a problem file is held out, all sibling declarations from the same parent are automatically excluded, preventing leakage between related theorems
- Storing reusable verified subgoals in a graph-backed knowledge base (the "fossil vault") for future retrieval and tactic reuse
This is the infrastructure layer that separates rigorous formal verification from superficially plausible proof generation.
NexusAgent is theorem-proving infrastructure. It provides:
| Capability | Description |
|---|---|
| Benchmark reproducibility | Deterministic, containerised verification of Lean proof artifacts |
| Axiom filtering | Mechanical rejection of proofs depending on native compilation |
| Proof provenance | Every verified part is tagged with its full axiom closure |
| Holdout isolation | Declaration-family holdout prevents cross-theorem leakage |
| Graph reuse | Verified sub-goals indexed in Neo4j for future proof retrieval |
Evaluated on 10 sampled parts from the
FC100SolvedSet1 corpus —
100 non-open problems with known sorry-free Lean 4 proofs — under a
restricted axiom policy (native_decide → reject):
| Status | Count | Meaning |
|---|---|---|
| Verified | 7 | Lean proof accepted; axiom closure ⊆ {propext, Classical.choice, Quot.sound} |
| Rejected | 3 | Proof depends on native compilation axioms (decide +native) |
| Excluded | 0 (1 with holdout) | Removed by declaration-family holdout policy |
Re-verified 2026-07-26 against the fixed pipeline (post #1/#2) — identical result. This gate runs AxiomChecker, which launches Lean directly rather than going through LeanOracle, so it was never exposed to the false-positive compile check fixed in #1.
Holdout test: Excluding Erdos1074.erdos_1074.variants.EHSNumbers_init
automatically excludes erdos_1074.variants.mem_pillaiPrimes (same parent erdos1074)
— confirmed 6 passed, 3 rejected, 1 excluded.
The pipeline enforces declaration-family holdout isolation to prevent leakage between related theorems originating from the same benchmark problem file.
Provenance: The 7 verified parts are pre-existing Lean 4 proof terms from the FC corpus — proofs authored by the FC benchmark contributors, not generated by NexusAgent. NexusAgent's role is mechanical verification (axiom-closure filtering + holdout isolation), not proof synthesis.
FC100SolvedSet1 is a corpus of already-solved, non-open problems with known Lean formalizations; this pipeline verifies them mechanically and filters by axiom strength.
NexusAgent.Core depends on Topos
(a typed-property hypergraph library, vendored as a git submodule at
external/Topos) as its representation for two independent graph-native
subsystems:
- AND-OR backward chainer — the proof-search planner's candidate-lemma
expansion is backed by a real
HypergraphKernelinstance, not a hand-rolled linked structure. ProofGoalGraph— per-SolveAsync-run memory of proof goals and tactic attempts (NexusAgent.Core/Planning/ProofGoalGraph.cs). Goal vertices and tactic-attempt edges are recorded as the prover explores, so the LLM prompt can show failed-attempt history and sibling-subgoal structure for the goals it's currently working on, instead of having zero memory of what already failed. Purely additive prompt context — it never influencesCompiled/SorryCount/IsFullyProved/the structural gate.
Both are ephemeral, per-run local state (NexusOrchestrator and
NexusProverSubagent are DI singletons nexus bench calls concurrently
across different problems) — no cross-run persistence yet.
| Layer | Technology |
|---|---|
| Formal language | Lean 4 (v4.27.0) + Mathlib |
| Proof verification | lake env lean + #print axioms |
| Graph backend | Neo4j 5 (Community via Docker; Enterprise locally) |
| Agent pipeline | C# / .NET 10 |
| Tests | 122 unit tests (xUnit) |
| Container | Docker (multi-stage, ~1.6 GB) |
Verified with:
- Lean
v4.27.0(elan-managed, baked into Docker image) - Mathlib pinned via
lake-manifest.jsoninformal-conjectures/ - Neo4j 5.x
- .NET 10
- Docker Desktop 4.x (macOS arm64)
# 0. This repo has a git submodule (external/Topos) — either clone with
# --recurse-submodules, or if already cloned:
git submodule update --init --recursive
# 1. Clone and build the formal-conjectures project (downloads ~1 GB Mathlib)
git clone https://github.com/google-deepmind/formal-conjectures
cd formal-conjectures
lake update && lake build # ~20 min on first run
cd ..
# 2. Configure environment
cp .env.example .env
# Edit .env — set NEO4J_PASSWORD and optionally LLM API keys
# 3. Build the NexusAgent image
docker build -t nexus-agent:latest .docker run --rm \
-v /path/to/formal-conjectures:/formal-conjectures \
-v "$(pwd)":/workspace:ro \
-e NEXUS_NEO4J_URI=bolt://host.docker.internal:7687 \
-e NEXUS_NEO4J_PASSWORD=your_password \
-e NEXUS_NEO4J_DATABASE=nexusdb-snapshot \
-e NEXUS_LEAN_PROJECT=/formal-conjectures \
-e NEXUS_PARTS_NATIVE_DECIDE=reject \
nexus-agent:latest \
ingest-parts --from-json /workspace/parts.json --dry-runExpected output:
[ingest-parts] 10 parts from parts.json sinks=[fossil] (DRY RUN — no writes)
FAIL erdos_1148.variants.lower_bound — native axioms (policy=reject): [...]
PASS [Weaker] erdos_647.variants.twenty_four axioms=[propext, ...]
...
[ingest-parts] Done: 7 passed, 3 rejected, 0 excluded (holdout).
echo "Erdos1074.erdos_1074.variants.EHSNumbers_init" > /tmp/fc100_targets.txt
docker run --rm \
-v /path/to/formal-conjectures:/formal-conjectures \
-v "$(pwd)":/workspace:ro \
-v /tmp/fc100_targets.txt:/tmp/fc100_targets.txt:ro \
-e NEXUS_NEO4J_URI=bolt://host.docker.internal:7687 \
-e NEXUS_NEO4J_PASSWORD=your_password \
-e NEXUS_NEO4J_DATABASE=nexusdb-snapshot \
-e NEXUS_LEAN_PROJECT=/formal-conjectures \
-e NEXUS_PARTS_NATIVE_DECIDE=reject \
nexus-agent:latest \
ingest-parts --from-json /workspace/parts.json \
--exclude-targets /tmp/fc100_targets.txt \
--dry-runExpected: Done: 6 passed, 3 rejected, 1 excluded (holdout).
NexusAgent also runs as an active proof-search agent: given a theorem statement from the
FC corpus, it attempts to produce a sorry-free Lean 4 proof using its graph-guided planner
and LLM tiers. Results below are from May 2026 benchmark runs; full telemetry
(per-problem outcomes, cost, turn counts, fossil hits) is in
data/results/ and summarised in
SOLVED_PROBLEMS.md.
Note on naming: The directory names
erdos_phase8/anderdos_phase9_ams5/continue the build-phase numbering from SPEC.md §5 — Phases 0–7 were infrastructure construction (LeanOracle, Neo4j schema, HallucinationGate, ProofCartographer, etc.). Phase 8 was the first live benchmark execution; Phase 9 was the expanded AMS-5 corpus run.
Terminology: Compiled = Lean accepted the file (may include
sorry). Sorry-free = axiom closure contains nosorryAx; the proof is mechanically complete. All sorry-free proofs were verified by#print axiomsinside the pipeline.
| Metric | Value |
|---|---|
| Problems attempted | 10 |
| Compiled (Lean accepts file) | 10 / 10 |
| Sorry-free proofs | 7 / 10 |
| Sorry-bearing (compiled, incomplete) | 3 / 10 |
| Total LLM cost | $0.44 |
Sorry-free: #109 (Erdős sumset conjecture), #139 (Szemerédi's theorem), #194, #219 (Green–Tao), #228 (flat Littlewood polynomials), #239, #250.
| Metric | Value |
|---|---|
| Problems attempted | 66 |
| Compiled (Lean accepts file) | 53 / 66 (80%) |
| Sorry-free proofs | 43 / 66 (65%) |
| Aborted | 12 |
| Budget exhausted | 1 |
| Total LLM cost | $4.81 |
See SOLVED_PROBLEMS.md for per-problem mathematical
descriptions of the 15 highlight results, and data/results/ for
HTML and JSON reports with full per-problem telemetry.
The axiom policy is controlled by NEXUS_PARTS_NATIVE_DECIDE:
| Value | Behaviour |
|---|---|
reject (default) |
Parts using native_decide / Lean.trustCompiler are rejected outright |
flag |
Parts are accepted but tagged :native-flagged in SourceProblems |
| (anything else) | Falls through to reject — warn/allow (documented in older versions of this README and .env.example) are not implemented |
A proof is Verified when its axiom closure is a subset of
{propext, Classical.choice, Quot.sound} — the standard Lean 4 logical foundation.
Any additional axioms (especially native compilation bridges) indicate reliance on
unverified reduction paths and are rejected under the reject policy.
Scope tags ([Weaker], [Instance], [Part]) are independent of verification status
and indicate how the proven statement relates to the original conjecture — a full-strength
theorem can be axiom-clean, and a weaker variant can still be axiom-unsound. These are
reported alongside the verification result, not as a sub-grade of it.
Full configuration surface (the ~19 env vars the code actually reads, beyond the 8 listed below): see
docs/CONFIGURATION.md. It also documents two other README-vs-code discrepancies worth knowing.
| Variable | Default | Description |
|---|---|---|
NEXUS_NEO4J_URI |
bolt://localhost:7687 |
Neo4j Bolt URI |
NEXUS_NEO4J_USER |
neo4j |
Neo4j user |
NEXUS_NEO4J_PASSWORD |
(empty) | Neo4j password |
NEXUS_NEO4J_DATABASE |
neo4j |
Database name |
NEXUS_LEAN_PROJECT |
(required) | Path to built formal-conjectures checkout |
NEXUS_PARTS_NATIVE_DECIDE |
reject |
reject (default) fails proofs using decide +native; warn accepts but flags |
GOOGLE_API_KEY |
(optional) | Gemini hallucination gate |
DASHSCOPE_API_KEY |
(optional) | Qwen cloud gate |
cd NexusAgent
dotnet build NexusAgent.sln
# Run all unit tests (122 tests; 3 in ProofFossilizerTests require a
# local Neo4j instance and are not yet tagged Category=Integration)
dotnet test NexusAgent.Tests/NexusAgent.Tests.csproj \
--filter "Category!=Integration" -v qNexusAgent/
NexusAgent.Core/ # Configuration, Neo4j client, LeanOracle, planning
Planning/ProofGoalGraph.cs # Topos-backed per-run goal/attempt memory
NexusAgent.Cli/ # CLI entry point (ingest-parts, bench, …)
NexusAgent.VerifiedParts/ # AxiomChecker, VerifiedPartIngestor, holdout logic
NexusAgent.MathlibIngestor/ # Mathlib tactic graph ingestor
NexusAgent.Tests/ # 122 unit tests (xUnit)
external/Topos/ # git submodule — hypergraph backend (see above)
formal-conjectures/ # Separate clone of google-deepmind/formal-conjectures (not a submodule)
data/ # Benchmark input files and results
docs/ # Architecture notes, Neo4j schema, Cypher queries,
# FC100_GAP_SET_METHODOLOGY.md
- Graph-guided proof retrieval — query the fossil vault for reusable sub-goals by goal-state similarity
- Tactic reuse — surface verified tactic sequences from the knowledge graph during proof search
- Proof clustering — group structurally similar proofs to detect common patterns
- Fossil-vault retrieval policies — configurable strategies for querying verified sub-goals
- Automated theorem search — use the hypergraph structure to identify candidate lemmas for new conjectures
- Expanded benchmark coverage — evaluate over the full FC100 corpus and beyond
Apache 2.0. See LICENSE.
The formal-conjectures/ directory is governed by its own license
(Apache 2.0).