> Outsourcing the work deprives you of who you become by writing it. Just because AI can do something that resembles work should not mean outsourcing work to it. Mathematicians should not outsource their work to AI just like programmers should not outsource programming to AI. Humans working with AIs in a tight loop means intellectual work becomes more high-level and creative, but a human should always own the work, validate it and stake their reputation to it. Simply ban any humans who produce low quality work using AI.

I think there would still be a place for it if it's beyond human comprehension. For instance, really complex lemmas to solve human-tractable problems. If you can pose a question in a proof assistant language like Lean, have an AI write a Lean program that solves it, you can use that as a Lemma for some other problem. There's quite a bit of math out there that is "correct assuming conjecture X is correct", maybe AI could fill that gap and "still be math".

My understanding is that we’re talking about “tool-assisted” proof generation, which provides some guard rails but would still allow significant creativity. Tools like Lean, Coq, etc.

It’s easy to imagine this being a problem both in quality and in volume. Verifiable work is less valuable than verified work. And noise is always costly.

Esoterism is mostly a social tool to keep those not initiated excluded from the private club. Most of the time mathematics becomes tricky less due to unfathomable intrinsic complexity, and more due to the way it’s communicated. LLMs don’t give a shit about social side effects, leave alone on unconscious level, because they are void of any intention. At most they are tuned on their thin edge layer to lean toward this or that kind of output, but that’s it. Now the landscape shift as it’s sold (I guess) is that anyone can take a postdoc gibberish infused with the hard gained academic winks and subtle references and turn it into a ELI5 "does it have any applicability for my concrete issue at stake, prove it through Lean, good let’s deploy".

> The authors warn the consequences are already becoming visible. AI-generated papers could overwhelm peer-review systems with low-quality work … It seems like a key problem here is that peer-review is expected but not explicitly funded/rewarded while it is probably one of the aspects where humans still add a lot of value. Academia’s incentives are hugely misaligned (… as usual unfortunately).

Math is one field where you can mechanically prove a paper's findings. The only thing that would need to be judged is the (verified) statement's importance.

Yes in theory, but not yet in practice because not everything is fully formalised.

The wording in the declaration may be a bit romanticized. But the points are valid: Is an 80 year old unsolved problem maybe unsolved because it was never prioritized? Some problems stay unsolved because few people consider them worth working on. Who is going to validate the results? Or do we skip that, with the risk of flooding the literature and collective understanding with unverified proofs?

I imagine the concern is more towards using LLM's to create proofs rather than using them to understand things.

> AI-generated papers could overwhelm peer-review systems with low-quality work That's not a problem unique to math, or even to academia. It's a problem in every context in human life where people communicate via written documents.

It is potentially worse with math because accuracy is much more important and there are fewer reviewers compared to other fields.

It will drive math journals to require formalization of the proofs in the supplemental material.

Sorry did you read the article or just the headline? The theme is mathematics is a human-endevor and automation undermines that, particularly the ones starting out. It risks killing the culture entirely. Some other key points: - AI-generated papers could overwhelm peer-review systems with low-quality work. - It may become difficult to assign proper credit for discoveries. - Researchers who choose not to use AI tools could be disadvantaged. - There are ethical concerns about mathematical work being used to train AI for military and surveillance purposes.

Sure, but their peers (who do use AI) will out-publish them soon enough and solve the open problems before they do.

Does it matter whether any of this is correct? (Mathematics at least has the potential for automated non-AI proof checking, although I don't think that's as widely used as you'd expect)

Does it matter if the Leiden Declaration is correct? To the humans, maybe but not in the bigger picture. At scale, correctness and reward are becoming increasingly disconnected. Example: capital continues to compound regardless of whether it reflects underlying human welfare, just as information can spread regardless of whether it is true. Reality still matters, of course. If you want airplanes to stay in the air, somebody eventually has to be correct. The problem is that our economic and social systems are becoming less effective at distinguishing between what is true and what is merely rewarded.

> This is all contingent on AI forays into mathematics being slop and low quality It's literally a set of recommendations for researchers on how to use AI to advance the field and prevent slop from overwhelming the people who might do anything with the research produced. For people who are so eager to declare that everyone else is just having an existential crisis because "your culture is commodified", AI people are getting awfully defensive about this document.

Are maths AI models now using "tools", aka formal solvers? I understand that the "language interface" of a "maths AI" could be some specialized trained LLM (Large Language Model) that to convey, with human language, "high level" mathematical mental contructs and intuition. But then, you would need some models which does the reasoning using formal mathematical solvers (and probably a ton of "scratch" memory, it would be interesting to see how those models end up storing "mathematical" lema data). I guess you can have ML (Machine Learning) for those models on 'general maths', but also we can think about more mathematically focused ML for a specific problem, area, etc. And in the end, ML for maths, would it be mostly permutations of truth statements fed to a neural net? When we were talking about "AI", one decade ago, that was what most had in mind (it may help a bit in physics, but it seems less likely, because reality/experiments are hard to teach to "AI"s). If that becomes a reality (aka easy hardware access, and some "working" models), mathematicians will have to be as good in maths than in maths ML. And this is were there is an issue: training honestely good mathematical human brains may become very hard with some broad availability of good general maths reasoning "AIs".