Every issue an adversarial audit found in Mathlib, one declaration at a time. Each finding was checked in Lean, and every critical or major one was also put to a second model (Astra) to try to refute it.
These findings are LLM-generated (Claude, with GPT as the second opinion) and have not been reviewed by Mathlib maintainers. Treat each one as a claim to check. The raw data is findings.json.
| File | Audited | Declarations | Findings |
|---|
Critical: the library says something it does not mean, such as a wrong definition or a junk value that makes a statement hold for the wrong reason.
Major: a second definition or construction of something Mathlib already has, made for no good reason (shown equal by rfl in Lean).
Minor: a restated or duplicated lemma, an assumption stronger than needed, missing API, a misnamed lemma, or a wrong docstring.
Nit: naming style, missing docstrings, leftovers and other hygiene.
Confirmed findings come with Lean evidence: a probe that compiles, a probe that fails as expected, or a measured fact about the source. Suspected findings are a model's claim not yet checked in Lean.
The "Critical & major" tab lists the confirmed critical and major findings. Only the critical finding and a first batch of majors became draft PRs; the rest are recorded here so they do not crowd the Mathlib PR queue.
Probe paths such as hunts/…/probe1.lean refer to the red team's working files. Source links open the file at the Mathlib commit the audit used.