Terence mentions how AI can potentially assist with finding mathematical proofs in the last few slides, but I wonder what his thoughts are on going the opposite

Terence mentions how AI can potentially assist with finding mathematical proofs in the last few slides, but I wonder what his thoughts are on going the opposite direction, i.e., using mathematics to accelerate the development of AI. If we consider Levin search to be the “brute-force” approach to universal search, then Hutter search improves upon this by interleaving the search of algorithm/program space with a search of the space of formal mathematical proofs to find proofs of algorithmic equivalence, whereby we substitute the slower running algorithm with its faster equivalent. But can we do even better? Terence touches upon automated theorem proving, which to some degree formalizes the notion of searching proof space. Once formalized, this becomes its own area of mathematics, where now the goal is to find proofs of the fastest ways to search the subset of proofs relevant to fast proof-finding. It’s always been a bit odd to me that we defaulted to considering probabilistic approaches to universal search rather than mathematical ones; these are all mathematical structures at the core of it after all, so I would think deduction would be much more effective than induction in this domain. But then again, who knows—GPT seems to be quickly getting better at providing novel intuitive ideas to explore. And I guess induction is actually kind of necessary when determining which potential path of deduction to explore. Another question is whether there exist algorithms that are the most efficient at solving particular classes of problems but unprovably so within any reasonable formal system, in which case automated theorem proving wouldn’t help. I kind of doubt it though. And in that case, brute-force search certainly isn’t going to find those algorithms either, so they may as well not exist within our “lightcone” of reachable algorithms that could be used to accelerate universal search. The only exception would be if these algorithms do exist and are actually dense in program space—in that case I suppose you would then have to optimize the balance of time spent between searching proof space and algorithm space. Again, I would intuitively think this possibility is highly unlikely, and so we should instead spend all of our time on improving machine assisted proof systems if we want to accelerate AI development via improvements to universal search.