from Hacker News

Formalising modern research mathematics in real time

by mauricioc on 11/5/23, 12:25 PM with 16 comments

  • by V1ndaar on 11/7/23, 10:50 PM

    > 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)

  • by tezthenerd on 11/7/23, 4:20 PM

    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.

  • by dunham on 11/7/23, 7:09 PM

    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

  • by n4r9 on 11/7/23, 4:40 PM

    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.

  • by abss on 11/8/23, 2:43 AM

    Math and most scientific output is equivalent to some sort of code (automated formal proofs, descriptions of classes of simulators or statistical models,etc) We could envision the tools and "programmming" languages for various domains to replace text articles with "code"

  • by Hugsun on 11/8/23, 12:21 AM

    Very interesting. I didn't understand the article's definition of Ramsey numbers until reading the first paragraph of the Ramsey's theorem Wikipedia page. At that point the article's definition became obvious. I think the usage of the word "find" was too informal to be legible.

  • by haltist on 11/8/23, 1:34 AM

    This would be a good application of AI, convert informal proofs into formal proofs for Lean or Coq.