AI in mathematics is forcing big questions

The sharpest distinction was between a proof being valid in Lean and a proof being worth merging into Mathlib, the shared Lean library. Many people treated the latter like software maintenance, not metaphysics. A 200,000-line generated proof may typecheck, yet still be bad library code if it is brittle, slow, undocumented, built on one-off definitions, or impossible to refactor when upstream lemmas change. That framing cut through a lot of the rhetoric. The objection was usually not "the theorem is false". It was "this is tech debt in the foundations of knowledge." That fed the deeper argument about what mathematics is for. A large chunk of the conversation rejected the idea that the theorem alone is the interface. They argued that the real value of math often sits in the intermediate lemmas, definitions, and proof techniques that later unlock other areas. History backs that view. Big results matter partly because they create tools, like how work around quintic equations led to Galois theory, or how Wiles's proof mattered beyond Fermat itself. Under that lens, an unreadable formal proof is closer to a binary than source code. It may certify a statement, but it does little to enlarge human understanding. Others pushed back that this is still anthropocentric. The universe does not owe humans elegant proofs, and a true machine-checked result can be useful even if nobody grasps the internals. That side did not win the conversation, but it did sharpen the stakes. If AI can generate correct but alien mathematics, human math may split from machine math, with libraries and standards optimized for one or the other. A separate practical thread focused on trust. Proof assistants shrink the trust surface, but they do not eliminate it. You still trust the kernel, the toolchain, the hardware, and the theorem statement itself. Several commenters pointed to the active effort to keep proof kernels small and to techniques like exporting proof objects for checking by independent programs. The consensus here was pragmatic: machine checking is a major advance for correctness, but not a license to dump opaque slop into core libraries or stop human review. The discussion also touched the economics of the field. If frontier mathematical AI depends on proprietary models and expensive compute, mathematics starts to look less like a pen-and-paper discipline and more like an experimental science with gated instruments. That raises concentration risk for universities, countries, and independent researchers. The overall mood was not anti-AI. It was anti-handwaving. People mostly accepted that AI will become a serious tool for proof search, formalization, and routine mathematical labor. They were much less willing to accept marketing claims that this automatically advances mathematics in the richer human sense, or that current systems are autonomous enough to deserve oracle status.