Mathematical Abundance

Mathematical abundance is Hong Letong / 洪乐潼’s vision in 137. 对洪乐潼的4小时访谈：AI for Math、把数学变成Lean、数学天书中的证明、直觉、被创造与被发现的 that AI can move society from being math-poor to math-rich. If proof, conjecture, formalization, and verification become much cheaper, mathematical discovery can expand in volume and feed more theory into science, engineering, software, and hardware.

Key Claims

• The bottleneck can shift from proving individual theorems to choosing which problems deserve attention, compute, and human interpretation.
• Human mathematicians become more like research directors, benchmark designers, and taste-bearing collaborators when proof supply expands.
• The episode compares this to a “fold everything” mindset after AlphaFold: if the marginal cost of solving a class of problems falls, the rational scope of curiosity can expand.
• Abundance does not remove mathematical culture; Hong argues that human community, taste, collaboration, and new questions remain part of mathematics.

Connections

• AI For Math, AI Mathematician, Axiom, and Axiom Prover — systems that could create this abundance.
• AI For Science, Discovery Model, and Research Taste — domains and human judgment that determine whether abundant results matter.
• Formal Verification and AI Coding Verification — applied branches where abundant proof can become commercial value.