Let me tell you a theorem whose proof is so long you couldn't fit it in the observable Universe if you wrote one symbol on every electron, proton and neutron available. In fact.... (to be continued)pic.twitter.com/Uq93Exq27f
You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
Hales’ original proof of the Kepler conjecture (on densest packing of space by sphere) took a hundred pages of writing together with about 3 gigabytes of computer calculations. If we wrote out those calculations in a text file, they’d fill about 2 million pages!
Which, of course and alas, leaves completely open the question of whether some shorter proof may exist. Still, it is surely a sobering, cautionary example.
We could now add the Kepler conjecture to our favorite axioms for math as an extra axiom, and considerably shorten Hales' proof. But this feels like "cheating" - and proving the new axiom system is equivalent to the original one would take a long time.
Yes. So the real (extremely subtle) question is, what axiom should we adopt, to ensure the existence of a proof of reasonable length, without "cheating"? If the shortest proof now really is so long, then we need new axioms. But we want our proofs to teach us something. Tricky.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.