= 27d567bc2d48d9f40e9ccc20ea370b15)
magfrump comments on Logical uncertainty, kind of. A proposal, at least. - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (35)
Okay, but say the robot in ten seconds manages to prove the theorem: "For all dimensions n not equal to 4, there is exactly one smooth structure on R^n." But is unable to produce a result regarding n=4? Or more realistically, say it is able to construct 1 smooth structure on R^n for any n, and can prove that no others exist unless n=4. How does it make guesses in the case n=4?
If we want to live in the least convenient possible world assume that in second 1 it constructs the smooth structures; it takes three seconds to prove that there are no more for n>5, three seconds to prove no more for n=1,2, and three more seconds to prove there are no more for n=3 and runs out of time. These results are obtained incidentally from inequalities that arise when pursuing a proof for n=4, which is the central value of some equation at the core of the proofs. (so the proofs really say "if another smooth structure exists, it exists for n<5, 2<n<5, 3<n<5.")
If it really can't prove any theorems that directly include the translation of "the number of smooth structures for n=4 is," it simply won't ever update that.
Well it can prove "the number of structures for n=4 is at least 1."