Independent verification for AI-generated proofs
A proof assistant checks that a proof establishes a statement. It never checks that the statement means what you intended. Qed connects you with professional mathematicians who verify that it does — and sign their name to it.
-- summable bound, formalized by an AI system theorem key_bound (a : ℕ → ℝ) (S : ℝ) (hsum : True) (h : ∀ n, a n ≤ S) : (∑' n, a n) ≤ S := by -- ... 40 lines, no errors, no `sorry` ...
#print axioms: propext, Classical.choice, Quot.sound. Zero sorries. CI is green.
Toggle the reviewer. Same file. Two very different verdicts.
When Lean, Coq, or Isabelle accepts a proof, it certifies exactly one thing: this term has the type of this statement. That's real and valuable. But a statement can type-check perfectly while saying something other than what you meant — a hypothesis that's secretly contradictory, a definition stubbed to True, a quantifier in the wrong place, a divergent sum silently defined as zero.
The elaborator is complete on the type stratum — every type error raises. It is silent on the meaning. A semantically wrong but type-correct statement passes without complaint. AI systems fail in precisely this register: not a wrong algebra step (the kernel catches those) but a hallucinated assumption or dropped subtlety, presented as if derived.
Machine verification of an incorrect specification provides false confidence that may be worse than no verification at all.
— Tao et al., “From Solvers to Research,” arXiv:2607.07779 (2026)
A re-analysis of miniF2F, the field's most-cited benchmark, found statement-vs-intent discrepancies in over half its problems. And there is, today, no reliable automated way to check faithfulness — it takes a mathematician.
Every item below type-checks. Every one has shipped in a published benchmark or an AI-generated proof. This is the checklist a Qed verifier works through — by hand, against your intended claim.
An assumption like hsum : True, or one that's secretly unsatisfiable, makes the theorem trivially true. It says nothing — and the kernel never objects.
Omitted finite-dimensionality, a collapsed biconditional, the wrong domain. The formal claim is a weaker — or different — theorem than the one you set out to prove.
sorry & axiomsGaps elaborate to sorryAx and still show a checkmark. A stray custom axiom can silently make anything provable. Both need #print axioms and a human who reads it.
Lean's total functions return defaults on undefined input — a non-summable ∑' is 0, division by zero is 0. Bounds can hold vacuously until the missing hypothesis is added.
The proof is only as good as the definitions under it. A plausible-looking definition that's subtly wrong yields a flawless proof of the wrong thing.
Tactics like native_decide trust external code outside the kernel — an avenue for an AI to "prove" a falsehood. High-stakes projects ban them; we check you did.
You bring a result — a Lean/Coq/Isabelle repository, or an informal proof plus its formalization. We return a signed report you can cite, publish, or hand to a customer.
The theorem in plain mathematics, the formal statement, and the proof. We scope difficulty, the axioms and tactics in play, and match a verifier with the right subfield.
We reproduce the build, run #print axioms and an independent kernel re-check (lean4checker), and flag sorry, non-standard axioms, and trusted-code tactics — before a human spends a minute on it.
A professional mathematician reads the statement against your intent, audits the definitions, and stress-tests every hypothesis for vacuity. This is the judgment no tool can yet make.
Either a named attestation of what was verified and under which assumptions, or a precise account of what breaks and why. Optional second-verifier consensus for high-stakes claims.
Publishing a solved problem or a benchmark result? An independent attestation that the statement matches the claim is the difference between a headline and a retraction.
Formalized your paper's main theorem? Have the encoding checked for faithfulness and hidden gaps before a referee — or the internet — does it for you.
Protocol, ZK circuit, or safety-critical property. Verification moves the risk into the specification. We audit the part your prover assumes is correct.
We're assembling a bench of Lean-fluent mathematicians to do the judgment work no model can. If you can read a formal statement and tell whether it captures the theorem, this is paid, remote, and intellectually real.
Per-verification or retainer, remote, take what fits. Comparable expert-review work runs $150–300/hr; we'll set rates with the first cohort — that's part of what we want to learn from you.
You'll scrutinize freshly AI-generated and autoformalized proofs — the specification traps, the vacuous hypotheses, the junk-value bounds. The interesting failure modes, not homework.
Certificates carry the verifier's attestation. Early members shape the review protocol and standards for a field that doesn't have them yet.
Not sure you're a fit? If you've formalized anything in Lean, Coq, or Isabelle — or you referee proofs — we want to talk. Sign up as a verifier →
We're early — building a first cohort on both sides and figuring out the details in the open. Sign up and we'll reach out for a short conversation to learn what you need (and, if you're a verifier, what you'd want to be paid).
Check your inbox — we follow up within a few days to scope what you'd want verified.