Completely agree about the machines. Many mathematical results become more rigorous as a result of "can be done on this kind of machine" type of proofs. However

Completely agree about the machines. Many mathematical results become more rigorous as a result of "can be done on this kind of machine" type of proofs. However, if the goal is getting rid of intuition, machines don't help! Because no matter what the machine (bucket of pebbles or a Buchholz hydra), it takes a lot of intuition to prove, that particular machine correctly enforces intended rules. Usually more intuition, than the original problem. Without having proof for the machine itself that machine is declared axiomatic. It is a valid way to go about things of course, but I would hesitate calling it "not requiring intuition".