[FOM] News about Mochizuki's claimed proof of abc

[James Smith]

Hi,

> Confidence in the correctness of the proof arises when these ideas are 
> disseminated and digested and people are able to reconstruct the proof 
> for themselves. 

Exactly.

When proof assistants are at the point where you can simply click on a 
link and navigate through the entire proof in the way we can navigate 
the Internet via hyperlinks (taking it completely for granted); and the 
proof itself is modular with each module the result of the work of many 
collaborators and is both constantly questioned and refined, debates 
such as these will become a thing of the past (or what debate there is 
will be continued in the 'issues' of the module in question and there 
for all to see and participate in, even non-experts).

To focus on the foundational issues around FLT, or any other large or 
debatable proof for that matter, is to miss the point. The veracity of 
such proofs is down to things like common knowledge, collective 
understanding, etc. In short it is a sociological problem, not a 
theoretical one, and a problem that can simply be solved by better software.

The future for mathematics lies in structured and simplified proofs such 
Hales' blueprint proof and in giving mainstream mathematicians the means 
to digest them piecemeal at their own pace and in greater numbers. 
Abstraction means that no one or only a chosen few mathematicians have 
to have the final word just because they claim, or others claim on their 
behalf, that they understand an almost unimaginably complex proof, and 
all the issues (foundational or otherwise) that go with it, in its 
entirety. This is clearly an untenable situation.

Kind regards,

James