AI Changes Who Gets Credit for Proofs

Large, cheap autoformalization projects (for example the Math, Inc. sphere‑packing formalization and Knuth's commentary) are starting to produce machine‑verified, publishable proofs at scale. That will shift authorship, citation, and tenure debates: institutions, teams that run formalizers, and the formalizers themselves may claim scientific credit, forcing new norms about attribution and verification. — If machines can produce and verify significant proofs, universities, journals, and funding bodies will have to decide who counts as a mathematician or author and how to evaluate machine‑produced knowledge.