The real legacy of these books, however, is not their content but their style. Bourbaki prioritized abstraction over all else, eschewing concrete examples and calculations in favor of only the most general statements. They presented each proof as a series of logical deductions, usually without reference to any underlying intuition or rationale.
“It’s a style that is very formal,” said Leo Corry, a historian at Tel Aviv University. “Very austere.”
Bourbaki’s philosophy quickly spread, influencing mathematics almost everywhere. “It had an enormous influence,” said Patrick Massot of Paris-Saclay University. “The most successful parts have become so much part of the common mathematical knowledge and style that it’s hard to think of what it was before.”
The subject became far more airtight, if increasingly abstract and difficult. “This was not a brilliant decision from a pedagogical point of view,” wrote Maurice Mashaal, the longtime editor of Pour la Science and the author of a book on Bourbaki. But the group’s emphasis on abstraction molded research mathematics in ways that are harder to assess.
Some mathematicians revere Bourbaki’s approach. Massot argues that through abstraction and elegance, “you are forced to understand what really makes things work, and what is just noise.” Formalization, in this view, has brought clarity.
But Bourbaki’s project had unforeseen consequences as well. Their vocabulary and style weren’t a natural fit for every type of mathematics. For example, the fields of combinatorics (often described as the science of counting) and graph theory (the science of networks) tend to be highly concrete and visual. Perhaps, then, it’s no surprise that for decades, they were sidelined at most prestigious institutions in the United States and parts of Europe; they were only able to thrive in places where Bourbaki’s influence was limited, like Hungary.
“Graph theory [was] the slum of topology,” said Béla Bollobás of the University of Cambridge. “That atmosphere changed only recently. Very recently.”
Even in fields that did flourish under the Bourbaki framework — algebra, topology, analysis — some mathematicians worry that Bourbaki was too successful. According to them, the ways in which proofs are written and theories constructed have become overly homogeneous.
“There is a sense that it decreased the cultural diversity of mathematics,” said Aravind Asok of the University of Southern California. Before Bourbaki, for instance, there were many versions of algebraic geometry. In France, for example, methods were grounded in analysis, while in Italy, a geometric style reigned.
The Italian school, which lacked rigor and involved many errors, quickly faded as Bourbaki’s influence spread. Certainly, algebraic geometry became more reliable. But by cutting off other paths of possible progress, Bourbaki introduced a new problem. “I don’t want any mathematics where one mode dominates,” Asok said. “There is a cultural history to mathematics that deserves to be preserved.”
Despite the best efforts of Bourbaki, Cauchy, and Weierstrass, truly formal proofs have always been objects of theory, not practice. Some mathematicians now hope that computers can change that.
Since the 1960s, researchers have been developing computer programs called proof assistants. Using a proof assistant, a mathematician will write every line of a proof (including every definition) in a language that the computer can understand, and then the proof assistant will check the logic. If even a single step doesn’t follow from a preceding one — if you haven’t rigorously shown every tiny detail, like the fact that 1 + 1 equals 2 — then the program will not consider the proof correct.
Currently, mathematicians are hoping to formalize all of mathematics using a proof assistant called Lean. They’ve created a library of more than 120,000 definitions so far and have verified a quarter of a million theorems. Several mathematicians maintain this database, keeping it up to date and vetting new contributions. (A handful of them do this work full time.) They’ve received over $10 million in funding, mostly from the billionaire financier Alex Gerko.