Interestingly, SotA Lean provers use TTT, specifically AxiomMath, Kimina, and AlphaProof

I like this question

I think the definition of SotA will matter here. Since you can probably max out many of the benchmarks with normal training and some kind of memory module implemented with weight updates during testing may just be a bottleneck.