Formalising modern research mathematics in real time
xenaproject.wordpress.com
Formalising modern research mathematics in real time
1–10 of 18 posts
Re: Formalising modern research mathematics in real time
#2If 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.
Re: Formalising modern research mathematics in real time
#3Cool 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.
Re: Formalising modern research mathematics in real time
#4The 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
Re: Formalising modern research mathematics in real time
#5> 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)
Re: Formalising modern research mathematics in real time
#6> 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 rea…
It's truly miserable and I share your sentiments completely. Unfortunately, I do not have the right words to express my sadness about the status quo; I am a mathematician who actually believes in the importance of the "mathematics edifice" as a service for society, present and future. Oh well.
Re: Formalising modern research mathematics in real time
#7Very 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.
Re: Formalising modern research mathematics in real time
#8> 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 rea…
It's truly miserable and I share your sentiments completely. Unfortunately, I do not have the right words to express my sadness about the status quo; I am a mathematician who actually believes in the importance of the "mathematics edifice" as a service for society, present and future. Oh well.
I don’t know if it’s recency bias or some other cognitive distortion on my part but I seem to be seeing more and more stories about Lean and formalizing mathematics recently. Perhaps the project is gaining some momentum!
Re: Formalising modern research mathematics in real time
#9> 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 rea…
I feel like this might not be such a big problem if mathematicians around the world weren't so focused on generating a glut of endless generalizations, each of one which is likely of interest to 2-3 people...maybe. (I'm a mathematician, and have published papers.)
Re: Formalising modern research mathematics in real time
#10This would be a good application of AI, convert informal proofs into formal proofs for Lean or Coq.