Contributions published at that review
Vidick–Claude reports: a Lean formalization of MIP* = RE
Makes a substantial known theorem and its reductions machine-checkable through a documented formal development.
Formalization milestone; distinguish it from the original mathematical discovery
Roos–Claude reports: Carleson’s theorem via a different formal proof
Documents AI assistance in producing a substantial alternative formal proof of advanced harmonic analysis.
Formalization milestone; distinguish it from the original mathematical discovery
Vu-Le reports: uniqueness and stability of Gerver’s moving sofa
If correct, strengthens a known geometric optimum into uniqueness and a quantitative description of near-optimal shapes.
Scoped research contribution
Strinz–Claude reports: Möbius invariance of spherical Ramsey sets
Extracts a geometric invariance principle from the existing classification and makes the stated implication formally checkable.
Scoped research contribution
Vojdanovski reports: a Lean proof of a scoped Fröberg result
Makes a uniform partial theorem machine-checkable, including its quadratic argument in arbitrary characteristic.
Formalization milestone; distinguish it from the original mathematical discovery
Cremer reports: selecting the seventh of sixteen in 28 comparisons
Closes one small exact-selection case by an explicit algorithm and improves other finite comparison bounds.
Scoped research contribution
AI-assisted Jacobian counterexample in dimension three
Advances the stated target relative to the recorded baseline.
Verification update to an existing contribution
Follow-up review
Dedekind-zeta source versions reconciled
2026-10-15 · The retrieved version-two manuscript states 31/32 in Theorem 1.1 and matches the pinned formal challenge. The scoped attributed claim was published on 15 October. The earlier version-one mismatch is retained in the research record; neither proof is declared refuted.
Unresolved at that review
Improved Sidorenko bound formalization
The AI disclosure documents migration of an existing Lean 4.19 formalization and an extremal-limit extension. Review the prior artifact and manuscript baseline before deciding whether the substantive extension merits a distinct curated milestone. No AI discovery of the human manuscript theorem is established.
Coverage and limits
The review collected 543 Palomar listing records at registry revision 269. Papers With Lean supplied 1439 discovery records. These counts describe metadata collection, not completed proof reviews.
- All 543 Palomar listing records were collected at revision 269; metadata collection does not establish a detailed review of all 543 proofs or AI roles.
- Papers With Lean supplied 1439 metadata records; targeted recent leads were followed to original sources, not a full historical survey.
- Lean community blog and AFP index were checked for relevant project reports; existing sphere-packing and unsplittable-flow entries were not duplicated.
Palomar’s checking policy explains its mechanical checks and automated statement review. Registration does not certify novelty, importance, or human peer review. Under current criteria, AI must supply a central idea or result; formalizing an existing human proof alone does not qualify.
Lean and Isabelle are proof assistants: they check precisely expressed statements under their assumptions. Each curated record identifies the checker, exact scope, and whether the check is reported or reproduced. Read the verification criteria.
This review uses Palomar’s paginated registry, Papers With Lean, Lean community project reports, and the Archive of Formal Proofs. We follow candidates to primary sources and retain unresolved questions.