The conjecture that formalizing more professional mathematics is the rate-limiting step for AI proof assistance

AI proof assistance refers to AI systems that help mathematicians develop and verify formal proofs, potentially by interacting with an interactive theorem prover. Formalization bottleneck conjecture. The current rate-limiting step for AI proof assistance is producing orders of magnitude more lines of formalized professional-level mathematics. The claim concerns the scale of available formal mathematical training data, which the source contrasts with the much larger datasets used to train modern language models; whether producing substantially more formalized mathematics is in fact the principal bottleneck remains open.