The Quest for Perfect Proofs: Can Computers Bring Too Much Rigor to Math?

The search for absolute certainty in mathematics has a long history. Today, mathematicians are working on an enormous project: to rewrite all of mathematics into a computer program called Lean. This effort to create perfectly logical, machine-checked proofs is the latest chapter in a centuries-old story about balancing creativity with precision.

In ancient Greece, Euclid showed that by starting with a few basic rules, or axioms, one could use logic to discover new mathematical truths. However, these early proofs, while logical, often skipped steps or relied on intuition. These gaps could hide mistakes, making it hard to be completely sure a proof was right.

For hundreds of years, mathematicians have tried to remove these ambiguities. By the early 1900s, they had established a standard set of axioms and logical systems to "formalize" arguments. The goal was to guarantee that if every single logical step in a proof were written out, the conclusion would be undeniably true, no matter how complex the argument.

Today, mathematicians are attempting their most ambitious formalization project yet. They're aiming to rewrite all of mathematics in a computer language known as Lean, which can then automatically verify their proofs. Writing a proof in Lean requires an enormous amount of time and effort, but so far, the program has been used to verify more than 260,000 theorems. It has the potential to put mathematics on the most solid foundation one can imagine.

This drive for formalization built trust and had other benefits. It revealed new connections between different areas of math, guided research in surprising directions, and taught intellectual humility. As mathematician David Bressoud notes, it shows that "you often don't know what you don't know."

Calculus immediately became useful throughout math and physics. But it was not formal by modern standards: Leibniz's and Newton's papers glossed over some ambiguities. Calculus relies on the notions of infinity and infinitely small quantities (called infinitesimals), but Newton and Leibniz defined these concepts in vague geometric terms; used incorrectly, their formulas could lead to nonsensical calculations, like division by zero.

Yet major breakthroughs in math often come from bold, creative ideas born from experimentation and intuition. Mathematicians frequently explore new concepts and test theories before every logical step is fully justified. This less formal approach is more likely to contain errors at first. Finding a good balance between the creativity needed for discovery and the rigor needed for verification is a constant challenge. Some see formalization as a path to greater certainty, while others view it as overly strict or even obstructive.

Renowned mathematicians such as Niels Abel, Augustin-Louis Cauchy, and Karl Weierstrass realized that to make sense of the bizarre sums and curves that were cropping up in their work, they needed to return to their most fundamental definitions. What is a function? What does it mean for a function to be continuous? What really happens when you add up infinitely many objects?

Still, some researchers also faced this new wave of formalization with trepidation. "It is not easy to get up any enthusiasm after it has been artificially cooled by the wet blankets of the rigorists," the physicist Oliver Heaviside wrote in 1899.

As with past formalization efforts, Lean gets mixed reactions. Supporters hope to let computers handle tedious verification and dream of a transformative new method. Critics argue that time and resources are better spent elsewhere, or worry that a focus on Lean could distort the true value of mathematics. A key debate is emerging: How do we balance the creative discovery of new mathematical ideas with the rigorous checking of every logical step?

A major push for rigor came from hidden problems within one of math's greatest achievements: calculus.

In the late 1600s, Isaac Newton and Gottfried Leibniz independently invented calculus, a framework for analyzing rates of change. Their work was informal by today's standards. Calculus uses ideas of infinity and infinitely small quantities, which Newton and Leibniz described with imprecise, geometric language. If misused, their methods could produce nonsense, like dividing by zero.

For 150 years, this wasn't a big practical problem, as people learned which applications worked. However, the early 1800s introduced strange new concepts—like infinite series and bizarre, discontinuous curves—that broke conventional intuition. This period also saw a broader cultural shift that was skeptical of intuition in both arts and sciences. "Intuition is suspect," says historian Alma Steingart. "There is this feeling that intuition can lead you the wrong way."

Mathematicians like Niels Abel, Augustin-Louis Cauchy, and Karl Weierstrass realized that to understand these new objects, they needed to return to basic definitions. They created precise, formal definitions for concepts like function, continuity, and the limit of an infinite sum. Weierstrass's epsilon-delta definition of a limit is still used today. This formalization allowed for a deeper, more rigorous study of functions, leading to the field of mathematical analysis.

Analysis is now a cornerstone of math. It is essential for modeling everything from fluid flow to stellar chemistry and is deeply connected to number theory and geometry. The formalization of calculus also helped create set theory, which provides the foundational rules for modern mathematics.

Still, this new rigor caused concern. Physicist Oliver Heaviside complained in 1899 about the difficulty of generating "enthusiasm after it has been artificially cooled by the wet blankets of the rigorists." A crucial compromise was found. Mathematicians adopted the rigorous frameworks, but also developed methods that let scientists like Heaviside calculate freely. The push for formalization was driven by specific problems, not just an abstract desire for order. As David Hilbert noted in 1905, scientific development is organic: researchers first find "comfortable spaces to wander" and only later strengthen the foundations as needed.

It is possible to prioritize clarity and rigor to a harmful degree, as shown by the influential and controversial Bourbaki school.

In the mid-1930s, a secret society of French mathematicians named Bourbaki formed to update their country's outdated math education. Their project grew into a multi-volume treatise covering huge areas of mathematics. Bourbaki's lasting legacy is its unique style: an extreme focus on abstraction. The group avoided concrete examples and intuitive explanations, presenting math as a sequence of pure logical deductions from general axioms.

"It's a style that is very formal," said historian Leo Corry. "Very austere." This philosophy deeply shaped 20th-century mathematics, making it more airtight but also more abstract and difficult. Supporters say this abstraction reveals essential structure. "You are forced to understand what really makes things work, and what is just noise," said mathematician Patrick Massot.

However, Bourbaki's approach had significant unintended effects. Its style was poorly suited to concrete, visual fields like combinatorics and graph theory, which were sidelined for decades in places influenced by Bourbaki. "Graph theory [was] the slum of topology," remarked mathematician Béla Bollobás.

Even in compatible fields, some believe Bourbaki's success led to a problematic homogenization. "There is a sense that it decreased the cultural diversity of mathematics," said Aravind Asok. For example, the vibrant but less rigorous Italian school of algebraic geometry faded, leaving one dominant method. While this increased reliability, it may have also closed off other paths to progress.

Despite centuries of work, fully formal proofs remained theoretical until computers arrived. Since the 1960s, researchers have built "proof assistants"—programs that let mathematicians write proofs in a code-like language, which the software checks for logical consistency. If a single step is wrong, the proof fails.

The current leader of this movement is Lean. A community of mathematicians is building a comprehensive digital library, containing over 120,000 formal definitions and 260,000 verified theorems. Maintaining this library requires full-time effort and has received significant funding.

Supporters like Alex Kontorovich call Lean "revolutionary." It breaks proofs into modules, allowing parts to be checked independently and reused—like engineers using pre-made parts instead of mining ore for every new project. Lean has also generated new mathematics. In 2021, a team used Lean to verify an extremely complex proof by Peter Scholze, confirming it was correct and even refining some of his original ideas.

"It forces you to think about mathematics in the right way," said Kevin Buzzard, a leading Lean supporter. "It forces you to become an artist." Buzzard is currently formalizing the proof of Fermat's Last Theorem, a famously long and intricate result.

Supporters also argue that Lean is a wise investment for a future with artificial intelligence, where automated theorem generation will need strong verification tools.

However, widespread use of Lean carries risks. Could it, like Bourbaki, subtly change what kinds of mathematics are considered valuable or possible?

A main concern is the loss of diversity. In Lean's system, every new proof can only use definitions and theorems already in its central library. This library must be perfectly consistent. Therefore, changing one definition can have a ripple effect, breaking proofs that used the old version. This is a challenge for a discipline that is, in the words of historian Stephanie Dick, "a moving, shifting beast, and the terms of it are changing all the time."

Past attempts to create comprehensive digital libraries, like the 1994 QED Manifesto, failed because people disagreed on foundational definitions and programming languages. "Everybody loves this idea in principle, but in practice, it's a nightmare," Dick said.

To prevent such disputes, a dedicated community governs Lean's library, deciding which definitions to include and how to write them—a process compared to Wikipedia's model. "It is really a community trying to do the best thing for the community," said Emily Riehl. While this democratic process has worked well so far, it centralizes a lot of authority. The ongoing challenge for mathematicians is to use the power of digital formalization without letting it limit the creative, intuitive, and diverse spirit that drives real discovery.