How Software Is Transforming Mathematical Proofs

Software is now joining the process – uncovering errors that nobody could previously see.

For a long time, an unwritten rule applied in quiet offices filled with blackboards and notebooks: a proof was only as reliable as the finest minds in the field considered it to be. That period is now being shaken. Increasing numbers of leading researchers are having their theorems checked line by line by programs such as Lean, Coq and Isabelle. Solitary geniuses are becoming connected teams, while trust is giving way to logic that can be verified in code.

From the solitary genius to the connected project

For centuries, mathematical research followed much the same pattern. One person, or a small group, worked away at a problem, wrote down an idea for a proof and submitted it to an academic journal. Colleagues would then scrutinise it for months. At best, they found no gap; at worst, someone uncovered an error years later that undermined the entire result.

Peter Scholze, one of Germany's best-known mathematicians and a Fields Medal recipient, also felt this uncertainty. In 2018, he published a highly complex proof concerning so-called “compact spaces”, expressed in a new and exceptionally abstract form. Only a handful of people worldwide could follow it at all. Scholze himself could not be entirely certain that a tiny error in reasoning had not slipped in somewhere.

Rather than commission further reviews, he took a radically different route: he publicly launched the “Liquid Tensor Experiment”. The aim was for people familiar with the proof software Lean to try to formalise his reasoning completely in that language. This meant no more loosely written prose, but rigorously structured code that a machine could understand and check.

In this new setting, a theorem is accepted only when not just humans, but also a strict algorithm, approves every single line.

After around six months, an international team reported success. Roughly 180,000 lines of Lean code covered the complete argument, with no logical gap. For Scholze, this represented a different level of quality from any conventional peer review. For the wider community, it was a pivotal moment: a craft thousands of years old had suddenly become a collective, computer-assisted undertaking.

Software makes apparently “uncheckable” proofs manageable

Scholze's case did not remain an isolated one. Another prominent example is the Ukrainian mathematician Maryna Viazovska, who solved an age-old puzzle about the densest sphere packing in eight dimensions, a deeply abstract problem that had remained open for centuries. Her solution also earned her the Fields Medal in 2022.

The proof's structure was ingenious, but so dense that checking it manually in full would have taken years. A group of researchers therefore chose to translate the work into Lean. For months, they broke down every section into even smaller logical steps until the complete proof existed as a program. In 2024, the full code was published openly on GitHub, and the proof was then secured in a formal, machine-readable form as well.

This reveals the real disruptive potential of the technology: proofs once regarded as “too long”, “too technical” or “virtually impossible to verify” can suddenly be divided into workable sub-projects.

• Exceptionally extensive theorems can be split into many small components.
• Teams on several continents can work simultaneously on separate parts.
• At the end, the machine joins all the pieces of the puzzle and checks the overall logic.

Mathlib, Lean's large standard library, plays a central role here. It now contains more than a million lines of formalised definitions and proven theorems. Each new proof can build on this expanding foundation rather than having to express everything from scratch. This greatly speeds up projects and lowers the barrier to entry.

When the computer corrects Fields Medal winners

These programs do more than confirm proofs that are already correct. They also expose weaknesses that even specialists miss. In 2021, researchers formalised an already prize-winning result in Lean. The work was accepted within specialist circles, a prize had been awarded and its reputation was firmly established.

While translating the proof into code, Lean stopped at an intermediate construction: a necessary assumption was missing, so the logical chain was incomplete. Not one human review had previously noticed this inconsistency. The authors had to revise their argument and state it more precisely.

This illustrates the nature of these new tools. A human reader examining a 100-page proof may eventually become tired or skim past something out of habit, whereas software accepts no leap in reasoning. Every variable requires a clear definition, and every conclusion must be justified exactly. The result is fewer informal shortcuts and more robust, demonstrable logic.

The machine does not negotiate: it demands completeness – or simply refuses to approve the next step.

How Proof Assistants are changing everyday mathematics

For a long time, these systems were considered toys for theoretical computer scientists. Anyone wishing to use them needed programming knowledge, considerable patience and a certain capacity for suffering. That is now changing rapidly.

Modern interfaces and AI-supported assistants are removing a large share of the obstacles. Language models suggest Lean code when researchers describe part of a handwritten proof. Interactive environments show in real time whether a step is formally sound or whether hypotheses are still missing. Doctoral students can therefore learn step by step how to turn their ideas into precise code.

What Lean, Coq and Isabelle actually do

All of these tools belong to the category known as proof assistants. Their central principle is straightforward:

• Mathematical statements are converted into a strict formal language.
• The software works with a fixed set of logical rules and permitted rules of inference.
• Every stage of a proof must be traceable under those rules.
• If there is a leap or a gap anywhere, the proof process stops.

Rather than automatically “inventing” a complete proof, the programs support people as they construct one. They can suggest partial routes, check hypotheses or present alternatives when an approach reaches a dead end. At its best, this creates a dialogue between intuition on one side and formal rigour on the other.

Opportunities, risks and unresolved questions

The benefits are obvious: greater certainty that published results genuinely hold up; faster checking of extremely complex projects; and better traceability because every step is stated explicitly in code.

At the same time, a difficult question arises: how far should the community rely on this software? Will researchers eventually check only whether the computer reports “green”, without understanding every step themselves? Some already warn of a form of “autopilot mathematics”, in which only a small number of specialists understand the code behind the tools themselves.

There is also dependence on particular platforms and programming languages. Anyone building a career around Lean proofs is tying themselves to an ecosystem. What happens if the community moves to a different system one day? Such questions are appearing increasingly often in academic debate.

What changes for students and teachers

At many universities, courses on formal proofs and proof assistants are entering the curriculum. Alongside traditional proof strategies, students learn how to encode arguments formally. This sharpens understanding: anyone required to state every supposedly “obvious” claim explicitly quickly discovers where they had previously only had an intuition rather than a genuine grasp.

Teachers see this as an opportunity to create greater transparency. Exam questions could, for example, be accompanied by simple Lean scripts through which learners can test whether their approaches are logically rigorous enough. The often mysterious concept of a “proof” then becomes a clearly structured process that can be practised step by step.

What comes next: human creativity, machine rigour

Many researchers expect a division-of-labour model to become established over the coming years. People will develop new concepts, venture bold conjectures and sketch broad strategies. The detailed work will then begin in the proof assistant, supported by AI that recognises suitable patterns across millions of lines of existing code.

Especially at the frontier of knowledge, where proofs run to several hundred pages or thousands of lines of code, this combination could advance the discipline substantially. Projects previously considered “too risky” or “too laborious” will become more realistic. This could produce theories whose complexity goes far beyond what any one person could ever fully oversee, yet which are still regarded as secure because every line of formal logic is available for verification.

This also shifts the understanding of what a proof is in the first place. It is no longer merely an elegant paper in an academic journal, but a structure made up of text, code and collaboratively maintained libraries. The old image of the solitary genius at a desk is making way for connected teams working with software at the boundary of what can be mathematically proven.