This is definitely something that we'll be looking into more closely in the future. Our old and busted `gptf` tactic was a good start but we can do much better!
I may be misunderstanding, but it seems like gptf can only apply theorems from the set you guys trained it on ... in which case I don't see how it could possibly help with the development of a theory beyond its first few statements. Have I got that right? and if so is it something that might be addressed in future iterations?
How long (or how much compute resources) does it take to solve one of these IMO problems right now? My estimation is that just the time to run tactics linarith for many different cases would be significant enough to make it too slow to do interactively, but I'm curious to check my guess.
It takes a lot of CPU (lean side) on top of GPU (neural side) indeed. But technically, when properly parallelized, it takes no more than 1-2h to crack the hardest problem we've cracked so far.