The Leiden Declaration on AI is pathetic

Many mathematicians have become concerned about the use of AI in mathematics. AI is used in formal proof verification but due to the competitive nature of academic publishing, also in generating parts or even entire articles. This concern has risen to the point that some mathematicians have come together to write a declaration advising caution in the use of AI. It’s called the Leiden declaration and I suggest reading it.

At the time of my writing this article, it’s been signed by 552 mathematicians. However, I will not be signing it, and I consider the Leiden declaration weak and ineffectual. Why?

Well, the only real recommendation is disclosure. Indeed, when it actually comes to stating a policy on AI tools, the declaration says,

Transparently disclose the use of automated tools, including large language models, machine learning systems, proof assistants, and other mathematical software. Include a “Tool and computational resource disclosure” section in your papers[.]

And:

The use of artificial intelligence in preparing papers can introduce material that makes reviewing more demanding. Make it easier for your peers to review your work by disclosing tool use, giving precise and complete references to previous results, and providing formal proofs where feasible and appropriate.

And:

Some automated tools and their developers will align with the provisions of this Declaration, while others will not. Consider this when deciding which tools to use, or whether to use them at all. Also consider whether non-proprietary, energy-efficient, or small-scale systems suffice for your task. If not, consider how preservation of the values articulated in this Declaration may be worth a delay in obtaining results.

There’s also a bit of pseudo-ethics thrown in:

Mathematics has led to technology which greatly improves everyday life for many people, yet it also has applications in the development of technology for use in warfare, oppression, mass surveillance, and the undermining of democracy. Evaluate the ethical consequences of your research to the best of your abilities, and if necessary withdraw from harmful work. Only enter into external partnerships which respect the values articulated in this Declaration.

It would be laughable if it weren’t so sad. Pretty much any AI technology developed for the use of mathematics is very likely to be applicable to warfare, oppression, and mass surveillance. That’s certainly true for an AI integrated into LEAN, a popular proof verification system. I can very well imagine at least some of the ideas in such an automated reasoning system being used to develop large-scale reasoning systems that could be used for warfare.

Now granted, mathematical proofs are a little different than strategies used for battle, but I mean it’s really not hard to think about how this technology could be integrated back into other AI systems as a component and be useful to the miltary. Interestingly, one of the signatories for the Leiden declaration is Terence Tao, a famous Fields Medalist who also is uses AI extensively and has contributed a lot to LEAN:

The entire Leiden declaration has the spirit of:

Let’s use as much caution as necessary so we don’t disrupt mathematics too much. But, let’s not do anything truly responsible, because we want to have our cake and eat it too — in other words, still use AI, as long as we don’t participate in any projects immediately applicable to warfare.

One professor, Steven Strogatz, said it best in his comment under his signature:

AI has the potential to become a powerful partner in mathematical discovery.

The Leiden declaration is an on-the-fence position. Unfortunately, AI is not a technology that can be used on the fence with caution. It’s negatively disruptive regardless of good intentions. The fact is, in a highly competitive field like mathematics, people will use it to get ahead.

In fact, what AI threatens most is a healthy environment in which to learn and practice mathematics. By even allowing AI into the field, it means that there will be a reduced emphasis on human independence in understanding and practicing mathematics. Imagine a world where you love math, go to school for it, and everyone around you is using AI to understand math instead of working it out on paper. Where people are asking each other fewer questions and asking AI instead. Where professors are using AI to do some grunt work on a problem and even solving problems with AI.

Now, maybe an isolated case of a researcher using AI to help prove a lemma doesn’t sound so bad. Maybe a student using AI to help work through the most difficult homework problem won’t really hurt them. But taken together, it means that AI is highly integrated into the system, regardless of whether it’s ethical open AI or something created by Google.

The end result is that a bright young student’s work to prove that lemma and help the professor will lose significance. And because machines are making all this possible, mathematics will become too specialized so that one won’t be able to completely understand it without the help of AI. In time, if AI is allowed in mathematics, it will become mandatory to use it to keep one’s career afloat.

It’s all terribly depressing, and it makes me happy that I got my PhD way before people were using AI. I think it’s ludicrous to use AI in math. Some have drawn parallels to more primitive computational tools like SageMath, but SageMath isn’t a tool that can be easily used to short-circuit understanding. It’s far more primitive than AI, especially the future AI which is likely to get even more powerful.

I don’t think we should go beyond what our natural intellect can produce, maybe with the help of the most primitive computational tools. I already thought the computational help on the four-color theorem was a mistake, as rudimentary as it was. AI is worse. Much worse. And furthermore, I think the use of AI not only is inevitably detrimental in a technical sense, but it’s also detrimental in a psychological sense because it embodies the psychological sickness of wanting to go too far.

Mathematics already has a problem of being overspecialized with endless questionable generalizations, and that’s actually precisely the environment that has caused AI to be so widely-adopted.

Continuing to use AI will make the problems worse, regardless of the weak cautions recommended in the Leiden declaration. The only thing the Leiden declaration really does is advocate for more care in: (a) using LLMs to write parts of papers, (b) declaring tool use, (c) making sure everything is properly cited, and (d) making sure tools aren’t immediately applicable to throwing political dissidents in prison or attacking other countries. It doesn’t address any of the serious, longer-term consequences of AI on learning. Senior mathematicians like Terence Tao just have the least to lose because they’re the most established.

If mathematicians really wanted to take responsibility for this mess, they would go collectively against the use of LLMs and other AI tools in math. Such tools should not be used, and research on LEAN should cease. And then we should do something about the core problem of math being a race to produce as many endless generalizations as possible.

The Leiden declaration says, “[a]s mathematicians, and also as inhabitants of a shared world, we have a duty to care for other people and our environment.” If they really believed that, then they would stop the use of AI completely because there’s no sane reason to believe that the immense energy required for AI use and development is justified just so one can prove yet another result about modular forms or p-adic spaces.

In short, the Leiden declaration has a pretense of caring about the mathematical community and the world. Personally, I think it reeks of merely trying to preserve the rotting status quo for long enough until the comfortable retirement of most of the people who sign it.