What is a direct proof, formally?

As Rob Arthan said in the comments, one way to distinguish between (one kind of) direct proof and indirect proof is simply to distinguish between proofs that use intuitionistically valid deductive rules and proofs that do not.

To show that there are some theorems (using classical logic) that have no intuitionistically valid proofs, it suffices to show that there is a way to interpret intuitionistic logic such that the intuitionistic deductive rules are sound for that interpretation, and also that there is a tautology of classical logic that is not a tautology under that interpretation. A popular one is LEM (i.e. $A∨¬A$), but it may not be convincing. Here is another:

$(A⇒B)∨(B⇒A)$.

You cannot prove this classical tautology in intuitionistic logic. In that precise sense there can be no direct proof of this tautology. This is more convincing than LEM because it is even slightly counter-intuitive and you really need to 'check cases' (relying on LEM) to prove it. Lest you think that 'checking cases' is direct, observe that every intuitionistic proof of ( $¬B⇒¬A$ ) can be translated to a proof that is intuitionistic except for a single LEM case-checking:

  If $A$:
    $B∨¬B$.
    If $B$:
      $B$.
    If $¬B$:
      [Insert proof of ( $¬B⇒¬A$ ) here.]
      $¬A$.
      Contradiction (i.e. $A,¬A$).
      $B$. [by explosion]
    $B$.
  $A⇒B$.

There are many interpretations of intuitionistic logic under which this classical tautology does not hold. One is Kripke frames (see here for a sketch), and another is the BHK interpretation. Understanding either of them will give you a clear idea of how exactly an intuitionistic proof can be considered to be 'direct'.

From wikipedia at https://en.wikipedia.org/wiki/Direct_proof

"In mathematics and logic, a direct proof is a way of showing the truth or falsehood of a given statement by a straightforward combination of established facts, usually axioms, existing lemmas and theorems, without making any further assumptions.In order to directly prove a conditional statement of the form "If p, then q", it suffices to consider the situations in which the statement p is true. Logical deduction is employed to reason from assumptions to conclusion."

This sentence "In order to directly prove a conditional statement of the form "If p, then q", it suffices to consider the situations in which the statement p is true.", is particularly important because it tells us that a direct proof only examines what happens if the hypothesis is true. A true hypothesis can't yield a false conclusion, so a direct proof doesn't examine false conclusions, either. However, an indirect proof examines what would happen if the conclusion were false for its proof.

I am not sure if there is any theorem that has been proven to have indirect proof, but here's an indirect proof of the irrationality of $\sqrt2$ as an example. https://www.math.utah.edu/~pa/math/q1.html