What is a “non-constructive proof”?

[Joe Shipman]

There are at least three kinds of “non-constructive proofs” that I have seen:
(1) A theorem that certain equations have finitely many solutions, with no bound given that would allow one to exhaustively search for them
(2) A theorem that a certain equation has a solution, with no bound given, but a guarantee that searching will eventually find one
(3) A counting argument that an object with certain properties of a certain size must exist, which comes with an implicit exponential bound on the search but no efficient construction.

Can people provide examples of each of these three types where the proof can be presented to undergraduate math majors, and where no improvement is known? (In other words, a nonconstructive proof of each type where no proof is known of an easier type.)

— JS

Sent from my iPhone