Two things come to mind: 1. There are non-constructive proofs, ie proofs that show that something exists, but do not provide an example (but rather derive a co

Two things come to mind: 1. There are non-constructive proofs, ie proofs that show that something exists, but do not provide an example (but rather derive a contradiction from the assumption that it doesn't exist, for example). Those are not really akin to running code. The Banach-Tarski paradox is a particularly striking example: You can decompose a ball into 5 pieces and reassemble them into 2 balls of the same size of the original. https://en.wikipedia.org/wiki/Constructive_proof https://en.wikipedia.org/wiki/Constructive_proof https://en.wikipedia.org/wiki/Banach–Tarski_paradox https://en.wikipedia.org/wiki/Banach–Tarski_paradox 2. Don Knuth famously sent a colleague some code with the warning "Beware of bugs in the above code; I have only proved it correct, not tried it." https://www-cs-faculty.stanford.edu/~knuth/faq.html https://www-cs-faculty.stanford.edu/~knuth/faq.html