It's a natural impulse to want to impose order on the world.

The New York City Street grid makes it much easier to know where you are, as opposed to a

city with a layout like London's or New Delhi or Tokyo.

But impose that order on, say, a forest.

You get an orchard, which is great for picking apples,

but it's less diverse, less interesting, less functional, less inspiring.

We're going to explore applying this same idea to the world of math,

where order and logic have to share space with inspiration and intuition.

Welcome to the Quantum Podcast, where we explore the frontiers of fundamental science and

math. I'm Samir Patel, editor-in-chief of Quantum Magazine.

We recently launched a new series that is going to run over the next few months,

the evolving foundations of math, and just published the latest piece in this series, which is about the concept of formalizing or imposing order on math,

what that means, its advantages and disadvantages, and where it's going next. I'm here today

with the author of that story, journalist Layla Sloeman. Welcome back to the show, Leila. Thank you.

So, Layla, what's the big idea? The impetus for this piece is that we're in a moment right now,

where it seems like computers might be able to start contributing to math in a really new way.

Computers have been useful for decades doing things like working through millions of computations that would take human beings forever to do.

But within the past decade, mathematicians have started using programming languages called proof assistance,

in which you can verify and write proofs. This has gotten quite a bit of media attention

lately, and it kind of invites this common belief about how math works, which is that

there's one right answer in math, and you verify that answer or you reach that

answer even through formal logic. But that's actually not how research works in mathematics.

...