Are there programs that never halt and have no non-termination proof?

Like black holes in computer science. We can only know they exist but when we have one of them we will never know it's one of them.

There are indeed programs like this. To prove this, let's suppose to the contrary that for every machine that doesn't halt, there is a proof it doesn't halt.

These proofs are strings of finite length, so we can enumerate all proofs of length less than $s$ for some integer $s$.

We can then use this to solve the halting problem as follows:
Given a Turing Machine $M$ and an input $x$, we use the following algorithm:

s := 0
while (True)
    test if machine M halts on input x in s steps
    look at all proofs of length s and see if they prove M doesn't halt on input x
    set s := s + 1

If $M$ halts on input $x$, then it halts in some finite number of steps $s$, so our algorithm terminates.

If $M$ doesn't halt on input $x$, then by our assumption, there's some proof length $s$ where there's a proof that $M$ doesn't halt. So in this case, our algorithm always terminates.

Thus, we have an algorithm deciding the Halting problem which always terminates. But we know this cannot exist, so our assumption that there's always a proof of non-halting must be false.

StackExchange Computer Science Q#35637, answer score: 23