> They have used a proof generator based on a logical theory...
I don't understand your scenario. If they're using a proof generator, that sounds like the opposite of intuiting or using the human mind. Maybe they used "intuition" to come up with new axioms for a logical theory, but that is not the same as determining of some particular concrete TM program whether or not it halts.
You got it - the creative developments of a stronger theory. This allows the creation of tools which can categorize TMs, tools which wouldn’t exist otherwise.
It’s fascinating that the entire space of finite amounts of random gibberish contains every such stronger theory.
As a thought experiment it does well. Interestingly the Church-Turing thesis seems to exclude ingenuity. That is, it doesn’t try to say there aren’t functions on natural numbers which are uncomputable but can be calculated with ingenuity. Seems that a ton of people conflate those things.
I don't understand your scenario. If they're using a proof generator, that sounds like the opposite of intuiting or using the human mind. Maybe they used "intuition" to come up with new axioms for a logical theory, but that is not the same as determining of some particular concrete TM program whether or not it halts.