All things considered, the proof is pretty short! It’s 19,000 lines of Coq (including white space and comments). And in my experience, if this were compiled into a traditional paper it would be significantly shorter than the Coq version. (Of course, length of the proof really isn’t a measure of difficulty or complexity, but it is a very rough yardstick we can use.)
When talking about the limits of human knowledge, I often think about the theorems that are provable, but so complex that no human being could understand them. Probably the most complex proof we have is the classification of finite simple groups, which is thousands upon thousands of pages, and there is probably very few or no people on Earth that fully understand all of it.
As the article suggests, BB(6) could be undecidable. But it could also have a proof millions of pages long, beyond the reach of humanity.
When talking about the limits of human knowledge, I often think about the theorems that are provable, but so complex that no human being could understand them. Probably the most complex proof we have is the classification of finite simple groups, which is thousands upon thousands of pages, and there is probably very few or no people on Earth that fully understand all of it.
As the article suggests, BB(6) could be undecidable. But it could also have a proof millions of pages long, beyond the reach of humanity.