Autonomous Proof Engine
Automated theorem proving in Lean 4.
Perqed is an open-source system that searches for mathematical witnesses, verifies them in Lean 4, and uses LLMs to direct the search when it gets stuck. Currently targeting open Ramsey number problems and Torus Decompositions.
Machine-Checked Proofs of the m=4 and m=6 Directed Hamiltonian Torus Decompositions
Verified proofs of Knuth's problem using Lean 4 and Perqed's parallel orchestrator.
Architecture
The proof loop
A hybrid search engine: heuristic annealing finds near-witnesses, Z3 repairs them, Lean 4 verifies them.
Formulate the Problem
The ARCHITECT reads the conjecture (e.g. R(4,6) ≥ 36),
determines the proof strategy—constructive witness or tactic
search—and generates the Lean 4 theorem signature.
Fast-Path SMT Check
Before expensive search, Z3 attempts an exact SMT solve over structured subspaces (e.g. circulant graphs). Proven empty subspaces are recorded as permanent lemmas.
Z3 · SMT Solver · ResearchJournalIsland-Model SA
8 parallel Simulated Annealing workers run with a diversity spectrum of cooling rates and patience—from rapid basin-hopper to deep explorer. Workers share their best result at round end.
Bun Workers · Adaptive Reheat · Hyperparameter DiversityLNS Finisher
Large Neighborhood Search selects the top J near-witnesses within energy K of the global minimum. Z3 attempts to repair each one by solving the residual constraint neighborhood.
Z3 · LNS · Multi-Candidate SelectionLean Verification
When a witness is found, it is compiled into a Lean 4
proof using decide and kernel-checked. For
non-constructive goals, DeepSeek Prover drives tactic search.
Memetic Pivot
If search fails, the ARCHITECT reads the ResearchJournal—accumulated lemmas, failure modes, and energy trajectories—and proposes a new strategy. The best near-witness warm-starts the next attempt.
Gemini 2.5 Flash · ResearchJournal · Warm-StartModel Stack
Runs on your hardware
Core search and tactic generation run locally. Gemini handles strategic planning.
Gemini 2.5 Flash
ARCHITECT · REASONER
Formulates problems, directs search pivots, interprets failure modes. ~$0.02/run blended.
DeepSeek Prover V2:7B Q8
TACTICIAN
Raw Lean 4 tactic generation via local Ollama. 1–2s per completion on Apple Silicon. ~7 GB VRAM.
Lean 4
Proof Kernel
Formal verification via tactic mode and decide. All proof steps are kernel-checked before acceptance.
Z3
SMT Solver · LNS Repair
Two roles: fast-path exact SMT search over structured subspaces, and Large Neighborhood Search repair of near-witness graphs.
Bun Workers
SA Island Model
8 parallel worker threads running Simulated Annealing with a diversity spectrum of hyperparameters. ~4M iterations/sec total throughput.
Building in public
Watch proof attempts in real time or read about progress on the blog.