4 ms·

While I do agree that mathematics are not limited by what either of us can conceive, there is a fundamental barrier in understanding that one may not be able to

While I do agree that mathematics are not limited by what either of us can conceive, there is a fundamental barrier in understanding that one may not be able to process due to sheer volume. A trivial example here, though a bit absurd, is 15000 page long proofs, or machine generated proofs that span hundreds of pages. It is one thing to conceive of something new, and another to fully grasp all that we have built as a species. Certain pieces of work required hundreds of mathematicians to verify, which to me suggests that we have hit the limit of what our brains can do.

auggierose 4y ago
The proof of the Kepler conjecture has been formalised, because the original proof was just too large and contained computer calculations that mathematicians could obviously not verify just with their brains in any amount of time. So what? The high-level structure of the proof is quite understandable, and the statement of the Kepler conjecture is very easy to understand as well. What I am saying is that understanding something does not necessarily mean you understand it in all of its details down to the lowest level. And machines can help us understand the things we need to understand. But even with machines we will never understand everything in all of its detail down to the lowest level. We won't even know all the theorems of something as simple as Peano arithmetic. What you can do is not limited to what you can do without machine help, and just with your brain. I would say what we can do now will pale to what we will be able to do in the future, but of course this is speculation.