Is it possible to prove by enumeration or other means that there cannot be a formal proof shorter than given length of a famous conjecture?
In particular, is it easy, given a formal proof of a conjecture determine that this proof is not a proof of the conjecture?
Does the difficulty depend on the conjecture in question?
On
Proof by counterexample:
In a curious turn of events, British biogerontologist Aubrey de Grey, a well-known author and Chief Science Officer of the SENS Research Foundation, which is devoted to “reversing the negative effects of aging” and “significantly extending the human lifespan,” has made a significant advance in a 60-year-old graph theory problem.
Needless to say, in this day and age when almost all frontier-level mathematical research requires substantial training and, regrettably, specialization, it is not very often that an person without graduate-level formal training in mathematics, and whose professional life is focused almost entirely in a completely different field, makes a notable advance in the mathematics. One struggles to think of any other comparable example, or even an apt analogy: A Silicon Valley CEO who discovers a new species of hominin fossils? A Wall Street quant mathematician who publishes a key advance in biogenesis? In this light, de Grey’s paper The chromatic number of the plane is at least 5 is even more remarkable.
de Grey is not a complete stranger to graph theory. Several decades ago, de Grey was an avid player of “Othello” (a computer-based version of Reversi). In the process he befriended some mathematicians, who in turn introduced him to graph theory. de Grey still works on graph theory from time to time: “Occasionally, when I need a rest from my real job, I’ll think about math” (see this Quanta article for more details). Still, his latest achievement is pretty impressive.
It depends on what you mean by possible. Given a proof, one could theoretically list all strings shorter than the proof and check if they prove the theorem. Most of them will be gibberish, so fail to be a proof for that reason. The number of such strings is finite, so the answer would be available in a finite amount of time. For any reasonable length of proof that finite amount of time is unreasonably long, so one cannot practically do this. This argument does not depend on what is being proved, nor on the axioms being used.