In general, I don’t like to write about my work because writing is a hobby I reserve to keep my mind diverted from work. A lot, however, has been happening recently in my work life, and I can feel its effect on my health. I write this as an effort to understand my own feelings better and to process. This essay should, in no way, be considered a technical piece.
I am a mathematician who has worked in the areas of formalization of pure mathematics, and more recently, AI for mathematics. I will try to explain these simply below.
Formalization inherently means making something “formal” – in this context, it refers to verifying mathematics written on paper using computer programs. It serves as a check by a machine, pointing to mistakes in proofs in precise locations. While formalization requires a proof, AI for mathematics developed with the aim of discovery. Until the last 6 months, AI for math meant training a small inexpensive model that could run on your computer to search for examples or counterexamples, or finding patterns in existing data. One would then use this to build interesting conjectures and theories.
A different direction was to use Large Language Models (LLMs) for the purposes of “autoformalization” – using a machine to do formalization. When autoformalization began, I was in the third year of my PhD (2022), specializing in formalization of mathematics. Formalization was a rather challenging field at the time, with most mathematicians asking why their work required checking, and if human trust was insufficient. I used to conduct training workshops on formalization. One of the frequently asked questions I received was: will this take our jobs? Remember that grading, lecturing and tutoring contributes a big chunk of the working mathematician-cum-researcher’s income. The enquirer was worried that these programs, which could detect mistakes in an argument, would make grading redundant. Formalization, however, was a rather time-intensive procedure, and I told them to have no qualms; it would be a long time before this could be integrated into the daily workflow of the mathematician. The estimate for a long time was at least a decade, with an underlying assumption that the community would find a systemic streamlined approach that would secure livelihoods by then.
Why a decade, you might ask. An LLM relies on having a large amount of data from which it can pick up patterns. Given the current architecture, and in order to get good at learning the nuances of a language, the data must be ginormous. In the case of formalization, this much data simply did not exist. At the time, we (the community) barely had managed to formalize some levels of undergraduate mathematics and a very tiny portion of research mathematics. To put things in context, my PhD thesis was based on formalizing about 20000 lines of code, and merely 3 pages in a textbook of number theory. This was because the background concepts were missing at the time, and we had to painstakingly build these from scratch.
What I did not estimate, however, was the power of compounding. A lot of stalwarts in the field went about advocating for more mathematicians to take formalization seriously, and they did. Suddenly there were armies of mathematicians dedicating a considerable amount of time to formalizing major theorems. As word spread, the number of contributors grew exponentially, as did the contributions. Industry started diving its nose in too, in an effort to gain more trust in their security and blockchain related products. What I also could not estimate was the big AI companies using (stealing, actually) literature written by thousands of mathematicians (and others) over centuries to train their models. If they would have followed through with these procedures, it would have certainly taken them a lot longer for their models to achieve the “intelligence” it currently possesses.
To be clear, I don’t think obtaining consent and giving appropriate honorariums would have solved this matter, whose outcome was impossible to know. Some of the creators of AI have been predicting this situation (and worse) for years, but one often forgets that benevolence and greed are two sides of the same human coin. Our desire to better humans lives and intellectual curiosity drove us to building the concept of an intelligent machine; our greed will persist with it. Even having followed all the procedures, there would certainly be a point in the future where we would have reached this same pickle we currently brine in.
Four years later, we now have LLMs that excel at autoformalization. LLMs have also become very good at inventing proofs, that too, to questions that have baffled humanity for decades! There is a conjecture that the former led to the latter, however, there is no evidence of the same. OpenAI recently dumped 722 solutions to major open questions in math, a lot of which came attached with complete autoformalizations. This way, one has no reason to distrust their proofs. This completely shook the community, with most mathematicians lying on either end of the spectrum: some breaking down over their career being over, the others celebrating advancement.
As a bystander, I chose not to react, at least publicly. As my experience with formalization taught me, when dealing with technology and fragility, panic spreads quickly. I could not understand the motivations of the AI companies; surely, they were aware of the havoc that would ensue. Was it showcasing intellectual superiority or a fearmongering tactic?
This has certainly changed how a vast majority of mathematicians currently work. Most mathematicians have paid to have access to a model of some kind, which they use not only for literature surveys, but also to speed up their research. This comes with its disadvantages: I hear rumours of ongoing work being stolen from the abstracts of talks to be given, with the results being published before the talk, heavily “assisted” by AI. This means that competitiveness is at an all-time high, leaving no time for novelty or a polished understandable piece of work. A famous journal has been flooded with 60000 submissions this year, with the total count for the previous year being about 19,500.
There is an even greater push to have autoformalized works, now that LLMs are so good at it. The bottleneck is that AI “vomits”: it can recreate existing concepts, and can make a direct proof take a very roundabout long path. This is where I come in, but the very fabric of my work has transformed.
As an example, the current project I am working on required me to autoformalize a paper. In the (recent but distant) past, I would have spent a few months first chalking out the skeleton, and then going through the individual pieces, perhaps using AI for small bits here and there. This time, I was instructed to use Claude, given that there was no time to waste. My team wanted the result to be released the next day, before any external party had a chance to scoop it. Claude gave me 40000 lines of code in about 6 hours of work – about double of what I had formalized for my PhD thesis!
Wading through that code and deciphering it, however, is a major bottleneck, potentially harder and more time consuming than formalizing it. The other snag is that the model could prove things differently to what is written in the natural language text. This is indeed often the case, even for manual formalization efforts. One cannot, however, claim that the proof they have written is correct, which means that one must understand the AI-generated code and distil it in order to write the accurate proof, and the cycle continues..
I am fortunate enough to be in a relatively decent position with recent tidings, in terms of academic jobs. Yet, this gives me anxiety. I have gone from being the creator and doer to the checker. This was somehow the goal that I had wished for: to not have to bother about the complex task of formalizing. I should be happy about it, but I miss the little tidbits of insight that I would gain from the process: an assumption less here, using a new tactic that speeds up work there. I miss the itch in my brain, and satisfaction that is the result of effort. Perhaps my own insights are no longer essential to the development of the field. This was a very hard truth for me to swallow.
In Legally Blonde, Professor Stromwell quotes Aristotle: “The law is reason free from passion”. Recalling this later in her speech, Elle says, “… I have come to find that passion is a key ingredient to the study and practice of law and of life.” Such is the case, I believe, with mathematics too. Contrary to widespread belief, mathematics is the fruit of passion, not only logical reasoning. The reason AI’s progress in math hurts is because we get to see the machine taking our place, following our passion, doing the work that fires our passion.
As it stands, this is another big issue for math academia. It has happened so quickly that the community has had no time to ponder about the ramifications of losing their passion and more importantly their source of income. Most mathematicians I speak to (especially those that do not have a permanent job yet) are panicking, and not without reason. Certainly, the structure of academia will undergo a shift, with even more jobs being cut in an already somewhat cut throat environment. Most of the people I know who completed PhDs in pure mathematics after me have been struggling to find postdocs. One must also keep in mind that our profession seldom encourages industry experience, which means that quite a few PhD graduates spend at least half a year after graduating without an income preparing for job interviews.
Amidst all the chaos, a lot of questions stand unanswered: how does one “share” credit with AI in joint work? What is the point of publications (a very important measure while job hunting)? What do we teach our students? What happens when AI overtakes human mathematicians, and deems them dispensable? How safe is the information we share with AI? Is there any meaning left behind the madness?
As I grappled with these questions, the light at the end of the tunnel seemed to be getting darker. I felt no inclination to continue working. So, I took a day off. A conversation with my father reminded me of a book reserved for doomsday occasions: Mans Search For Meaning by Victor Frankl. I found my beacon of light in the preface:
“Everything can be taken from a man but one thing: the last of the human freedoms—to choose one’s attitude in any given set of circumstances.”
Dr Frankl was talking about a situation with a lot more depth: surviving the Auschwitz concentration camp. His statement, though, still rings true. Beyond its profound meaning, I realized that this is what drives me: to create something that outlives me, that holds meaning beyond my mere existence. That is certainly worth fighting for.
With a renewed motivation, some quality sleep, and a lot more calmness, I thought. I realized I was doing something I was trying to stop others from doing: panicking. The waters of my mind were bordering on turbulence, as opposed to the tranquil I envisaged. I also realized that it is human nature to do so. Once the grief of a changing world had been processed, people would be ready to collectively answer the questions we need answers to.
Mathematics is the first and will probably be the most affected, given the infinite amount of perfect data the field produces. To be clear, I have no doubt that AI can potentially offer breakthroughs that could benefit humanity and better shape our world. One can, however, expect other white-collar jobs to be affected soon. Depending on advances in robotics, perhaps almost all jobs are at stake. Fortunately, or unfortunately, unlike the arts, most fields do not have the luxury of turning down the benefits AI offers. Moreover, the lack of transparency regarding the resources used (especially environmental) is very concerning. We have tools that we are not currently equipped to deal with, and are walking into an unknown future agitated. I sincerely hope we start asking and answering the right questions very soon.
It is quite humbling to see the finite dimensionality of human thinking and the human world; perhaps these machines can help perfect it. In the hands of humans, whether they are a boon or a bane remains to be seen. Until then, I shall persist in my pursuit for a meaningful life.
