I think you have it backwards-- formalization is tedious and seldom yields insight.

It's the kind of low yield completionist task that you just don't do without something equivalent to cheap slave labor.

AI makes formalization more accessible and makes it more important: The current superpower of LLM powered research is that the LLM is absolutely relentless, but the relentless is a liability without a source of truth to check against.