You've convinced me that I don't have conscious introspective access to the algorithms I use for these things. This doesn't mean that my brain isn't doing something pretty structured and formal underneath.

The formalization example I think is a good one. There's a famous book by George Polya, "how to solve it". It's effectively a list of mental tactics used in problem solving, especially mathematical problem solving.

When I sit down to solve a problem, like formalizing the natural numbers, I apply something like Polya's tool-set iteratively. "Have I formalized something similar before?" "Is there a simpler version I could start with?" and so forth. This is partly conscious and partly not -- but the fact that we don't have introspective access to the unconscious mind doesn't make it nonalgorithmic.

As I work, I periodically evaluate what I have. There's a black box in my head for "do I like this?" I don't know a lot about its internals, but that again isn't evidence for it being non-algorithmic. It's fairly deterministic. I have no reason to doubt that there's a Turing machine that simulates it.

Effectively, my algorithm for math works like this:

while(nothing else is a higher priority than this problem) { stare at the problem and try to understand it search my past memories for something related // neural nets are good at this for each relevant past memory, try to apply a relevant technique that worked in the past evaluate the result. if it looks like progress declare this to be the new version of the problem

}

Seems algorithmic to me!