In 1941, the Argentine writer Jorge Luis Borges imagined an infinite library. Its hexagonal galleries hold every possible book: every combination of letters, of every length. Somewhere on its shelves, then, lies the proof of every theorem, the answer to every question, the exact story of your life.
And yet the librarians of Babel are in despair. Everything is there, but nothing is readable. For every true page there are billions of false ones, and nobody knows which is which.
This week, OpenAI posted online 722 mathematical manuscripts produced by a machine. The Library of Babel is no longer fiction. The question it asked is back: what is the use of a truth no one reads?
What a proof is for
We often think a proof exists to show a statement is true. That is its most visible role. It is not the only one.
In 1994, the American mathematician William Thurston, a Fields medallist, published a famous essay on what mathematicians really do. His answer: they do not produce theorems, they produce understanding. A good proof does not just say "it is true". It says why, and that why often sheds light on other questions than the one being asked.
A proof that establishes a result without anyone understanding how is like an oracle. It gives the answer. It teaches nothing. It is a bit like knowing the score of a match you did not watch: you know who won, but nothing about the game.
Not the first time
Mathematicians have felt this vertigo before. In 1976, two researchers, Kenneth Appel and Wolfgang Haken, proved the four colour theorem: four colours are enough to colour any map so that no two neighbouring countries share one. But their proof relied on a computer checking hundreds of cases one by one. No human can redo it by hand. The debate lasted years: is it still a proof?
In 1998, Thomas Hales proved the Kepler conjecture, on the tightest way to stack oranges. After years of review, the experts checking his proof declared themselves "99% sure". Hales then launched a project to have every step checked by software. It was completed in 2014, sixteen years later.
Each time, the community eventually accepted these proofs. But each time, they remained the exception. What changes today is the scale.
Proof-checking software like Lean, used by OpenAI, guarantees that reasoning contains no logical error. That is a huge advance: it solves the problem of reviewers who are "99% sure". But it does not say whether a result is interesting, what it means, or whether it was already known. It answers "is it correct?", not "what does it teach us?".
The Fields medallists' fear
According to the specialist site The Decoder, twenty-five Fields Medal winners signed an open letter warning of a deep disconnect between the aims of the AI industry and those of mathematics. What they fear is not that a machine gets things wrong. It is that it gets them right, in bulk, and that this bulk gradually replaces the effort to understand.
The risk is concrete. If thousands of results arrive every month, who will have time to read them? Will young researchers spend their PhD years checking what machines produce, rather than learning to think?
The other side
There is another way to see it. Most theorems published each year are read by only a handful of specialists. Science has always produced more than it could absorb.
And a machine that clears tedious problems could instead free up time for what matters: looking for the why. Calculation by hand disappeared from laboratories without killing physics. It simply changed its questions.
The takeaway
The Library of Babel held every truth, and its readers were miserable. It was not space that was missing. It was meaning.
A machine can fill the shelves faster than we could ever browse them. The question is no longer whether it finds truths. It is whether we will keep the taste, and the time, to understand them.