AI‑formalized math advances

Large language models, when combined with formal proof assistants, are beginning to produce independently checkable solutions to previously open high‑level math problems, and to scale progress across long tails of obscure conjectures (Erdos problems). This creates immediate issues around provenance, authorship, peer review, reproducibility, and how mathematical credit and publication norms should adapt. — If AI routinely advances mathematical frontiers, governments, funders, journals and universities must update research‑governance rules (verification standards, attribution, audit trails) to preserve integrity and public benefit.