| In principle, a mathematician can discover new truths just by sitting in a comfortable armchair, thinking really hard, and then writing out an argument step by step. This basic approach to devising proofs dates back more than 2,000 years (though armchairs are a more recent addition). But proofs aren't just for mathematicians, and in the past few decades theoretical computer scientists have developed radically new ways to think about them.
To a computer scientist, the key property of a proof is that it's easy to check whether the result is valid. For example, we often have computers tackle problems that would be too hard to solve by hand. In these situations, it would be nice to have some sort of rigorous guarantee — in other words, a proof — that the computer's solution really is correct. That's possible for many of the problems that computer scientists care about, but not all of them.
In the 1980s, a handful of computer scientists began to wonder how things would change if the computer's proof of correctness didn't have to be written down like an ordinary mathematical proof. Perhaps an interactive process could help them verify solutions to more problems? It's an appealing idea, rooted in the way real mathematicians persuade each other that their arguments are valid.
"You're interacting with your students, and they can ask you different questions," the computer scientist Tom Gur said when I talked to him last fall. "Maybe there is more power in that."
Indeed, researchers soon discovered that interactive proofs are a lot more powerful than ordinary ones — they can verify the solutions to much harder problems. But interactive proofs were just the beginning. In the decades since, computer scientists have reinvented the proof again and again. Their inventions have had profound impacts on other branches of math and computer science, and even quantum physics.
What's New and Noteworthy
The new types of proof often defy our intuition about how a convincing argument should work. With an ordinary mathematical proof, only a reader who understands the details of the argument can know for sure that it's valid. The reader must also digest the whole proof: An impatient reader who skips some steps might miss a flaw in the argument. It turns out that neither of these properties is actually necessary. In the 1980s, computer scientists invented the "zero-knowledge proof" — a way to prove that a statement is true without revealing anything about why it's true. A decade later, they invented "probabilistically checkable proofs," which can convince someone who only reads a few small snippets of the argument. Last year, three computer scientists finally figured out how to combine the ideal versions of these two proof techniques. A month after I wrote my article about this breakthrough, the team pushed their result even further.
After computer scientists discovered how powerful interactive proofs could be, they quickly moved on to more complex proof procedures involving interactions between more than two participants. It turned out that these "multi-prover interactive proofs" could verify solutions to harder problems still. But nothing prepared researchers for what they found when they extended their investigations to interactive proofs involving multiple quantum computers. Kevin Hartnett reported on their shocking 2020 discovery that these proofs can verify the result of any conceivable computation. That discovery turned out to have implications for seemingly unrelated questions in math and physics.
Another connection between computer science and mathematical proof has had a more direct impact on the practice of math research. Called the Curry-Howard correspondence, it's a precise equivalence between proofs and computer programs. Sheon Han broke down how it works in an explainer for Quanta. This link is the foundation for "proof assistant" programs that have helped mathematicians verify the correctness of their proofs. As my colleague Jordana Cepelewicz wrote in the March 25, 2024, issue of Fundamentals, proof assistants have opened up new ways for mathematicians to collaborate. They've also made the field more accessible for researchers without traditional academic backgrounds — my favorite story from last year chronicled one especially inspiring example. | 
