Represent proof search as state
Rust types represent claims, definitions, subgoals, attempts, and strategy families. A SQLite ProofStore records branches and claim evidence rather than leaving the search as an unstructured conversation.
01 / THE IDEA
A closer look.
A proof-orchestration prototype combining a Rust state and search core with a Python proposer and solver stack. AMPP models candidate claims, strategy branches, subgoals, verification stages, and audit artifacts; parts of the verifier stack remain scaffolding and do not yet justify unconditional formal-proof guarantees.
Creative search and mathematical acceptance have different jobs. AMPP explores how candidate generation, branch management, solver interfaces, and a claim store can be separated so the evidence behind a proposed proof step is inspectable. The current implementation also makes the remaining acceptance gaps concrete.
Generate across strategy families
The Python ensemble orders proposers by weights, collects candidates, deduplicates hashes, and applies rubric triage. Strategies include induction, contradiction, extremal arguments, constructions, and double counting.
Orchestrate staged checks
The Rust cascade runs structural validation and then dispatches the candidate’s selected Python stages. Adapters cover counterexample-search scaffolding, SymPy, Z3, external theorem provers, and Lean source compilation.
Keep branch and artifact history
Beam states track accepted claim counts, resolved subgoals, and stale iterations. Run artifacts and verification records expose how a branch evolved and which stages produced a response.
02 / UNDER THE SURFACE
A candidate’s path through the proof pipeline
Inspect the stage contracts carefully: “not rejected” is not the same as a formal proof.
DRAG TO PAN · SELECT A NODE · + / − TO ZOOM
Read the architecture as text
- Problem normalization — The normalizer turns the input problem into a structured specification used by the planner and proposers. This is an interpretation step, not independent mathematical verification of the resulting statement.
- Subgoal planner — Planner inserts a top-level target subgoal and auxiliary edge-case subgoals into the store. It queries unresolved work and can mark a subgoal resolved as the orchestration progresses.
- Strategy beam — BeamState scores accepted claim count and resolved subgoals against stale iterations. BeamSearchManager orders active states, prunes stale branches subject to its minimum, and avoids adding duplicate active strategy families.
- Proposer ensemble — The ensemble invokes active strategy proposers in weight order, gathers their StepCandidates, filters previously rejected or duplicate hashes, and passes candidates through optional rubric triage.
- Typed candidate — StepCandidate packages proposed statements, dependency IDs, Lean source, small-case tests, and a verification plan. Schema validity describes a well-formed proposal; it does not establish that the proposal is true.
- V0 structural check — StructuralChecker validates candidate structure and requires listed dependencies to appear in the branch’s accepted claim set. Unknown Lean names are logged as warnings; known stage names are checked against V0–V5.
- Python worker bridge — The Python worker uses one JSON object per line over stdin/stdout and sends logs to stderr. A stage field dispatches normalization, proposal generation, or a selected verifier with request IDs and context.
- V1 counterexample scaffold — The interface contains small-case, bounded-enumeration, and random-search loops. In this revision its shared _evaluate_claim method is explicitly a stub that always returns True, so this stage does not provide general falsification evidence.
- V2 symbolic adapter — SymPyVerifier attempts to simplify supported equalities and inequalities. A refutation rejects the stage, but undecidable statements and an absent SymPy dependency are not treated as proof failures.
- V3 SMT adapter — The Z3 adapter negates supported simple claims and checks satisfiability. Its translator covers narrow arithmetic patterns; unknown or unexpressible claims return undecided internally and are not equivalent to proof certificates.
- V4 theorem prover — ATPVerifier translates supported claim material into an external prover workflow. A missing prover binary can skip this stage; availability and supported encodings must be inspected before interpreting its result.
- V5 Lean compilation — LeanVerifier wraps candidate.lean_stub with Mathlib imports and an AMPP namespace, writes a temporary file, and invokes Lean. If Lean is absent, verify returns passed=True with skipped=True; compilation is therefore not universally required by the current path.
- Cascade decision — VerificationCascade always performs V0, then runs only stage names selected by the candidate. It records artifacts and rejects explicit failures. After selected stages pass, it creates an accepted claim, so skipped or undecidable adapters are a material trust-boundary limitation.
- ProofStore — The SQLite store supplies accepted dependencies, rejected hashes, and branch state to the cascade. The source marks a claim Verified after selected stages pass; that stored status should not be confused with a mandatory Lean-checked theorem.
- Rejection memory — On an explicit verifier failure, the cascade records the failed attempt and registers the candidate hash. The ensemble can use the rejected set to avoid proposing an identical candidate again.
- Run artifacts — The artifact module defines a run manifest and paths for emitted proof and verification material. These files preserve what happened in a run; their existence alone does not establish a valid formal proof.
03 / INTERACTIVE STUDY
A finite search is not a proof
Explore an illustrative candidate frontier and bounded tests of the claim that n² + n + 17 is always prime. A single counterexample refutes it; passing a finite range cannot prove it.
CHANGE THE INPUTS
Educational browser model, not AMPP execution. The real V1 evaluator is currently a placeholder. The finite example has a counterexample at n=16; no slider setting constitutes a formal proof or a real search-performance result.
ILLUSTRATIVE MODELLIVE
04 / ENGINEERING CHOICES
Why it works this way.
Separate proposals from the state core
Python supplies flexible proposal and solver integrations while Rust tracks typed search and claim state. The bridge is a narrow protocol rather than shared mutable in-process objects.
Record failures as search input
Candidate hashes and failed attempts make retries inspectable and allow exact rejected proposals to be filtered. This avoids treating every new generation as unrelated work.
Treat the verification gaps as unfinished work
The intended architecture distinguishes creativity from acceptance, but the current cascade permits selected stages, skip-as-pass adapters, and a placeholder V1 evaluator. Mandatory proof certificates and fail-closed handling would be needed for stronger guarantees.
05 / OPEN THE SOURCE
Trace it back.
Implementation details, examples, and project documentation.
Cascade acceptance logic
Selected-stage execution, rejected hashes, artifact recording, and the final stored claim status.
Counterexample evaluator boundary
Bounded/random-test scaffolding and the current always-True placeholder evaluator.
Lean adapter boundary
Temporary Lean file compilation and skipped success when Lean is absent.
Search and branch state
Branch scoring, staleness, active strategy diversity, and state synchronization.
Scope & limitations
- This revision is an experimental orchestration prototype, not evidence of unconditional machine-checked theorem solving. Its V1 claim evaluator is a stub that returns True.
- The cascade runs candidate-selected stages; absent solvers can be skipped with a passed response, and some undecidable results are not rejected. Stored Verified status therefore does not imply mandatory Lean certification.
- The portfolio lab demonstrates a finite mathematical example and search bookkeeping only. No external solver, language model, Lean compilation, or source test suite was executed for this page.
Architecture and descriptions reflect the linked repository snapshot. The playground explains a mechanism; it does not execute the repository or report measured performance.