Comment by pfdietz
6 hours ago
> 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.
What is absurd is evaluating something on the lines of code it produces. AI psychosis at work.
That's some industrial strength denial you've got going there. Please entertain the possibility that people who are presenting reasoned arguments with evidence against you are not "psychotic". BTW, is Ken Buzzard also psychotic?
Anyway, this avalanche is going to come down on your head whether or not you believe in it. Have fun!