Why can humans solve certain "undecidable" problems?

High-order pattern matching is an undecidable problem. That means there is no algorithm that, given an equation a => b, where a and b are open terms on the simply typed lambda calculus, finds a substitution S such that aS => bS, where => stands for "has the same Bn normal form". Yet, humans can solve that problem efficiently. For example, given the following problem:

a = (λt . t 
    (F (λ f x . (f (f (f x))))) 
    (F (λ f x . (f (f x)))))
b = (λ t . t
    (λ f x . (f (f (f (f (f (f x)))))))
    (λ f x . (f (f (f (f x))))))

Any human with sufficient knowledge on the lambda calculus will be able to notice F is the "double" function for church numbers, quickly coming with the solution that

F = (λ a b c . (a b (a b c)))

My question is: if that problem is undecidable, how can humans quickly and effortlessly solve it?

Humans can solve some instances of that problem efficiently, but there is no reason to believe that humans can solve all instances efficiently. Showing one instance that a human can solve efficiently does not imply that humans can solve all instances efficiently.

Undecidable means "there is no algorithm that can solve all instances and that always terminates". There could still be an algorithm that can solve some instances, even for an undecidable problem.

So there is no contradiction.

StackExchange Computer Science Q#47712, answer score: 88