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, an…
Thomason is a phenomenal lecturer, and clearly a great mathematician. It was kind of crushing when he called my Part III essay "pedestrian".
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.
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"
> 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.)
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.
> 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…
> 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)
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, an…