The NN is providing advice to it. Any machine learning system could provide heuristics to a theorem prover.

I don't think this is a meaningful distinction. The system requires NN for top performance. Would you say that AlphaGo doesn't show NNs can play Go because 'really, it's the tree search which is doing the Go playing, all the CNN is doing is providing advice to it'?

I would stand by my original statement - if you actually read through these papers they do demonstrate the amount of acrobatics that has to be done to join the world of neural networks to anything discrete like programming or proofs.

Explain again how working NN systems delivering results, sometimes better than previous approaches, despite minimal research effort so far, shows that 'neural networks (deep or shallow) are hopelessly unsuited to programming and mathematics.'

This must be some new and novel definition of 'hopeless', I am hitherto unfamiliar with, where it now means not 'nearly impossible' but 'possible and already done sometimes' As a descriptivist, I of course must move with the times and try to understand new uses of old words, and so I don't object to this use, but I do want to be sure I am understanding you correctly.