well lean systems might be still useful for other stuff than max benching

my point being transformers and llms have all the tailwind of all the infra+lateral discoveries/improvements being put into them.

does that mean they're the one tool to unlock machine intelligence? I dunno

I think formal systems like Lean are still extremely interesting. And I would imagine that, if these machines get good at standard "informal" proofs, that the overhead of formalization would be a lot less painful for them than humans (it is pretty tedious these days but even for humans the friction is decreasing).

Verified proofs allow you to collaborate with much less trust (for humans or machines), at least in the phase where you are trying to figure out what is true. They don't guarantee that a proof is insightful for "why" a result is true, but that is much easier to put together once you have a valid proof.