> I predict that in the future people will ditch LLMs in favor of AlphaGo style RL done on Lean syntax trees. These should be able to think on much larger timescales.

This is certainly my hope.

In my spare time, I'm slowly, very slowly, inching towards a prototype of something that could work like that.