[HN Gopher] Formalising modern research mathematics in real time
       ___________________________________________________________________
        
       Formalising modern research mathematics in real time
        
       Author : mauricioc
       Score  : 79 points
       Date   : 2023-11-05 12:25 UTC (2 days ago)
        
 (HTM) web link (xenaproject.wordpress.com)
 (TXT) w3m dump (xenaproject.wordpress.com)
        
       | tezthenerd wrote:
       | If you want to see this kind of thing done "really in real time"
       | check out Terry Tao's recent mathstodon posts where he learns
       | Lean while formalizing a paper of his own. Fascinating stuff.
        
       | n4r9 wrote:
       | Cool to see the mention of Andrew Thomason! He was my
       | supervisor/tutor for several undergrad courses, as well as
       | lecturing a couple of the courses I took over the years. He had a
       | brilliant Yorkshire accent, and if I remember rightly he enjoyed
       | eating Walkers crisps and making good use of Fellows' privilege
       | to ride their bike on college grounds. I actually had no idea
       | that he had a seminal result on Ramsey numbers, and in the same
       | year I was born no less.
        
       | dunham wrote:
       | The guy behind the xena project, Kevin Buzzard, recently got a
       | grant to formalize Wiles' proof of Fermat's theorem in Lean4:
       | https://mathstodon.xyz/@xenaproject/111170563403967905
        
       | V1ndaar wrote:
       | > An obvious question when formalising a maths paper is how much
       | the proof needed to change to be formalised: in other words
       | whether there were any flaws in the paper. This question is
       | surprisingly subtle, but a simple summary is that most of the
       | mistakes I identified were easily fixable. Importantly all
       | mistakes were fixable in a way that preserved the spirit of the
       | argument, so the Lean version of the proof can reasonably be said
       | to be a translation of the informal proof.
       | 
       | > I like to consider certain such small mistakes "mathematical
       | typos". It's fair to call them errors, and just like typos in
       | English prose can confuse a non-native speaker, mathematical
       | typos can impede meaning for a reader who isn't familiar with
       | mathematics. However, with a little experience, it's not hard to
       | see what the intended meaning was, and fixing it isn't too bad. A
       | mathematical typo certainly doesn't constitute a flaw in the
       | proof, and almost all the problems I found fall in this category.
       | 
       | If only we had better ways to distribute fixes to papers. These
       | kind of issues happen all the time and unlike in code where
       | someone can just come in and provide a fix, these usually remain
       | forever in papers. Yes, some publish errata or upload a new
       | version to the arxiv, but the majority remain as a form of
       | horrendous "exercise for the reader". If I'm an expert in a field
       | I may quickly notice such issues, but more often than not I won't
       | spend the time required to do so. And hence I probably propagate
       | wrong information myself / wonder why my numerical calculations
       | don't produce the correct result etc.
       | 
       | It is especially bad when branching out into areas somewhat out
       | of your area. The amount of mistakes and utterly wrong
       | information I had to deal with just in the last few months thanks
       | to papers being sloppy is just sad. So much time wasted. :( (I'm
       | a physicist)
        
       ___________________________________________________________________
       (page generated 2023-11-07 23:00 UTC)