> LLMs have done nothing for "making large scale mechanization viable."

I'm sorry, but this assertion is ridiculous. LLMs absolutely have radically simplified mechanization. Autoformalization of papers using LLM is orders of magnitude faster than doing it manually.

To quote Ken Buzzard (of the Xena Project):

https://xenaproject.wordpress.com/2026/07/20/human-mathemati...

> [...] Sol had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project. Lean’s fantastic (declaration of conflict of interest: I am a maintainer) mathematics library mathlib is only 2.3 million lines of code, and took nine years to write.

LLMs are going to be the basis of total formalization of all ~4M papers in the historical math literature. This project wouldn't be feasible without them.