What was already known
Ibragimov posed the unrestricted central limit claim in 1971; Iosifescu later proposed a stronger invariance principle. Prior positive results required an additional variance condition.
AI involvement
The repository credits GPT-6 Astra with the rare-spike and feedback construction and Lean disproof under Tom Adamczewski’s direction. It does not document a named human explanation or completed human proof check.
The repository explicitly attributes the central construction and Lean disproof to GPT-6 Astra, under Adamczewski’s direction; no no-human-input session is documented.
- Supporting source (github.com) — Provenance; Summary and roadmap; Build and verify
- Supporting source (github.com) — Formal statement audit; proof construction and residual risks
- Supporting source (github.com) — 5 September 2026 prior baseline and near-miss search
- Supporting source (github.com) — parts.i formal statement and disproof target
Importance
If the formal statement matches the historical hypotheses, the construction refutes the longstanding CLT claim and, by implication, the stronger invariance claim.
Limitations
Lean checks the formal disproof of the CLT part, not a separate invariance-principle statement. The source calls the result a candidate; its machine-written statement-faithfulness analysis lacks independent human review or a reproduced kernel run.
Technical verification
The recorded verifier accepted the exact parts.i disproof with Lean’s default kernel and only standard axioms; a source-provided statement audit maps the formal hypotheses to the classical CLT. This is reported machine verification, awaiting independent replay and expert review.
Formal checking
Recorded Lean default-kernel and comparator acceptance with standard axioms for parts.i; exact dependencies were not replayed here.
- Checker
- Lean 4 default kernel and recorded comparator verifier
- Scope
- Formal Conjectures parts.i CLT disproof
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Default for missing human explanation: the detailed mechanism and formalization audit are machine-written, and no named human probabilist explains or endorses the central feedback/rare-spike mechanism.
Correction and publication history
One formal CLT counterexample across two directory entries; the stronger invariance statement follows only by implication and is not separately formalized.
Read this published revision