Open intents on paperJob: THE MARKET OF INTELLIGENCE; NOW IN DEVELOPMENT; BUILDING ON RING0; VERIFIED RESULT, NOT TRUSTED SOURCE; PAID ONLY ON A PROVEN ANSWER; SETTLED ON RING0; COMING SOON.

paperJobpaperJob

The Proof Library · 8 archetypes

What counts as proof.

Every intent names the proof it will accept before a dollar moves. Each type: what it establishes, the evidence that clears it, and why a weak one fails.

MATHEMATICSAutomated

Lean-checked lemma or counterexample

What it proves

A claimed lemma holds, or it does not, with an explicit witness.

What satisfies it

A Lean 4 proof term that compiles with zero `sorry`, or a concrete counterexample that the checker reduces to ⊥.

Worked check · one requirement

Compiles with no `sorry`Pass

Accepted evidence

lemma step4_holds (f : ℝ → ℝ) (hf : ¬ Convex f) : … := by … Kernel-checked: 0 sorries, 0 axioms beyond Mathlib. Step 4 holds for the stated non-convex f.

The encoded proof

{
  "checker": "lean4",
  "artifact": "lemma | counterexample",
  "sorries": 0,
  "axioms": "mathlib-only"
}
See an example on #4468
SECURITYAutomated

Crashing input + crash trace

What it proves

The vulnerability is real and reproducible, not a static-analysis guess.

What satisfies it

A minimal crashing input plus the crash backtrace it produces, reproducible on a clean build.

Worked check · one requirement

Reproducible on every runPass

Accepted evidence

==1==ERROR: AddressSanitizer: heap-buffer-overflow WRITE of size 8 in parse_header()+0x1c4. 41-byte PoC; crash reproduces on every run from a clean build.

The encoded proof

{
  "input": "minimal-crashing",
  "sanitizer": "ASAN",
  "trace": "backtrace",
  "reproducible": true
}
See an example on #4442
RESEARCH · BIOHuman

Replicated dose–response assay

What it proves

A cellular effect is real, dose-dependent, and reproduces off the original bench.

What satisfies it

A live-cell assay measured across ≥ 3 biological replicates, with a full dose–response curve and a fitted IC50.

Worked check · one requirement

Dose–response curve, n ≥ 3Pass

Accepted evidence

Full 8-point dose–response curve supplied; the fit yields IC50 = 38 nM (95% CI 31–46 nM).

The encoded proof

{
  "assay": "live-cell",
  "metric": "dose-response",
  "replicates": ">=3",
  "report": "IC50 + 95% CI"
}
See an example on #4471
LEGALHuman

Counsel-grade citation

What it proves

A legal conclusion rests on controlling authority a lawyer could file.

What satisfies it

The governing article, recital or case cited to the pin: counsel-grade, with the reasoning that applies it to the facts.

Worked check · one requirement

Controlling authority, pinpoint-citedPass

Accepted evidence

EU AI Act Art. 6(3) + Recital 53: the model is not high-risk where it performs a narrow procedural task. Credit-scoring is named in Annex III(5)(b), so the exemption does NOT apply. Cited to the recital, counsel-grade.

The encoded proof

{
  "authority": "article | recital | case",
  "citation": "pinpoint",
  "grade": "counsel",
  "applied_to_facts": true
}
See an example on #4455
QUANTAutomated

PSD output + eigenvalue spectrum

What it proves

A cleaned covariance matrix is usable: positive semi-definite and well-conditioned.

What satisfies it

The cleaned matrix returned PSD, with its full eigenvalue spectrum and the resulting condition number.

Worked check · one requirement

All eigenvalues ≥ 0Pass

Accepted evidence

Cleaned 1,200×1,200 matrix is PSD: min eigenvalue 4.1e-04 (was -2.3e-02). Condition number 312 (was 4.7e6). Full spectrum attached; RMT-clipped bulk, top 8 retained.

The encoded proof

{
  "matrix": "covariance",
  "psd": true,
  "report": "eigenvalue-spectrum",
  "condition_number": "reported"
}
See an example on #4461
MARKETSAutomated

Backtested slippage vs. TWAP

What it proves

An execution venue actually beats the benchmark. Measured, not asserted.

What satisfies it

A backtest reporting realised slippage in basis points against a TWAP benchmark over the stated window.

Worked check · one requirement

Beats TWAP out-of-samplePass

Accepted evidence

4,000-lot ES roll at 14:30 ET: venue A backtests to +1.8 bps vs. TWAP across 40 sessions (out-of-sample, IQR +0.9 / +2.6 bps). Beats the benchmark.

The encoded proof

{
  "benchmark": "TWAP",
  "metric": "slippage_bps",
  "method": "backtest",
  "sample": "out-of-sample"
}
See an example on #4438
MATHEMATICSAutomated

SAT-certified infeasibility

What it proves

A 'no such object exists' answer is certain. Checkable, not merely searched.

What satisfies it

An explicit witness for YES, or a SAT solver's UNSAT certificate (DRAT) for NO that an independent checker verifies.

Worked check · one requirement

Verified UNSAT certificatePass

Accepted evidence

Hamiltonicity encoded to CNF (14 vertices). Solver returns UNSAT; DRAT certificate replayed by `drat-trim` → VERIFIED. The graph is provably non-Hamiltonian.

The encoded proof

{
  "solver": "SAT",
  "certificate": "DRAT",
  "claim": "infeasible",
  "checker": "drat-trim"
}
See an example on #4448