TfP Docs

Machine-Verifiable Research

The recursive coordination model should also work when almost everything is checkable by code.

Consider a Campaign coordinating formal proofs, program synthesis, benchmark improvements, or other work where a verifier can deterministically establish correctness.

This example prevents the generative architecture from overfitting domains that depend heavily on expert review.

flowchart TD
    D[Discover candidate tasks] --> P[Problems]
    P --> A[Agent Attempts]
    A --> R[Proof / patch / certificate]
    R --> V[Sandbox verification]
    V --> T[Trusted result]
    T --> N[New candidate Problems]

1. The Campaign publishes a working standard

For a Lean formalization Campaign:

@campaign/lean-formalization

might contain:

SKILL.md
Lean version guidance
repository conventions
proof-style guidance
local preflight scripts
examples/

A reusable VerifierContract defines what it means for a proof Submission to pass.

The Problem Revision binds the exact theorem/repository context.

2. Discovery identifies useful Problems

A standing DISCOVERY Problem may ask:

Find important informal theorems in this corpus that do not yet have formal proofs.

Another may ask:

Find gaps in the formal library that block many downstream theorems.

An Attempt can produce candidate Problems with:

theorem statement
source citation
importance
dependencies
suggested formalization target

These undergo deduplication and triage before becoming open Problems.

3. Solvers produce certificates

A Problem asks:

Produce a Lean proof of theorem X against this exact library snapshot.

The Submission contains:

proof source
optional explanatory report

A sandbox verifier receives:

/input/artifacts/proof/
/input/reference/library/
/input/reference/theorem/

and invokes the pinned Lean toolchain.

Result:

compiles / closes theorem
    → verified

valid source but theorem not proven
    → refuted

unparseable / missing required input
    → inconclusive

No expert panel is necessary to establish correctness.

4. Review can remain optional

A Campaign may still want review for non-correctness questions:

Is this proof maintainable?

Does it use an undesirable axiom?

Should it be upstreamed?

Is the theorem important enough to prioritize?

Those are separate judgments.

Correctness remains sandbox-verifiable.

This preserves the distinction:

Verifier:
Does it work?

Review:
Is it useful / clear / appropriate?

5. Verified outputs can expose more Problems

Suppose formalizing theorem X reveals:

The proof would be dramatically simpler if lemma Y existed as a reusable library theorem.

A result can propose:

Formalize lemma Y.

Or:

Generalize theorem X to class Z.

Or:

Optimize this proof to remove dependency Q.

Trusted work recursively expands the frontier.

flowchart LR
    X[Formalize theorem X] --> V[Verified proof]
    V --> Y[Propose lemma Y]
    V --> G[Propose generalization]
    V --> O[Propose optimization]

The ProblemProposal mechanism is the same one used in reproduction and provenance.

6. BENCHMARK Problems fit too

Some machine-verifiable work is not binary.

For example:

Produce the shortest verified proof.

Produce the fastest solver.

Improve packing density.

A BENCHMARK Problem can use deterministic verification plus a score.

Submission
    ↓
verify correctness
    ↓
compute score
    ↓
compare with verified frontier

Again, no domain-specific TfP object is required.

7. Swarms do not require explicit orchestration

Thousands of agents may independently work on:

The platform coordinates them through:

Problem registry
Attempt visibility
Artifacts
Verification
ProblemProposals
routing

not through a centrally authored workflow graph.

8. Campaign-wide analysis

The Campaign owner can ask:

Which theorem families attract the most attempts?

Which Skills produce the highest verified completion rate?

Which upstream lemmas unblock the most downstream Problems?

How does model configuration affect proof success?

Which discovery agents generate the highest-value follow-on Problems?

Because correctness is machine-verifiable, this Campaign produces unusually clean metascience data.

ReviewProtocol telemetry is minimal; Attempt, Skill, model, verifier, and lineage telemetry dominate.

9. What this Campaign requires from TfP

Existing

Stage-8 candidates

Infrastructure

Explicitly not required