A proper disproof disallows any instance. If I disprove that bachelors are married, you can be sure there are no married bachelors. If I prove Hume's guillotine, you can be sure there are no moral facts. If I disprove nonexistence, then existence definitely exists; there are no instances of nonexistence.
While = true.
This program doesn't halt. Proof by inspection.
Whoops. How can there be no general algorithm to determine if a program halts if every particular program has a particular proof? What do you think a general algorithm is except the most compressed version of [every particular poof]?
Do you remember the six simple machines? The ramp, the screw, the pulley, the lever, etc? In reality, computer programs likewise have a set of simple digital machines. Some of their relationships result in non-halting, and you can just list these relationships if you want, because there's like six simple machines and thus like 15 binary relationships between machines,
Sure halting is likely NP-complete, but you can just brute force it, the same way you solve a travelling salesman problem. If the trinary relationships matter, I think there's 90 of them. Goes up quick. Still finite though. (Plus the designer can control this. If you haven't checked a relationship for halting yet, don't use it.)
Second empirical disproof: physics is a formal system. Here's my algorithm to determine if a program halts: run it and see what happens. How does physics know whether physics halts or not? Physics has to run an algorithm, because physics is simply the greatest algorithm. Turing's proof should demonstrate that physics itself doesn't know whether a program will halt or not. (Ref: uncertainty principle.) All programs should enter an incollapsible superposition of both halting and not-halting. In reality all programs that halt in under t hours will be proven to halt by running them until time t.
Godel's and Turing's proofs are isomorphic. They both commit a grammatical solecism. They are not valid.
The actual form is basically [G = G is not provable]. This would mean [G = G is provable] is also grammatically allowed. Or [G = G is true = is true]. [3 = 3 is true] = is true, 3 = G = 2 = 0. You also can't prove or disprove 3 = +, because + is an operator, not a number. If 3 = + then 9 + 2 = 9  2. If 3 != +, then some number does, and you get the same nonsense. 3 = = amuses me more, to be fair. 9 + 2  11.The equation is just malformed, like 3/0 = ?.
"True" isn't a number, it's a meta-property. Get this: [system + ε] has elements that are non-provable using only [system]. Amazing. Stating things about [system + ε] without using ε is inconsistent. Inconceivable.
Bonus round: every program halts. Are you watching? Look ma, no brain: it's called the second law of thermodynamics. The machine is itself a program which is running your explicit program as a proper subset, and the machine is going to break down. The program halts at t < ∞, for all programs.
Reminder that Godel numbers are absolute genius brilliance, which is presumably why nobody talks about them and fewer use them. See also: Xeno was likely the best philosopher after Socrates, yet he's considered a footnote.
P.S. Speaking of doing things the easy* way rather than the hard way, rather than trying to use (n-1)n/2 with odd numbers, you can remember it's equivalent to n * (n/2-0.5). [5 => 5 * 2]. [9 => 9 * 4]. Etc. This formula always has an integer-only form as long as n is an integer.
Really, why would you factor out the n/2 instead of the n/1? WTF?
Technically the formula is n!/2(n-2)! ( n=5 => 120 / 2*6 ) you could use that instead if you wanted...
*In the above case, the possible way instead of the impossible way.