A new equation

There are two age-old laments about mathematics which persist to this day. The first is that either ourselves or someone we know will express that they are not a math person — an admission that we are not good at math, or that somehow we are not hardwired for it. But we don’t tend to admit the same for reading, writing, child rearing, cooking or other skills that we deem inherent to the human experience.

The second lament is one that asks why we even learn math. “We’ll never use this in the real world,” goes the saying, particularly within the context of pre-calculus mathematics or calculus itself.

Both of these laments are regrettable, and most certainly need to be corrected by the public education system. Because, as author Kevin Hartnett argues in his latest work, The Proof in the Code: How a Truth Machine is Transforming Math and AI, mathematics is not only the language of the universe, but also a pathway to learning how to reason and seek truth.

Mathematics, ergo, is the language, both the physical and the metaphysical.

Harnett, who contributes to the Atlantic, Scientific American and the Boston Globe, sets out to tell the story of why mathematics is so critical to the human experience through the unlikely but inspiring coming together of the computer science and mathematics communities.

The story begins with Leo de Moura, a Brazilian-born computer scientist working for Microsoft over a decade ago, who wanted to build a program that would help him debug and verify developmental software.

The program was called Lean, and to de Moura’s dismay, it was mathematicians such as Tom Hales — who famously discovered a proof for Kepler’s Conjecture from 1611 (how many balls can you cram into a given space) — who saw the power of computer- assisted mathematics initially.

Hales released his massive proof in 1998, but the math community was unable to verify his results, given the complexity. Computers were needed to help confirm the results, to verify truth. Truth provers, if you will, had cracked open the door.

Over the course of the next decade, an open-source motley crew of mathematicians began to help de Moura develop Lean in order to formalize mathematical proofs and change the field. The development of Lean, an interactive theorem prover (or ITP), was not a top-down affair. Rather, it was developed democratically through contributors all over the world.

Mathematics was shifting from an isolated experience to one where thousands could contribute to MathLib, Lean’s repository for all mathematical knowledge. As Harnett highlights, the contributors were “bumping into each other almost by chance in the Gitter chat and helping each other gain a foothold in this new world.” As he posits, “Coming into the Lean community was more like entering a frontier town.”

And this serendipity created two truths. One was that de Moura began to resent the demands and often self-interested goals of PhD students or those seeking ambition. He would soon back away from the day-to-day support of Lean — not only fearing that Microsoft would clip his wings, but also because he was still clinging onto the goal of Lean as a software verifier.

The second truth, as Harnett argues, is that “people look for new tools when they have problems the old ones can’t solve.” Human mathematical reasoning has become so complex that chalkboards and scraps of paper no longer will suffice. Nor will working in solitude. As the mathematicians in The Proof in the Code contend, mathematics is not created, it is discovered.

Harnett’s inquiry highlights that as this discovery of the language of the universe becomes both broad and narrow, humans need new intellectual vessels to reach new territory.

Enter artificial intelligence (AI).

As the third and fourth generations of Lean were created in the early 2020s, AI companies and oligarchs began to take interest in Lean and other ITPs. DeepMind, the AI company that created the first robot to play and win at Go, picked up the torch first, entering the first AI to compete in the International Mathematics Olympiad in 2024 — and garnering a silver medal.

The trick for AI developers, however, is to create an AI that doesn’t mimic, but rather can reason, mathematically. While the integration of AI into ITPs is still in its infancy, the jury is out as to the cost-benefit analysis on the development, and the impact on our species.

But the message behind The Proof in the Code is one of hope for our species and the importance of seeking truth — hope in the sense that when humans come together with a common goal, they can achieve astounding feats.

The other message is that we all need various languages to discover the universe. We all, and particularly children, desperately need the chance to discover the language of mathematics so that we may better understand just how precious the universe, and the life within it, is.

The Proof in the Code demonstrates the power in collaboration, collective interest, intellectual rigour and the pursuit of truth — perhaps the simple ingredients for a better world.

Matt Henderson is superintendent of the Winnipeg School Division.