Comment by PowerElectronix

Just like in chess, at some point the problem at hand and its solution becomes so unwieldidly complex that you either make of it the work of your life or you use a math/chess engine to handle the complex stuff.

Just like you can find a forced mate in 120 moves for a given position, you can find a 120 pages of pure gibberish demonstration of some conjecture with its lean check.

The thing is to not become reliant on it and just cheer it up so it makes progress on its own in the Riemann hypothesis, but to use it like a lever to lift heavier stuff, as Dr. Tao does here.