| ▲ | leonidasrup 3 hours ago | |
Even Peter Scholz is not always sure of correctness of extremely complicated mathematical statements and welcomes computer assistance in verification of his results. See the Liquid tensor experiment: https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e... https://www.ma.imperial.ac.uk/~buzzard/xena/pdfs/liquid_tens... " I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. In the end, we were able to get an argument pinned down on paper, but I think nobody else has dared to look at the details of this, and so I still have some small lingering doubts. " In a sense, mathematics is not very different from software engineering. More precisely: Curry–Howard correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... | ||