Post #2920372

@tao@mathstodon.xyz The recent disproof of Open AI of the Unit Distance Conjecture contains commentary strangely relevant to the above discussion from Timothy Gowers. In footnote 4 he mentions theory building, definitions, and questions as things that he suspects AI will soon become good at, so I wanted to comment again. The specific problem is that we have absolutely no palatable methods of objectively measuring quality in these areas. So, I think to claim that an AI will get good at these areas ignores the major gap in our knowledge of what 'good' means, a gap I am not sure we can computably close. E.g. when it comes to theory building, theories relating to logic and set theory can not be computably shown to be true or false. For example, some have argued that mathematical semantics should be non-well founded, that we should remove the axiom of foundation, and replace it with something like AFA. How does one measure the quality of such a claim? How does one measure the quality of Joel David Hamkin's Multi-verse theory against the alternatives? How does one measure the quality of the Univalance axiom in Homotopy Type Theory? If proofs become cheap, then mathematics will stop being about proofs, and become more about truth. (I'd argue that this would be a return to form) The relevant question then is whether an AI can access truth in the same way that a human can. This kind of reasoning seems inherently higher order, which (under full semantics) does not yet have a reasonable notion of 'proof'. So, my worry is that without objective measures of progress in these 'second order' areas of truth and meaning, this discussion will stagnate and become dominated by politics, instead of whats right.