“It’s a very formal style,” said Leo Corry, a historian at Tel Aviv University. “Very austere.”
Bourbaki’s philosophy spread rapidly and influenced mathematics almost everywhere. “It had a huge influence,” said Patrick Massot of Paris-Saclay University. “The most successful parts have become so much a part of common mathematical knowledge and style that it’s hard to think of what they were before.”
The subject became much more hermetic, although increasingly abstract and difficult. “This was not a brilliant decision from a pedagogical point of view,” wrote Maurice Mashaal, long-time editor of for science and author of a book about Bourbaki. But the group’s emphasis on abstraction shaped research mathematics in ways that are harder to evaluate.
Some mathematicians revere Bourbaki’s approach. Massot maintains that through abstraction and elegance, “you are forced to understand what really makes things work and what is just noise.” From this point of view, formalization has provided clarity.
But Bourbaki’s project also had unforeseen consequences. His vocabulary and style were not naturally suited to all types 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 very concrete and visual. Perhaps, then, it is not surprising that for decades they have been marginalized in most of the prestigious institutions of the United States and parts of Europe; They were only able to prosper in places where Bourbaki’s influence was limited, such as Hungary.
“Graph theory (was) the slum of topology,” said Belá Bollobás of the University of Memphis. “That atmosphere changed only recently. Very recently.”
Even in fields that flourished under Bourbaki’s framework (algebra, topology, analysis), some mathematicians worry that Bourbaki has been too successful. According to them, the ways in which tests are written and theories are constructed have become too homogeneous.
“There is a sense that the cultural diversity of mathematics decreased,” said Aravind Asok of the University of Southern California. Before Bourbaki, for example, there were many versions of algebraic geometry. In France, for example, methods were based on 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 avenues of possible progress, Bourbaki introduced a new problem. “I don’t want any math where I dominate one mode,” Asok said. “There is a cultural history of mathematics that deserves to be preserved.”
Tests and promises
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 test assistants. Using a proof assistant, a mathematician will write each line of a proof (including all definitions) in a language the computer can understand, and then the proof assistant will verify the logic. If not even a single step follows the previous one (if you haven’t rigorously shown every little detail, such as the fact that 1 + 1 equals 2), then the program will not consider the proof correct.
Today, mathematicians hope to formalize all mathematics using a proof assistant called Lean. So far they have created a library of more than 120,000 definitions and verified a quarter of a million theorems. Various mathematicians maintain this database, keeping it up to date and examining new contributions. (A handful of them do this job full time.) They have received more than $10 million in funding, mostly from billionaire financier Alex Gerko.