Kristina Armitage/ Quanta Magazine

n ancient Greece, Euclid showed that if you agree on a small list of preliminary principles, or axioms, you can use deductive reasoning to reveal all sorts of new mathematical truths. But although these early proofs, as mathematicians call them, were derived using the laws of logic, they sometimes also contained hidden, unstated assumptions or relied on misleading intuitions. In these cases, small gaps in a proof might go unnoticed; one couldn’t say with absolute confidence that it was correct.

Over the past few centuries, mathematicians have sought to close those gaps. By the early 1900s, they settled on the axioms they wanted to use. They also introduced different logical systems and standards in an effort to further “formalize” their arguments — to guarantee that, if you made every deduction in a proof explicit, its conclusion would have to be true no matter how long and convoluted it got.

Ad for Quanta's Math Series "The Evolving Foundations of Math"

This formalization effort engendered trust. But it did far more than that. The push to formalize has helped mathematicians uncover novel connections between different areas of math. It has taken the field in unexpected new directions. It has taught us, said David Bressoud of Macalester College in Minnesota, that “you often don’t know what you don’t know. And to be humble about that.”

But big advances in mathematics inevitably require bold ideas. These often come from experimentation and intuition — from exploring novel mathematical worlds and testing out novel theories, even if you can’t prove that every step in the journey logically follows from the last. It’s a less formal way of doing math that at first tends to contain mistakes.

It’s not easy to strike a fruitful balance between the creativity needed to paint new mathematical landscapes and the rigor necessary to ensure that the resulting pictures are true. Sometimes, formalization can upset that balance. What some mathematicians see as a move toward greater certainty, others might see as pedantry or a barrier to progress.

Euclid’s Elements marked the first major effort to formalize mathematics in the West. It established a deductive method for proving statements that’s still used today. Above, pages from the first printed edition of the work, made in 1482.

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.

As with past attempts to formalize math, Lean has generated mixed feelings. Some mathematicians look forward to offloading tedious verification work onto computers and see Lean as a potentially transformative new way of doing mathematics. Others think that their time and resources are better spent elsewhere — or, worse, that a Lean-centric approach will distort the true value of mathematics. It’s a discussion that’s starting to play out in the hallways of math departments around the world: How do we balance the creativity needed to discover new mathematical connections with the rigor needed to ensure that every logical step is undeniable?

A major milestone in the quest for rigor came about because of hidden problems with one of the most important mathematical achievements of all time.

In the late 17th century, Isaac Newton and Gottfried Leibniz independently developed calculus, a technique for understanding how quickly a function changes at a given point. But in an informal sense, calculus had already been around for centuries. In fact, Archimedes was doing something like calculus in the third century BCE. To calculate the area of a circle, he first studied the areas of shapes with straight sides called polygons. By using polygons with more and more sides, he was estimating a limit: the area of the circle. Newton and Leibniz took a similar approach, using limits to understand change.

In his treatise On Conoids and Spheroids, seen here in an 1897 translation, Archimedes introduced ideas that would play a key role in the development of calculus millennia later.

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.