AI‑assisted proofs enter formal math

A growing number of research systems are producing proofs that are accompanied by machine‑checkable artifacts (Lean, Git repos) and public manuscripts. This development narrows the gap between human and machine roles in formal mathematics and creates new norms for provenance, verification, and attribution in research. — If AI routinely generates formally verifiable mathematical results, that will shift how science is done, how credit is assigned, and how states and institutions regulate advanced research tools.