Formalising modern research mathematics in real time | Hacker News Reader

Formalising modern research mathematics in real time

xenaproject.wordpress.com

111 pointsmauricioc16 comments

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

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

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

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.

This is why I think we need to push for destroying the journals and transforming conferences (to be specifically about networking, not publishing venues). Their purpose really is a fuzzy metric for the academic bureaucrats who are using them as a signal to determine if a paper is good or not rather than relying on their departments, where accountability exists. But of course this is only a small part of the metric hacking and Goodhart's Hell, because we need to say fuck off to the publish or perish shit. I'm in ML and trust me, you don't want to be where we're at. Publishing multiple times a year, chasing hype (because if you don't you get rejected), and overselling papers (you just can't publish groundbreaking work in a few months. Sorry, it ain't gonna be novel but if you don't make it look novel you're gonna get rejected). The treadmill has made me hate academia with a passion (still love research though)

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!

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.

https://mathstodon.xyz/@tao

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

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.

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

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

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"

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.

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

Reply on news.ycombinator.com