I still don’t want a “first pass the post” kind of math, but that would be a sensible solution

Just to give a comparison, a high-output mathematician publishes between 2 and 5 papers a year (depending on branch of math and dividing by co-authors).

Most are incremental work, so a little step towards solving a problem or a conjecture. A lot is just a “hey, look at this neat trick”. Solving “big problems” is usually the work of a decade or more, in which the mathematician is working on other stuff as well. So let’s roughly say that solving a big problem usually takes some 10 years of work and some 10-30 papers (assuming working roughly half time on it).

So on one hand, 1 paper per big problem is too little to actually understand what’s going on, on the other 700 papers are the output of more than a hundred mathematicians over a year. A math department in a university is around 50 mathematicians, I would say? So two medium-sized departments.

The other part of your comment. “If its proven and understandable”

At the moment, the preprints are assumed to be a shit sandwich. (Aka “would you eat a sandwich is there could be shit in it?” ). Using the results is just too risky without understanding if they are correct and how they are build.

The “understandable” bit is also really hard. I picked a random one in my field (nothing I directly worked on) and it was unreadable - mostly because of notation used without defining it and no explanation of what is going on, no overview or intuition. So to me it seems more shit than sandwich. As a reviewer, I would never accept such a paper.

Then finally, let is assume it’s all perfect and good. The goal of proving something in math is to develop understanding and a method to apply to other cases. So once all these papers are studied and understood, poop discarded, rest of the sandwich saved, ideally we will have new understandings of whole sections of math, new connection between items we’re weren’t aware of. What I think AI did in this context is to chain things that were already known, but there was no one whose knowledge spanned wide enough to know that all the pieces were already laid out. So it could be groundbreaking - once we remove the shit. How much shit there is is anyone’s guess.

Maybe there should be: link to preprint stating that the Lean code doesn’t do what the papers claim (for Navier-Stokes)

I can add about your last paragraph(it’s literally the core of what I do). There is a field of computer assisted proofs, that is mathematical proofs that need a computer to be completed.

The first and most well known example is the four color theorem. How many colors do you need to color “a map”. Answer: 4. Proof: very very long. By hand it is possible to prove that there are only 1834 options, and a computer was used to color all these explicit options. At the time, it was a scandal. Nowadays, other computer assisted proofs are accepted, such as the ones relying on validated computing: if a computer (with some restrictions and guardrails) can show that a certain value is over/under a given threshold then something else is true.

Then, there is the validated proofs approach. This is where Lean comes into play, if you have heard about it. You can ask a computer to check your proof. This is helpful for confusing, long proofs (most of math). You input all the logical steps you took and Lean confirms that all is logically sound. Many AI proofs are “Lean verified”, but there is controversy if they are proving what they claim they are proving. It’s also a massive chunk of code that nobody can understand.

I joined Lemmy a couple of years ago and I already notice more user engagement. I would like a little bit more, such that more niche communities can have an ecosystem of posters instead of a single one doing most posts. But not much more indeed