[maest]

A nuance here is that you are assuming the existence of a solution. It may be the case there are no values for A to J that can result in that equation.

Iterating through all possibilities shows that the solution exists, the proof in the tweet doesn't.

[johnday]

The proof in the tweet gives steps to getting a solution, and the solution works. In what way is that not showing that the solution exists?

[Jeff_Brown]

The tweet only shows what J is, conditional on that there is a solution.

[quchen]

Isn't that exactly how any constructive proof works?

[DinnerAtEight]

Consider the following problem:

         ABC
         DEF
       + GHI
  ----------
   12300000J

where each letter represents a unique digit. The logic in the tweet would give the same value for J as the original problem, but in this case there is no solution.

[yodsanklai]

A constructive proof would exhibit a solution.

In that case, it has been shown that if a solution exists, it must be that J=6. With this additional information, you can try and find the other digit and conclude the proof (or in the case there's no solution, reach a contradiction).

I don't know how this type of proof is called in English but it's quite common. First come up with necessary conditions on your potential solution, and then you use these conditions to build an actual solution.

[Jeff_Brown]

I suppose it depends on your definitions, but most constructive proofs construct an entire solution -- that is, leaving no variables free unless the solution applies to any value of them. This only solves for J assuming the others can be solved for.

[antognini]

Yes, this is a good point. I wonder whether there is a proof to show that a solution exists that doesn't involve brute force.