Formalising modern research mathematics in real time

https://xenaproject.wordpress.com/2023/11/04/formalising-modern-research-mathematics-in-real-time/

by mauricioc • 3 years ago

111 16 3 years ago

xenaproject.wordpress.com

tezthenerd• 3 years ago

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.

SkyMarshal• 3 years ago

https://mathstodon.xyz/@tao

n4r9• 3 years ago

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.

curiousgibbon• 3 years ago

Thomason is a phenomenal lecturer, and clearly a great mathematician. It was kind of crushing when he called my Part III essay "pedestrian".

mauricioc• 3 years ago

He had a brilliant Yorkshire accent

There's a talk of his on YouTube for anyone curious: https://www.youtube.com/watch?v=E8BNIohtyMQ (it's unrelated to Ramsey theory but also very interesting).

dunham• 3 years ago

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• 3 years ago

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)

ykonstant• 3 years ago

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.

chongli• 3 years ago

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!

vouaobrasil• 3 years ago

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

whatshisface• 3 years ago

I don't think researchers like running on the treadmill, they are just suffering under a system that rewards what they're doing and that selects so strongly for the top performers, that they can't do anything else.

godelski2• 3 years ago

If only we had better ways to distribute fixes to papers.

I'm not sure what's wrong with OpenReview?

Anyone can upload, like arxiv. Comments are allowed and threaded so can be tracked. Revisions are possible.

But as a ML person, I post to arxiv a lot too. They have improved a bit, allowing for links to Github and such. Which we could make it common place to upload tex source files. Which are already completely accessible via arxiv fwiw.

Hugsun• 3 years ago

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.

haltist• 3 years ago

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

abss• 3 years ago

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"

Formalising modern research mathematics in real time

Related Stories