1/ Fascinating report by a world leading mathematician, P Scholze, on an open source project to use 'proof assistants' on an important maths proof. Byproduct = the computer improved human understanding. Seems clear these tools will play ever greater role xenaproject.wordpress.com/2021/06/05/hal…
2/ Concept of 'proof assistants' goes back to e.g Hilbert's 1900 question on the possibility of automating maths & Gödel's 1931 proof re incompleteness/undecidability. I got very interested in this history & wrote about it here: dominiccummings.com/2017/06/16/com…
3/ Almost everything you read re Gödel is wrong. Franzen wrote a brilliant book explaining all the misconceptions: 
4/
5/ When Gödel first read out his famous result, nobody understood what he was on about - except a very young von Neumann who went to talk to him after the talk...
6/ Gödel summarised the effect of the combination of his & Turing's 1936 proof:
7/ This work led Gödel to formulate the P=NP? problem, central to the potential for 'proof assistants', but it was in an unreported letter to von Neumman as latter lay dying of cancer. It took ~15 years for the problem to be rediscovered rjlipton.wpcomstaging.com/the-gdel-lette…
• • •
Missing some Tweet in this thread? You can try to
force a refresh
