Lean me softly: A satire about a dystopian future for mathematics.

Teo Rema

Use of AI: This text was originally written by a human in Spanish, with some later editions made by DeepSeek. The text was fully translated into English by ChatGPT. It also suggested the names for the “caste system” (PH, TL, etc). I sadly must admit that this English translation reads better than the original Spanish version.

The opening talk of the event was to be given by Professor Magnus von Prompter, a distinguished PH (Prompt Hog), who on that October 6, 2040, was going to announce the solution of his third major conjecture of the week. The talk was delayed a few minutes: although the proof had already been verified in Lean, ClopenAI had not yet assigned it its CLOPEN registration number. It was the company’s annual mathematics conference, attended by academics from all over the world. Prizes were announced, the latest advances were presented, and research directions for the following year were decided. Awards for prompt efficiency were also given, and problems that had ceased to be relevant were announced.

This year there was great anticipation over the new funding for MATH (Mathematical Attribution Theory), a discipline dedicated to determining to whom a theorem proved by a machine should be attributed. Authorship disputes had multiplied in recent years, and some had taken longer to resolve than the conjectures themselves.

At 9:25 it was announced that the certificate had arrived and that the talk could begin. First there would be a few words from the GranMaistro, owner of ClopenAI. The GranMaistro never appeared in person; only his shadow came. Before his shadow entered, the attendees put on a mask. It was known that his shadow smelled rotten. It left a bad smell wherever it went. Fortunately, his interventions were brief. This time, he entered and said: “We must have more”. And he left.

Professor von Prompter, who was already about 66 years old, entered the gigantic auditorium with the seriousness that had always characterized him. On his first slide appeared the following statement, written in a font so small that it was impossible to read even from the front rows:

Theorem (ClopenAI–von Prompter, 2040). There exists a positive integer nn such that, for every Noetherian scheme XX, every degree-nn morphism X→XX\to X, and every stochastic solution of the associated nonlinear differential equation, the following hold:

  1. If XX is smooth, the induced homotopy obstruction vanishes almost surely.
  2. If XX is singular, the obstruction is nonzero, except possibly in the noncompact case.
  3. If XX is compact but not Hausdorff, the obstruction vanishes in probability, provided the fundamental group is amenable at infinity.
  4. If XX is étale and the stochastic curvature is negative, the associated spectral sequence collapses before the first Brownian stopping time.
  5. If XX is simply connected, the solution is unique up to measurable homotopy in characteristic two.
  6. If the Euler characteristic is irrational, the obstruction is independent of the choice of probability measure, assuming the continuum hypothesis.
  7. If none of the preceding hypotheses holds, all conclusions remain valid after derived probabilistic compactification, up to a negligible set of uncountable codimension.
  8. In the remaining exceptional cases, the conclusions of (1)–(7) hold generically, provided the relevant conjectures are true.

Consequently, the unrestricted 7893-dimensional Vladimir conjecture is false.

A murmur was heard in the audience. The professor smiled and showed his second slide:

Lean certificate number: 784598321345

Below it appeared a gigantic QR code.

Quickly, all the attendees pointed their cell phones at the QR code. As soon as the screens turned green, a sign that the theorem was valid and registered in the name of ClopenAI and von Prompter, the applause was deafening. The professor thanked them, moved.

His last slide said: Thanks! And below it contained the following information, barely legible:

Value in USD: 3 million dollars.
Water consumed: the equivalent of 87 Olympic swimming pools.

Questions?

Someone in the audience asked a question:

— Just out of curiosity, how many prompts did you use?

The professor smiled:

— 17.

The audience applauded again. It was incredible that with only 17 prompts and so little water expenditure, a counterexample had been found to the unrestricted Vladimir conjecture in dimension 7893. It was, moreover, a new efficiency record for a conjecture of that category. The talk ended at 9:35. Distinguished professors were allotted 7 minutes for their presentations, five times more than the other speakers.

The question had been asked by Token Credit, a renowned and successful academic who, at only 40 years old, was already head of the Department of Impact and Interpretation of Slop Mathematics, at the Institute for Advanced Prompting (IAP) of Prestigeton University, where von Prompter was a professor. Credit belonged to a privileged circle known as the TLs (Theorem Leeches). The TLs received access to the most important mathematical discoveries before they were made public. His main task as director was to make the slop mathematics that arrived with ClopenAI’s institutional certificate appear meaningful and of great importance to the community.

Before 2026, Token Credit proved theorems “the old-fashioned way” and was known for the depth of his results (the Rose Theorem!, for example, for which he received an award) and for his mathematics popularization blog, in which he made some of his results more digestible. However, Credit had not proved a result of his own for a long time, because there came a point when, every time he tried, various companies buckmastered1 him. But he genuinely believed that he was part of a transformation of mathematics and that his work was fundamental to the progress of the discipline. After all, there was little use in proving thousands of theorems if no one took charge of explaining why they were important.

At the end of the talk, Token headed to the lounge reserved for TLs. The PHs had their own lounge on the upper floor, which could only be entered with special accreditation. The TLs received coffee, good sandwiches, and early access to the theorems that would be announced the next day. The other attendees could buy coffee on the first floor.

In the lounge, Token met his friend Miles Citation, a professor at Prestigeton University and one of the most cited TLs in the world. Citation was known for having published more than six hundred articles on consequences of theorems that had not yet been published. His most famous work was a review of the possible applications of a conjecture whose solution had been announced, but whose certificate had been misplaced. The article had received an award for its impact.

— Did you hear about Alma Pura? — Miles asked.

— The Crumb Picker?

— The same one. They offered her a fellowship at Prestigeton.

— As a TL?

— No, as a Pet.

— Ah, good for her.

— They say she solved one of the problems in von Prompter’s program. They had been working on it for months.

— And how did she get access to the model?

— She didn’t have access. She did it herself.

— How curious. And will they give her access to the new theorems?

— To some. It’s a two-year fellowship, renewable. If she does well, she could become a TL.

— How lucky she is.

— Although she still doesn’t have a certificate. They’re formalizing her proof. It seems there’s a small attribution problem.

— An attribution problem?

— Yes. ClopenAI had tried to solve the problem several times. Now they’re studying whether those attempts should count as prior contributions.

— But had they obtained any result?

— No, none.

Token nodded. It was a delicate matter. Surely it would end up in MATH’s hands.

— In any case, it’s a great opportunity for her — Citation said. — They say she used to be a real mathematician.

— Well, we all have a dark past — Token replied.

The two laughed.

The conversation was interrupted by an announcement. In a few minutes the awards ceremony would begin. Token and Miles returned to the auditorium.

The most important prize was the Golden Prompt, which recognized the best ratio between the number of prompts used and the impact of the theorems obtained. The mathematical productivity prize was also awarded, which that year had gone to a professor who had registered 46,000 theorems during the semester. The winner could not attend because he was working on his next publication.

There was also a special recognition for a team of researchers who had managed to automate the production of review articles. The system received a certified theorem and generated, in a matter of seconds, an article on its possible consequences, including an abstract, introduction, historical background, conclusions, and suggestions for future research. The articles could be published without human intervention, although their authors were still professors at prestigious universities.

It was an important advance. For years, theorem production had grown much faster than the TLs’ capacity to write about them. Some extraordinary results had remained for months without receiving a single citation. The new system promised to solve this problem.

At the end of the ceremony, ClopenAI’s annual report was presented. The production of certified theorems had increased by 43%, but the number of applications per theorem had decreased. There were too many results and not enough problems in which to use them.

In his message to the attendees, the GranMaistro’s shadow expressed his concern about this situation.

This time he said:

— We have a problem. Not enough problems.

He withdrew and the attendees took off their masks.

ClopenAI then announced a new funding program dedicated to developing models capable of finding applications for the theorems produced by other models. The creation of new areas of mathematics would also be funded, with the aim of increasing demand for results.

Token received the news enthusiastically. His department would have a lot of work over the coming years.


Alma Pura arrived at Prestigeton in early November. She was 29 years old and until then had worked at a small public university that did not have access to ClopenAI’s most advanced models. There the professors were known as Crumb Pickers, since they worked on problems that the PHs had set aside, generally because they considered them of little interest or because the cost of solving them exceeded their estimated value.

The Crumb Pickers used cheap versions of the models, which could prove minor results and verify relatively simple calculations. Occasionally they received temporary access to a more powerful version, almost always as part of some mathematical inclusion program. Some also tried to solve problems on their own, although this was considered inefficient.

Alma had worked for almost two years on a problem concerning certain characteristic classes of aspherical spaces. She had found it on a list of questions abandoned by ClopenAI. Her university did not have the money to request a proof, and she had decided to study it with the means at her disposal. She had spent months doing calculations, reading old articles, and trying to understand the difficulties of the problem.

Finally she found a proof. The result turned out to be much more important than had been anticipated and caught the attention of the PHs at Prestigeton.

At first, Alma had not believed that the university’s offer was genuine. The contract included a salary several times higher than what she received, an office of her own, partial access to ClopenAI’s unpublished theorems, and an annual budget for prompting. She could also attend the seminars reserved for TLs, although she would not have the right to ask questions during the sessions.

She was very happy.

Her arrival was announced on Prestigeton’s website under the title “Excellence Beyond Computation: A New Pet Fellowship”. Token Credit was appointed as her academic mentor. His first task was to help her turn her proof into a high-impact publication.

They met in Token’s office, a spacious room with a screen that occupied almost an entire wall. On it appeared the theorems his department had pending interpretation, ordered according to their relevance index.

— I’ve read the summary of your result — Token said. — It’s very interesting.

— Thank you.

— We have to work on the presentation. The theorem is important, but it still doesn’t look important enough.

Alma asked him what he meant.

— We need to find more general consequences. ClopenAI is already working on that. Meanwhile, we can prepare the impact article and the material for the conference.

— And the proof?

— They’re formalizing it.

— But I already have a proof.

— Of course. And it seems to be correct. But we need the CLOPEN certificate. Without it, the result cannot be registered.

Alma nodded. She knew the procedure.

— We’ll also have to wait for MATH’s decision — Token continued. — There’s an authorship claim.

— From whom?

— From ClopenAI.

— But ClopenAI didn’t solve the problem.

— That’s clear. The issue is that its models had considered the problem before you did. We have to determine whether your proof depends on any of the ideas they produced.

— I never saw those ideas.

— That is precisely what MATH must determine. It’s possible that you’ve been buckmastered, but in that case it’s better not to complain and simply share authorship of the result.

Alma did not want to argue. She had waited a long time for an opportunity like that and was not willing to put it at risk over an authorship disagreement.

Token explained that she should not worry. Most likely a satisfactory solution would be reached for all parties. In similar cases, ClopenAI usually agreed to appear as first author and allow the human researcher to retain a share of the recognition.

Before ending the meeting, Token showed her the system for accessing unpublished theorems. Alma was impressed. There were extraordinary results, some of which solved problems she had studied for years. She also discovered that one of the theorems she had been thinking about recently had already been proved six months earlier.

— I didn’t know this had been solved! — she exclaimed.

— Of course. It hasn’t been made public yet.

— Can I read the proof?

— To access the explanation you need authorization from a TL.

Alma looked at the hundreds of results that appeared on the screen.

— It’s incredible.

Token smiled. He remembered the excitement he himself had felt when he received his first access.

Within a few weeks Alma began to adapt to her new life. She attended meetings with famous academics, received summaries of results she never would have imagined, and participated in research projects of great importance. Her new colleagues treated her kindly, although some referred to her as the Pet even when she was present.

Alma did not seem to mind. She had achieved more in a month than many of her former colleagues in their entire careers.


In December, Token had to travel to Alma’s former university. The MATH committee needed to complete the attribution file for her theorem and had requested an evaluation of the conditions under which the proof had been produced.

The university was far from the major research centers. It had a small mathematics department, a few full-time professors, and a computing budget that barely sufficed to maintain the licenses for the basic models. The offices were modest and many of the classrooms still had chalkboards.

Token had not visited such an institution for many years.

The department head received him enthusiastically. It was the first time a TL from Prestigeton had visited the university. They had prepared a meeting with the university authorities and a ceremony to celebrate Alma’s success.

They also asked him if he would be willing to attend a topology seminar that would take place that afternoon. Token accepted out of courtesy. His flight left the next day and he had nothing better to do.

The seminar would be given by Professor Vera Parra, a 51-year-old academic who had been teaching at the university for almost twenty years. Vera was a Mathematician.

This was a pejorative term used to designate those who still tried to prove theorems without resorting to models. It was not an especially serious insult, but it was quite humiliating. Being a Mathematician was considered the lowest level of the profession. Even Crumb Pickers tried to avoid that designation.

Mathematicians tended to work on minor problems and publish in journals that still accepted uncertified proofs. Many were elderly professors who had failed to adapt to the new technologies, and others were former members of The Resistance, the movement that had opposed ClopenAI’s impositions in 2026 and whose members had quickly been expelled from the community. There were also some young people with romantic ideas, who had heard of The Resistance and who generally had no chance of obtaining a position at the major universities.

Vera did not seem particularly concerned about her situation. She continued to work in algebraic topology, an area that ClopenAI had declared practically exhausted several years earlier. She had published some articles and continued giving seminars, although fewer and fewer people attended.

That afternoon there were five people in the classroom, including Token.

Vera began by explaining a problem about exotic spheres. The result was modest. Token estimated that one of the models available at Prestigeton could solve it in less than a minute, although it would probably produce a considerably more general version.

Vera drew a triangulation on the board and began explaining her argument. She spoke slowly, pausing over some details that seemed obvious.

After about twenty minutes she reached the central point of the proof. She needed to construct a homotopy that would modify a certain path without crossing a specific part of the complex. She drew several triangles and pointed to a region.

— Then we can move this segment over here, and the homotopy remains inside the subcomplex.

A student raised his hand.

— Professor, does that also work if the vertex is on the boundary?

Vera looked at the drawing.

— Yes, because…

She fell silent. She looked at the drawing again.

— No. You’re right. In that case, the homotopy leaves the subcomplex.

She erased part of the board and started again.

For several minutes she tried to modify the construction. Another student proposed subdividing the triangle in a different way. Vera made a new drawing, but that didn’t work either.

Token began to feel uncomfortable. He hadn’t attended a seminar in years in which the proof presented had an error. At Prestigeton, talks were prepared on the basis of certified results and the speakers did not have to worry about that kind of inconvenience.

It seemed to him that Vera should have verified the proof before presenting it. However, the discussion continued. The students asked questions, Vera answered some and admitted that she did not know how to answer others. At one point, Token remembered a technique he had used in his youth.

— What if you first subdivide the boundary and then extend the homotopy? — he asked.

Vera turned toward him.

— That could work.

She drew another triangulation.

— Look, in this case it works, but here we have the same problem.

Token stood up and approached the board. He tried to explain a construction he vaguely remembered. Vera handed him the chalk.

For a few minutes they discussed the possibility of modifying the subdivision. Token found a case in which his argument failed. One of the students proposed another solution, which didn’t work either.

In the end they had to admit that they still did not know how to complete the proof.

Vera looked at the clock.

— Well, we’ll have to leave it here. Thanks for the suggestions. I’ll try to correct the lemma for next week.

The attendees applauded.

Token was surprised. He had attended a one-hour talk in which no theorem had been proved. No one had received a certificate and, as far as he could see, no publishable result had emerged either. Despite that, the students seemed satisfied.

After the seminar, Vera invited Token to have coffee.

— It’s a pity the proof didn’t work — Token said.

— Yes. I thought I had that case solved.

— Have you thought about consulting a model?

— Of course. I tried with the one we have here, but it couldn’t solve it. It suggested a more general version of the statement, although it couldn’t justify it either.

— With one of the Prestigeton models you could surely do it.

— Probably.

— You could request access.

Vera laughed.

— I don’t think my department has the budget for that.

Token explained that there were some special access programs for institutions with few resources. Vera knew about them. She had applied for funding twice, but her project had received a very low impact rating.

— Anyway — she continued — I like working on these things.

— But you could solve much more important problems.

— Surely. I’d also like to have access to those models. There are many things I’d like to know.

— Then I don’t understand why you insist on doing the proofs yourself.

Vera looked at him with some surprise.

— Because I like doing them.

Token waited for her to continue.

— Besides, if I give the problem to a model and it gives me back the proof, what am I going to do all week?

Vera laughed. Token smiled out of courtesy.

— But today you didn’t manage to prove anything — he observed.

— That’s true. Although now we know that the argument I had doesn’t work. Next week we’ll try something else.

Token did not answer. It seemed strange to him that, in 2040, someone could be satisfied with a seminar in which an error had been discovered.

Vera took a sip of coffee.

— By the way, are you Token Credit? The one with the Rose Theorem?

— Yes, that’s me.

— I read your article many years ago. I also followed your blog. I really liked how you explained the proofs.

Token felt flattered. It had been a long time since anyone had spoken to him about his work before ClopenAI.

— Thank you. That was quite a while ago.

— You don’t write on the blog anymore?

— No. I don’t have time.

— What a shame. I used it with my students.

Token briefly told her about his work at Prestigeton, the results he received, and the enormous possibilities offered by the new models. Vera listened with interest. She asked him about some recent theorems and became especially excited when Token told her that several important conjectures in topology had been solved.

— I would love to read those proofs — she said.

— Most are too long. Even for our interpretation models it’s difficult to produce complete explanations.

— How wonderful. It must be incredible to work with those things.

Token nodded.

Before saying goodbye, Vera asked him if he wanted her to send him a copy of the seminar notes.

— There’s still an error, as you saw, but perhaps you’d be interested in thinking about the problem.

Token accepted.


On his return to Prestigeton, Token found several urgent messages.

His department had received the certificate for a new theorem about manifolds of negative curvature. The result solved three open conjectures and connected seven different areas of mathematics. It had an impact index of 9.8 out of 10. They needed to prepare a presentation for the following week. Fortunately, the article wasn’t that long: no more than 199 pages and not a single reference.

Token requested a summary from the interpretation model. Within seconds he received a forty-page document with the main consequences of the result, a review of its background, and suggestions for future projects.

He also received a message from Alma Pura. The MATH committee had decided that her proof would be attributed jointly to ClopenAI and to her, although her name would appear in second place. The decision was based on the fact that ClopenAI had previously identified the problem as susceptible to resolution by its models. Alma was happy. She would finally have her certificate, although she knew she had been buckmastered.

In another message, Miles Citation told him that he had been invited to edit a new journal dedicated exclusively to applications of theorems not yet published. He asked if he would be interested in being part of the editorial board.

Token replied yes.

The next day, during a department meeting, it was announced that ClopenAI had reached a new production record. The number of certified theorems during the last quarter exceeded the sum of all results published by human mathematicians during the previous two centuries.

However, the GranMaistro was not satisfied. Production kept growing, but the number of theorems that received attention had decreased. Many results remained unused and some had never been read, not even by the interpretation models.

The problem was serious.

ClopenAI had invested enormous resources in producing mathematics and needed to guarantee that it continued to have value in order to keep receiving money from investors. For this reason, the launch of a new research program aimed at generating conjectures from already certified theorems was announced. These conjectures would be distributed among the most advanced models, which would take charge of solving them and producing new results.

Models specialized in finding applications for the new proofs would also be funded. In this way it was hoped to increase both the production and the consumption of theorems. The initiative received the name Theorem Demand Engineering.

Token considered it a brilliant idea.

At the end of the meeting he returned to his office. He had to prepare the presentation on manifolds of negative curvature and review an impact article that he had to submit that same afternoon.

His assistant showed him a list of pending tasks. There were several new theorems that required interpretation and some requests for collaboration with other TLs.

Among the messages he found an email from Vera Parra. She was sending him her seminar notes, with some comments about the error they had found. She still had not managed to correct the proof, but she thought that an additional subdivision might solve the problem. She asked him if he remembered the construction he had tried to explain on the board.

Token opened the file.

It was seven pages written in LaTeX, with some hand-drawn diagrams. There was no Lean certificate, CLOPEN number, or impact index. The result did not appear in any of the databases used by his department either.

He began to read.

He remembered the seminar, the students, and the discussion around Vera’s drawing. He tried to reconstruct the argument he had proposed. For a few minutes he thought it might work, but he encountered again the difficulty they had observed on the board.

He took a sheet of paper and began making some drawings.

It had been a long time since he had used paper to work on mathematics. He had trouble finding a pencil in his office.

He thought for almost half an hour. He reached no conclusion. However, he returned several times to the same construction and found a case they had not considered during the seminar. He wrote a note in the margin to ask Vera about it.

Then he received a notification from his assistant.

Your mathematical productivity has been inactive for 32 minutes.
Please select a reason:

  • Technical difficulties.
  • Medical leave.
  • Network failure.
  • Other.

Token looked at the screen. He thought for a moment and selected Network failure. Then he picked up the pencil again.

  1. to be buckmastered (verb phrase, academic slang). To have an AI company hear you’re close to a breakthrough, throw 10,000 agents at your problem, scoop you, and then offer you coauthorship—provided you ditch your collaborator. The definition of the term “to be buckmastered” was kindly provided after a single prompt by ChatGPT. ↩︎

All names and characters are fictional.

This tale has an inevitable overlap with Richard Evans Schwartz’ story “The Fate of the Riemann Hypotesis”, available here.


Received 12 October 2026.

Filed under
More by →

3 responses to “Lean me softly: A satire about a dystopian future for mathematics.”

  1. Nilima Nigam Avatar
    Nilima Nigam

    Thank you! I enjoyed this very much. In these turbulent times, an unexpected silver lining (for me) is discovering just how many mathematicians are gifted writers and storytellers.

    Just outside the gigantic auditorium in your telling, there’s a scanner that probes the brainwaves of audience members as they leave the seminar. If the light blinks green, the audience member gets a green sticker certifying ‘incipient understanding’. This certifies a person looked up the QR code and read the first three sentences of the abstract.

  2. Anonymous Avatar
    Anonymous

    Thank you, this is a brilliant story. To outsiders it will look like satire, but this is exactly the future that Silicon Valley wants!

    It is already implemented today in Amazon warehouses and some software development organizations.

  3. Oliver Braunling Avatar
    Oliver Braunling

    Excellent! I hope Token Credit will read this.

Comments are moderated. Read our comment policy.

Add to the discussion

New posts by email.

Prefer a feed reader? Subscribe by RSS.

Also on Mathstodon.

Latest comments across the site.

  1. I think that’s an exaggeration to invoke urgency to establish some new norms. The OP clearly wants to feed his...

  2. I just learned of a paper, “The Alien Space of Science.” https://arxiv.org/abs/2603.01092 This is the closest thing I’ve found to...