AI in mathematics is forcing big questions

Role of AI in Mathematics

• AI is seen variously as tool, collaborator, and possible “oracle”; many argue all three roles will coexist.
• Current strengths: speeding up search, exploring cases, suggesting steps, formalizing and verifying existing ideas.
• Weaknesses: difficulty generating genuinely new ideas or big conceptual leaps; some argue recent AI “breakthroughs” mostly repackage known techniques.
• Several note that, like with code, you must already be strong in the area to reliably judge AI’s mathematical output.

Verification, Proof Assistants, and Trust

• A core theme: distinction between generating proofs and checking them.
• Proof assistants (e.g., Lean) can give very high confidence once a statement is correctly formalized; “it compiles or it doesn’t.”
• However, you must still trust the theorem statement, the axioms, and the implementation of the kernel, plus the whole software/hardware stack.
• Debate over whether “proofs for proofs” make sense; many emphasize correctness vs understanding as separate issues.

Understanding vs Usefulness of Proofs

• Large auto-generated formal proofs (e.g., 200k lines of Lean) raise questions:
  • Pro: if the theorem is formally proved, that’s enough; the theorem itself is the API.
  • Con: opaque blobs are like binaries without source—hard to reuse, extend, or learn from; math is valued for insight, structure, and techniques, not only answers.
• Some argue non‑intelligible but correct proofs can still be practically useful (e.g., cryptography, engineering). Others see this as eroding the point of mathematics.

Impact on Practice and Profession

• AI may not fix the long‑complex‑proof bottleneck; verification still takes effort unless fully formal.
• Likely near‑term role: assistant for busywork (formalization, Latex, local refactors), not replacement of human creativity.
• Concern that human mathematicians could become “priests to oracles,” merely interpreting AI results, seen by some as anti‑enlightenment.

Philosophical and Social Concerns

• Ongoing debate: math as discovered vs created; aesthetic choice of axioms and “interesting” theorems remains human.
• Some believe useful mathematics may outstrip human intelligibility; others fear a “tech‑priest” future where we rely on incomprehensible systems.
• Access and equity worries: powerful models are proprietary and expensive, potentially turning math into an elitist, resource‑intensive field like experimental physics, worsening existing inequalities.