Comment by minkowski

Probably not since LLMs can now carry out very large formalizations (https://www.anthropic.com/research/formalizing-fermats-last-...).