Maybe "reducible" was the wrong word to use here. I'm a passionate believer in formal proof. I recognise the arguements about both the unreliability of formal and/or computer assisted proof and I can see that the incomprehensibility of many formal proofs makes them of questionable use to the practice of mathematics. However I do believe there is a value in reliability, in and of itself, and that formal computer-assisted proofs provide a better guarantee of reliability than normal mathematical practice. This is completely beside your point but its my interest in "reducibility" or perhaps "representability" stems from this direction. Human reasoning and discovery would appear to happen at the diagramatic level in these cases, converting this to logic is, as you say, a discovery but is useful for generating correctness, even if this is by non-human-like processes.
It wouldn't surprise me if non-Turing, particularly analogue, devices or add-ons turned out to be necessary for reasoning in some cases, especially since there are many problems which are solved more easily by physical interaction with the real world than by simulation (all those boundary detection problems), but my gut feeling is that you didn't present any of those. I'd be surprised if the problems you presented were not amenable to solution by a Turing machine reasoning with the right representation.
Re: The slides for the talk (still developing) are available online
Maybe "reducible" was the wrong word to use here. I'm a passionate believer in formal proof. I recognise the arguements about both the unreliability of formal and/or computer assisted proof and I can see that the incomprehensibility of many formal proofs makes them of questionable use to the practice of mathematics. However I do believe there is a value in reliability, in and of itself, and that formal computer-assisted proofs provide a better guarantee of reliability than normal mathematical practice. This is completely beside your point but its my interest in "reducibility" or perhaps "representability" stems from this direction. Human reasoning and discovery would appear to happen at the diagramatic level in these cases, converting this to logic is, as you say, a discovery but is useful for generating correctness, even if this is by non-human-like processes.
It wouldn't surprise me if non-Turing, particularly analogue, devices or add-ons turned out to be necessary for reasoning in some cases, especially since there are many problems which are solved more easily by physical interaction with the real world than by simulation (all those boundary detection problems), but my gut feeling is that you didn't present any of those. I'd be surprised if the problems you presented were not amenable to solution by a Turing machine reasoning with the right representation.