I do not know about a conjecture, but I would like to mention the Ax–Grothendieck_theorem.
A very nice way of proof is to show that the (first-order) theory $ACF_0$ of algebraically closed fields with characteristic zero is complete (through quantifier elimination iirc).
Thus, if the statement is false, there is a “somewhat” equivalent (because of the number of variables and degree of polynomials) first-order statement the negation of which can be proved in $ACF_0$.
Since the proof has finite length, there exists some prime $p$ such that the assumption “$p \neq 0$” is not used in the proof. So that first-order statement never holds in any algebraically closed field with characteristic $p$.
It remains to prove that the Ax-Grothendieck theorem holds in the algebraic closure of $\mathbb{F}_p$ for each prime $p$.
In a nutshell, we actually disprove the existence of a general disproof in $ACF_0$ ; since $ACF_0$ is complete, this entails the existence of a proof.
More a reflection than an answer, but too long for a comment.
Your observation that
Apparently, most mathematical proofs of any kind of theorem are
"informal" and omit many logical rules of inference and argumentative
steps for the sake of conciseness.
is true. I think it should follow that starting an undergraduate text on discrete mathematics with formal logic - truth tables, rules of inference, quantification - only confuses students when they are then expected to construct convincing proofs using everyday clear thinking. They rightly wonder whether all that formality is necessary and ask questions like this one.
Of course it is necessary in other contexts - when studying logic, when designing programs to prove theorems - but not in introductory courses.
Edit, suggested by @Bram28 's excellent answer. Rosen's Universal Generalization that replaces "for all elements $x$ such that" by "let $x$ be an arbitrary element such that" is close to what is often called "proof by representative special case". Those are not proofs but tell you clearly how a formal (or informal) proof will work.
For (a toy) example, to prove that the square of an odd number is odd, look at what happens when you square $15$. The distributive law tells you
$$
15^2 = (2\times 7 + 1)^2 = 4 \times 49 + 2 \times (2\times 7) + 1
$$
which is the sum of two even numbers and $1$, hence odd. There was nothing special about $15$ in this argument - you can clearly see how it represents all odd numbers.
(Parenthetically, this example/proof suggests the even stronger theorem that the square of an odd number is congruent to $1$ modulo $4$.)
If you search for "representative special case" (with the quotation marks so that you get just links to the whole phrase) you find this from Hilbert:
The art of doing mathematics consists in finding that special case
which contains all the germs of generality.
(Example for Hilbert quote),
a quote from Polya , and other links worth following.
Best Answer
Edit: I see that Ian has already given this answer. Nevertheless, I'll leave this here because it offers more detail. This is the closest thing to a real-world application of an existence proof of which I am aware.
Numerical PDE have many applications in modeling physical problems and help us accomplish many engineering feats - for example, building a bridge or placing an oil rig in the ocean.
To be confident in the answers that these numerical methods produce, we must know that the equations involved are well-posed, meaning
1) the solution exists,
2) the solution is unique, and
3) the solution depends continuously on the data given.
If (1) isn't true, then the model is flawed. If (2) isn't true, then which solution are you converging to? If (3) isn't true, then your discretization of the problem may introduce significant errors.
So for numerical PDE to work (and their applications in engineering), non-constructive proofs of existence, uniqueness, and continuity are used.