Is it possible that “A counter-example exists but it cannot be found”

A standard example of this is the halting problem, which states essentially:

There is no program which can always determine whether another program will eventually terminate.

Thus there must be some program which does not terminate, but no proof that it does not terminate exists. Otherwise for any program, we could run the program and at the same time search for a proof that it does not terminate, and either the program would eventually terminate or we would find such a proof.

To match the phrasing of your question, this means that the statement:

If a program does not terminate, there is some proof of this fact.

is false, but no counterexample can be found.

I actually like this one:

There are uncountably many real numbers. However, given that all specifications of specific real numbers (be it by digits, by an algorithm, or even a description of the number in plain English) is ultimately given by a finite string of finitely many symbols, there are only countably many descriptions of real numbers. Therefore almost every real number cannot be individually specified in any way. Therefore there exist uncountably many counterexamples to the claim "you can uniquely specify any real number".

Of course I cannot give a counterexample, because to give a counterexample, I'd have to specify an individual real number violating the claim, but if I could specify it, it would not violate the claim and therefore not be a counterexample.

Yes. For instance,

There exists a non-measurable subset of $\mathbb{R}$ (with respect to Lebesgue measure).

It requires the axiom of choice; so we could claim that it can't really be found. Any non-constructive proof would be another possible answer. See Wikipedia on constructive proofs.

Note the interesting, related question on MO: Are there non-constructive existence proofs without the axiom of choice?

The question has a bit of ambiguity in it.

What does it mean that a counterexample cannot be found? What does it mean to find something in mathematics?

We might want to talk about purely physical computation (by which I mean using our current technology and reasonably conservative projections thereof; not some hypothetical future in which we have new theorems, algorithms and hardware capable of factoring prime numbers larger than the volume of the observable universe instantly). In this case the word "find" means also verify without any doubt, as well.

In this case we can easily make claims like "Every prime number larger than $2^{2^{100000000000}}$ is of the form $2^n-1$". Of course we can prove that there exists a prime number larger than $2^{2^{100000000000}}$ which is not a Mersenne prime, but computationally speaking verifying that a number which is not a Mersenne prime is prime, is an immensely difficult task.

If the above feels a bit wide, you can also plug in all the other "relatively easily verifiable prime" into the list above. The point in the above example is that there is no efficient way of verifying whether or not a certain number is prime or not; and so to verify whether or not an arbitrary number larger than $2^{2^{100000000000}}$ is a prime number, we are expected to run a very lengthy computation. We can replace "prime number" by "solution to sufficiently complicated problem" just as well.

In contrast, we can easily verify if a given number is even or not. We just need to check one bit of its binary representation (or one digit of a decimal, or hexadecimal representation), or any other "sufficiently simple problem".

If we talk about theoretically computation, it depends on what do you mean prove that a counterexample exists. In particular what do you mean by "prove"? More specifically, prove from what theory?

From $\sf PA$, the axioms of Peano arithmetic, we can develop a nice theory of computation and computability, and we can prove that many natural problems that can be solved, but not in a computable way. For example the ability to decide whether or not a sentence is true or false in the natural numbers.

In this context the term "supercomputer" can be interpreted, perhaps, as an oracle, or more specifically some "additional" function[s] that work in a way we don't necessarily know, and this helps us to solve problems that we couldn't solve before. But even then, we can prove there are always statements that are not computable (now in this stronger sense), but are provably false, so we can't "find" a counterexample.

We can extend this to mathematical questions that we can prove existence of certain objects, without our ability to give an explicit construction (read: definition) of an example. For this we usually move one up a notch and use set theory as our theory for the term "prove". Many objects, in particular infinite (and often uncountable) objects are researched in modern mathematics, and we can prove many things about these sets using an axiom known as the Axiom of Choice. This axiom is non-constructive in its nature, as it asserts the existence of certain objects, but doesn't provide us with a way to define them explicitly.

In this context we have so many examples. For example, the existence of non-measurable sets; a linear order of all the sets of sets of natural numbers; a free ultrafilter on the natural numbers.

To sign off this answer, let me point again, that this depends on what you mean "cannot be found" and what it means "prove to exist". In different contexts the answers will differ. And things which may be considered "definable" or considered "found" in one context might not be considered as such in another.

This answers your question, maybe in an indirect way. There are a lot of probabilistic proofs in which one proves only the existence of something without the possibility of finding it.

For example, in information theory, the random coding argument is used to show that there is a code which is capacity achieving however we really cannot find any specific code using the argument. Capacity achieving codes were discovered only recently.

There are two opposite answers, both correct on their own terms.

One is that in most situations that have distinct concepts of "finding an example" and "existence of an example", for which finding an example always implies an example exists (but no assumption is made about the reverse implication being valid or not in general), concrete instances can be shown where something "exists" but cannot be "found". For example:

• seeing a dead body in some unusual place and circumstance, it might be easy to demonstrate with at least 99.9% certainty that there exists a murderer of that person, but finding the murderer with 99.9% certainty of the identification is far more difficult both logically and practically.

• a prime factorization of a large number "exists", in the sense that theories of arithmetic have that statement and its generalizations as provable theorems, but one might not be able to "find" the prime factorization if that means writing it down, or computing it efficiently, from the description of the number. Tables of factorizations of special large numbers (such as Mersenne numbers, repunits, Fibonaccis, etc) include entries like C307 to mean a 307-digit factor that is known to be composite number but without a known factorization.

• there "exists" a first-player win in finite two-player games such as $30 \times 30$ Tic Tac Toe or Chomp that are amenable to strategy-stealing arguments, but the resources to "find" and describe the winning strategy are vast compared to the resources needed to find the existence proof, and the strategy is not known.

• there "exists" an optimal strategy for chess, or any finite two-player game with rules that forbid unlimited repetition of positions, but to "find" the strategy requires impossibly large resources compared to what is needed to show "existence".

• the "exists" a shortest length of LISP computer code that will print out the Baghavadad Gita, but if that length is more than $1000$, no proof system that currently exists, such as formalized Zermelo-Fraenkel set theory, could "find" that program. Doing so would require writing down a program code, proving that it works by running it until termination, and a proof that the program is minimal-length, but no such proof exists in the proof system.

The other point of view, which is approximately the "intuitionist" or "constructivist" position, is that:

• the idea of existence proofs without any power to construct examples, is meaningless, and

• any healthy notion of proof will either define existence proof to mean finding an example, or have the property that an abstract existence proof can always be materialized into a proof that a specific example exists (e.g., Numerical Existence Property in intuitionistic proof systems).

In the finite examples, the supposed separation appears when there is an ability to efficiently describe and operate upon elements of a data structure (such as the positions and moves in the game tree of chess), and then extrapolating from that to an imaginary superpower to exhaustively search through the whole structure, and larger structures constructed from it (such as the space of strategies for black and for white). The problem in the infinite case is similar, where it is assumed that one can casually perform an infinite search to decide questions such as whether there "exists" a largest Fermat prime. If you reject the extrapolated abilities as no more than a pleasant fairy tale, it makes sense to reject the distinction between existence and the ability to find witnesses.

The busy beaver function has many opportunities for this sort of thing. 'In an axiomatic system of ordinary mathematics, there is a true-but-unprovable sentence of the form "Σ(10↑↑10) = n", and there are infinitely many true-but-unprovable sentences of the form "Σ(10↑↑10) < n".'

So, for the description "a counter-example exists but it cannot be found", the equality with $n$ in the quotation is such a counterexample. And it "cannot be found" in the strong sense that has been discussed in the other answers -- the counterexample exists (it's just some number) but even if you had some finite, "useful" (This word in this context baffles me.) representation of that number, you would not be able to prove the equality. This $n$ would be the greatest counterexample to the inequality with $n$ above.