Mathematics Just Changed Forever — Kevin Hartnett

“The Fields Medalist Peter Scholze proof was just sort of six pages of technical calculations that we had skimmed through at best. He'd become convinced that nobody had actually read his work.”

Claim: Peter Scholze believed that nobody had actually read his proof, which consisted of about six pages of technical calculations.

“We found four Fields medallists have actually proved theorems in the annals of mathematics. Strictly speaking, that theorem is not true.”

Claim: The speaker said that four Fields Medalists had proved theorems in the Annals of Mathematics, while noting that the theorem under discussion was not strictly true.

“The humans hadn't bothered to mention that obviously N had to be at least three.”

Claim: The humans had not stated that N had to be at least three.

“When you prove something using a tool like Lean, you can get certificates. You, you have an algorithm that can check whether the proof is correct or not.”

Claim: Lean can produce proof certificates that an algorithm can check for correctness.

“The machine says it's right, and something has now actually finally read it.”

Claim: A machine can check a proof and thereby provide a reader that verifies whether it is correct.

“AI is coming for mathematics. This is absolutely clear. Companies like OpenAI and Anthropic are doing mathematics and then just translating it into Lean.”

Claim: AI is increasingly being applied to mathematics, with companies such as OpenAI and Anthropic doing mathematics and translating the work into Lean.

“Mathematicians have had various different reactions to this, ranging from, you know, what could only be described as grief.”

Claim: Mathematicians have had varied reactions to AI's arrival in mathematics, including reactions resembling grief.

“Can I make a machine prove stuff? Sure. But I'm interested in understanding it, right? And I'm still the one who has to understand it.”

Claim: The speaker values understanding mathematical proofs and says that even if a machine proves something, he still has to understand it himself.

“And it can output, you know, millions of potential proofs, but you need to then quickly sort among them to the ones that are plausible or correct. Lean can tell you which ones those are.”

Claim: When a system generates millions of potential proofs, Lean can help identify which are correct, while plausible candidates still need to be sorted.

“But a checked proof can still be a proof of the wrong thing.”

Claim: Formal verification that a proof is correct does not ensure that it proves the intended statement.

“It's about the ideas, it's about the understanding.”

Claim: The speaker regards ideas and understanding as central to mathematics.

“You multiply two numbers on a calculator, you get a result. You just take the calculator's word for it. Nobody's gonna check it.”

Claim: People generally accept a calculator's result when multiplying two numbers without independently checking it.

“So four hundred years ago, when Johannes Kepler was in a greengrocer, he had an interesting idea. He was looking at the way the oranges were stacked on top of each other in a pyramid structure, and he thought that that might be provably the densest possible configuration.”

Claim: Johannes Kepler conjectured that oranges stacked in a pyramid might be the densest possible arrangement, roughly four hundred years ago.

“Unfortunately, it was impossible for him to know for sure whether his idea was correct. So fast-forward to about 1990.”

Claim: Kepler could not establish with certainty whether his proposed densest-packing arrangement was correct.

“This had become Kepler's conjecture. It was one of the most interesting problems in mathematics, and many famous mathematicians had spent decades trying to solve it, honestly, without making too much progress.”

Claim: By about 1990, Kepler's conjecture was a prominent mathematics problem that famous mathematicians had worked on for decades with little progress.

“Now, two mathematicians, Thomas Hales and Samuel Ferguson, they reduced it to seventeen hundred and sixty-two combinations.”

Claim: Thomas Hales and Samuel Ferguson reduced Kepler's conjecture to 1,762 combinations.

“Now, back in these days, computers were incredibly slow, so almost on a case-by-case basis, they had to write this insanely optimized computer program with lots of heuristics, doing intersection checking and so on, to individually prove that each one was less than about nought point seven four, which is the ratio of the optimum, uh, you know, pyramid placement.”

Claim: With computers then very slow, Hales and Ferguson used a highly optimized, heuristic-based program to check each case and show it was below approximately 0.74, the optimal packing ratio.

“Kevin Hartner tells this story in his brand-new book, Proof in the Code. Now, um, the book isn't just about oranges and, uh, Kepler's conjecture, but that's certainly where it starts.”

Claim: Kevin Hartnett's book Proof in the Code begins with the story of oranges and Kepler's conjecture but covers more than those topics.

“But, um, the, the thrust of the book is mostly about this gentleman called Leo de Moura, who is the creator of Lean, and the tumultuous and interesting, fascinating journey that he went on with many of his collaborators to get to where Lean is today.”

Claim: Kevin Hartnett's book mainly recounts Lean creator Leo de Moura's journey with collaborators in developing Lean.

“And he was saying how this guy, Thomas Hales, he actually had a bit of paper on his, on his wall, and every single one represented one of these configurations, and they became harder and harder as the density converged towards nought point seven four.”

Claim: Thomas Hales tracked each configuration on a piece of paper, and the cases grew harder as the packing density approached 0.74.

“And it took him many, many, many years to do this, and eventually he did it. So he had seventeen hundred and sixty-seven computer programs for every single configuration of these balls, and he was elated.”

Claim: Thomas Hales completed the work after many years, producing 1,767 computer programs for the configurations of the balls.

“So he published his work to the Annals of Mathematics, expecting a celebration that he had just, you know, proven Kepler's conjecture.”

Claim: Thomas Hales submitted his work to the Annals of Mathematics expecting recognition for proving Kepler's conjecture.

“He dumps this proof, um, on the journal-- on the editors of the Annals of Mathematics, the most prestigious journal in the field, and they essentially don't know how to referee it, how to kind of send it out to other mathematicians to verify its correctness, and it languishes for, like, many years without actually being kind of determined true or false.”

Claim: The Annals of Mathematics editors struggled to find mathematicians able to verify Hales's proof, leaving it unresolved for years.

“'Cause if you think about it, for many years, the way mathematical proofs were done were high up the abstraction mountain. So they would make these really high-level arguments, and it would just go without saying that certain arguments had been proved before, so you didn't need to go step by step, and it was very, very parsimonious.”

Claim: Traditional mathematical proofs often used high-level, concise arguments that omitted steps considered previously established.

“And when you submitted your paper to a journal, um, they would be able to review it, and they would be able to check your work. But this was different. The sheer volume of it made it almost impossible to check.”

Claim: The sheer volume of Hales's proof made it almost impossible for journal reviewers to verify, unlike more conventional mathematical papers.

“Every part of the proof that reviewers looked at seemed correct, but the proof as a whole was such a sprawling edifice of calculations, buried deep in computer code, and it was hard to determine how they all hung together and whether, in the end, they yielded the proof Hales claimed they did.”

Claim: Although reviewed portions of Hales's proof seemed correct, its sprawling computer-code calculations made it difficult to determine whether the complete proof established the claimed theorem.

“When Hales had finished the proof in the summer of 1998, he had imagined he would use the methods he had developed for Kepler to attack other similar problems.”

Claim: After completing the proof in summer 1998, Thomas Hales expected to apply its methods to other similar problems.

“That's how it goes in math. Methods that solve one hard problem are generally good for solving others. Yet as the review process dragged on without resolution, Hales changed his mind.”

Claim: Thomas Hales reconsidered applying his Kepler-proof methods to other problems as the review process remained unresolved.

“That's how it goes in math. Methods that solve one hard problem are generally good for solving others. Yet as the review process dragged on without resolution, Hales changed his mind.”

Claim: Mathematical methods that solve one difficult problem are generally useful for solving other problems.

“He couldn't get the math community to verify his proof of Kepler's conjecture. Why would he court frustration by applying the same methods to other problems?”

Claim: Thomas Hales was unable to get the mathematics community to verify his proof of Kepler's conjecture.

“The paper was accepted with a disclaimer saying something like, "We're ninety-nine percent confident this proof is correct." But then Tom started using proof assistants.”

Claim: Hales's paper was accepted with a disclaimer stating that the reviewers were 99 percent confident the proof was correct.

“This all happened before Lean. He used Holight and Isabelle to do this work. But it was a milestone.”

Claim: Before Lean, Thomas Hales used HOL Light and Isabelle to formalize this work, marking a milestone.

“I mean, it was a big result that has been formalized in proof assistants. And Tom was famous twice for solving the Kepler conjecture and for using a proof assistant in a paper that the math community cares.”

Claim: Thomas Hales became known for solving Kepler's conjecture and for formalizing a significant result with a proof assistant in a paper valued by the mathematics community.

“And the fact that he decided to do the next project using Lean was a big deal on Lean.”

Claim: Thomas Hales's decision to use Lean on his next project was significant for Lean.

“And the fact that he decided to do the next project using Lean was a big deal on Lean.”

Claim: End-to-end solutions from first principles can still feel unsatisfying because people incur an understanding debt when they cannot mentally grasp the entire proof at once.

“But the remarkable thing is that it still feels unsatisfying. Even if we can solve problems from first principles end to end, there's a kind of understanding debt because we can't hold it all in our brains at the same time.”

Claim: Solving problems from first principles end to end can still feel unsatisfying because people cannot hold all the relevant understanding in their brains simultaneously, creating what the speaker calls an understanding debt.

“So how do mathematicians know when a proof is correct, when they can trust a new theorem and then use that as an input into additional proofs? It's very much a social process.”

Claim: Mathematicians assess whether to trust a new theorem through a social process.

“They kind of have a general understanding for what works already. They kind of like know the person behind a proof. They can kind of like trust that this person kind of understands the way things should go.”

Claim: When assessing proofs, mathematicians often rely on their general understanding of established methods and on whether they trust the proof's author.

“And then they, you know, they can check a proof. They can check the kind of the lines and the argument, but they don't necessarily check every last line all the time.”

Claim: Mathematicians may review a proof's lines and argument without checking every line in every instance.

“And for the most part, that works, especially when proofs are kind of close to the existing body of knowledge, when they kind of go just incrementally beyond things we already understand to be true.”

Claim: Mathematicians' usual approach to checking proofs works for the most part when a proof is close to existing knowledge and extends it incrementally.

“Well, I think the main thing is that we can, when you prove something using a tool like Lean, you can get certificates.”

Claim: Using a tool such as Lean to prove a result can produce certificates.

“You have an algorithm that can check whether the proof is correct or not. For math, for example, this is useful for trust. I mean, you can collaborate with people you never have met.”

Claim: An algorithm can verify whether a mathematical proof is correct, supporting trust and collaboration with people who have never met.

“I think many people in the math community got excited about that, even before AI. It's like saying, oh, wow, I can work even with high schoolers and they can contribute to my project.”

Claim: Even before AI, many people in the mathematics community were excited that formal proof checking could let them collaborate with contributors such as high school students.

“I don't need to check if their proofs are correct or not. A big math project you can view as engineering projects. I mean, Johan Commelin, for example, he's a really hardcore mathematician and he's a software engineer.”

Claim: Johan Commelin is both a mathematician and a software engineer.

“I don't need to check if their proofs are correct or not. A big math project you can view as engineering projects. I mean, Johan Commelin, for example, he's a really hardcore mathematician and he's a software engineer.”

Claim: A large mathematics project can be organized and understood as an engineering project.

“He doesn't know, but he's a software engineer. He breaks big projects in smaller pieces and people can fill the smaller pieces. He's like the architect of the project and people start filling the holes and he doesn't need to check manually, right?”

Claim: Johan Commelin organizes large projects by dividing them into smaller pieces for others to complete, so he does not need to check each piece manually.

“Of course, he will look later for, to see if people can maintain this proof later. But you don't have to keep thinking about is this, the proof is correct or not. He knows the proof is correct.”

Claim: Johan Commelin later checks whether other people can maintain the proof.

“people can maintain this proof later. But you don't have to keep thinking about is this, the proof is correct or not. He knows the proof is correct.”

Claim: Formal proof checking can provide assurance that a proof is correct, so its organizer need not continually question its correctness.

“He can clean up, improve, but the proof is correct. This is valuable.”

Claim: A formally checked proof can be refined after verification, while retaining the value of its established correctness.

“We want provenance. We want to know why, right? And that's the thing that I'm much more interested with if you want to talk about symbolic AI. The thing that's interesting is I don't want merely things that don't get it wrong because like that's still not enough.”

Claim: For symbolic AI, the speaker values provenance and explanations of why an answer was produced, not merely avoiding incorrect answers.

“I want to know why it comes up with a particular answer. I want the reason.”

Claim: The speaker wants systems to provide reasons for their particular answers.

“Thomas Hales' proof was extremely verbose. It was complex. He was going through on an instance-by-instance basis, and it wasn't very abstract like the proofs that came before.”

Claim: Thomas Hales' proof was highly verbose and complex, handled cases instance by instance, and was less abstract than earlier proofs.

“And does that remind you of anything? Yes. If you look at AI proofs now, they have a similar property, right? They are, they look a bit like spaghetti and they're inscrutable to us, and that doesn't give us a very satisfying feeling.”

Claim: The speaker says current AI-generated proofs resemble Hales' proof in being spaghetti-like and inscrutable to people, which feels unsatisfying.

“Well, it's not less legitimate because he settled the question. I think one thing that, one way in which you can kind of like assess the value of a new mathematical result is it like, does it enable additional results?”

Claim: One way to assess the value of a mathematical result is to ask whether it enables further results.

“Do you invent new concepts, new abstractions, new definitions in the process of prosecuting an argument that then have like widespread utility for answering other questions?”

Claim: Another way to assess a mathematical result is whether its argument creates concepts, abstractions, or definitions with broad utility for answering other questions.

“And in Hales' case, I mean, there were some computational methods that he would have wanted to apply to other problems, but he was not inventing kind of like broadly new mathematics.”

Claim: Thomas Hales used computational methods that he would have wanted to apply to other problems, but his work did not create broadly new mathematics.

“In a certain sense, the techniques he used were like fairly elementary. He himself kind of acknowledges that. So he was not creating new math in the same way that like Andrew Wiles had to create new math when he solved Fermat's Last Theorem, where he had to like invent some very like powerful new concepts that just opened up entirely new branches of the field.”

Claim: Andrew Wiles' solution of Fermat's Last Theorem required powerful new concepts that opened entirely new branches of mathematics.

“In a certain sense, the techniques he used were like fairly elementary. He himself kind of acknowledges that. So he was not creating new math in the same way that like Andrew Wiles had to create new math when he solved Fermat's Last Theorem, where he had to like invent some very like powerful new concepts that just opened up entirely new branches of the field.”

Claim: Thomas Hales' techniques were fairly elementary, a characterization he himself acknowledged.

“So Hales' proof was not like that.”

Claim: Thomas Hales' proof did not involve the kind of creation of powerful new mathematical concepts attributed to Andrew Wiles' solution of Fermat's Last Theorem.

“There's utility probably in the generation of proofs that are not constrained by our desire for interpretability. But once you talk about like doing actual mathematics, like that's, I'd like, I still like to think that, you know, the human understanding is still center in this. It may not be, but I think those are different quests at some point. It's like, can I make a machine prove stuff? Sure. But I'm interested in like understanding it, right?”

Claim: The speaker still regards human understanding as central to doing mathematics, while acknowledging that this may not remain the case.

“There's utility probably in the generation of proofs that are not constrained by our desire for interpretability. But once you talk about like doing actual mathematics, like that's, I'd like, I still like to think that, you know, the human understanding is still center in this.”

Claim: The speaker thinks there is probably value in generating proofs without requiring them to be interpretable.

“It may not be, but I think those are different quests at some point. It's like, can I make a machine prove stuff? Sure. But I'm interested in like understanding it, right?”

Claim: The speaker is more interested in understanding machine-produced proofs than simply establishing that a machine can prove things.

“And I'm still the one who has to understand it.”

Claim: The speaker believes they still need to understand a proof themselves.

“There is resistance because mathematicians don't see by and large or didn't see the value in that type of time investment. So Hales invests 20 person years in formalizing his Kepler conjecture result.”

Claim: Mathematicians have resisted formal proof formalization because they have not seen sufficient value in the time investment; Thomas Hales spent 20 person-years formalizing his Kepler conjecture result.

“And at the end, all he gets out of it is assurance that the thing is correct. Now that is like, that's much less exciting than getting new math and new discoveries.”

Claim: Thomas Hales' 20 person-years of formalizing his Kepler conjecture result yielded assurance of correctness, which the speaker considers less exciting than new mathematics and discoveries.

“It's especially not exciting in situations where you're already fairly confident that things are correct. So in most cases, mathematicians know when things are right or not. They're not troubled by correctness.”

Claim: The speaker says mathematicians generally know whether mathematical results are correct and are not troubled by correctness.

“It's especially not exciting in situations where you're already fairly confident that things are correct. So in most cases, mathematicians know when things are right or not. They're not troubled by correctness.”

Claim: The speaker considers formal verification especially unexciting when mathematicians are already fairly confident that a result is correct.

“There's a ratio called the De Bruijn ratio, which is the amount of lines of code you need to write in Lean for every one line of informal math, like in a LaTeX PDF.”

Claim: The De Bruijn ratio measures how many lines of Lean code are needed per line of informal mathematics in a LaTeX document.

“And it's very high, 20 to 1, often higher. Mathematicians don't generally see the reason to invest that additional time just to verify the correctness of something.”

Claim: Mathematicians generally do not see sufficient reason to spend the additional time required solely to verify a result's correctness.

“And it's very high, 20 to 1, often higher. Mathematicians don't generally see the reason to invest that additional time just to verify the correctness of something.”

Claim: The De Bruijn ratio is often 20 lines of Lean code or more for each line of informal mathematics.

“So that's really where the resistance comes from. They don't see the utility of Lean for the thing they most care about, which is discovering new math.”

Claim: Mathematicians' resistance to Lean stems from not seeing how it helps with their primary goal of discovering new mathematics.

“Oh, Lean is both a programming language and a proof assistant. You can write codes. Lean is actually implemented in Lean itself. Uh, uh, but the cool thing is that you can prove properties about your codes.”

Claim: Lean is both a programming language and a proof assistant, and its implementation is written in Lean.

“Oh, Lean is both a programming language and a proof assistant. You can write codes. Lean is actually implemented in Lean itself. Uh, uh, but the cool thing is that you can prove properties about your codes.”

Claim: The Lean programming language is implemented in Lean itself.

“Oh, Lean is both a programming language and a proof assistant. You can write codes. Lean is actually implemented in Lean itself. Uh, uh, but the cool thing is that you can prove properties about your codes.”

Claim: Lean is a programming language and a proof assistant.

“Oh, Lean is both a programming language and a proof assistant. You can write codes. Lean is actually implemented in Lean itself. Uh, uh, but the cool thing is that you can prove properties about your codes.”

Claim: Lean allows users to prove properties about code.

“Oh, Lean is both a programming language and a proof assistant. You can write codes. Lean is actually implemented in Lean itself. Uh, uh, but the cool thing is that you can prove properties about your codes.”

Claim: Lean lets users write code and prove properties about the code.

“You can state mathematical theorems. You can prove them. You can build a mathematical library like the Lean math lib.”

Claim: Lean allows users to state and prove mathematical theorems and build mathematical libraries such as Mathlib.

“You can state mathematical theorems. You can prove them. You can build a mathematical library like the Lean math lib.”

Claim: Lean lets users state and prove mathematical theorems and build mathematical libraries, including Mathlib.

“An interactive theorem prover has two basic components, a logical foundation, which determines how ideas are expressed and interact with each other, and a checker program, called a kernel, which verifies that programs correctly adhere to the rules of the logical foundation.”

Claim: An interactive theorem prover consists of a logical foundation governing expression and interaction of ideas, and a kernel that checks whether programs follow the foundation's rules.

“The kernel answers the first question anyone asks when they learn about an ITP, which is that if the ITP says a proof is correct, how do I know it hasn't made a mistake? The kernel is how.”

Claim: An interactive theorem prover's kernel is the mechanism used to check that a proof reported as correct has not been accepted due to a mistake.

“We have the notion of a small trusted kernel. Uh, Lean's massive, has zillions of bugs, right? But to trust our results, uh, in Lean, you only need to trust the kernel.”

Claim: Although Lean has many bugs, trusting Lean's results requires trusting only its kernel.

“The cardinal sin for a kernel is to verify false statements as true, which is far worse than rejecting true statements as false.”

Claim: A kernel's more serious failure is accepting a false statement as true rather than rejecting a true statement as false.

“Calling true statements false merely creates a roadblock. It's an inconvenience. But calling false statements true opens the door to validating countless more false statements, all justified by the original false claim.”

Claim: A kernel that rejects a true statement creates a roadblock, whereas accepting a false statement as true can justify validating many additional false statements.

“At that point, the ITP is useless until the bug in the kernel is fixed. Over the years, ITPs such as Agda, Coq, and Isabelle had all contained bugs in their kernels that allowed users to validate false statements.”

Claim: Agda, Coq, and Isabelle have each had kernel bugs that allowed false statements to be validated.

“At that point, the ITP is useless until the bug in the kernel is fixed. Over the years, ITPs such as Agda, Coq, and Isabelle had all contained bugs in their kernels that allowed users to validate false statements.”

Claim: If a kernel bug allows false statements to be validated, the interactive theorem prover is useless until that bug is fixed.

“His answer was independent checking. Let users build their own kernels. To make this option realistic, de Mora knew he would need to keep the kernel as small and minimalistic as possible, comprising as few lines of code as he could possibly achieve.”

Claim: De Mora proposed independent checking through user-built kernels and aimed to make the kernel as small and minimal as possible to make that approach practical.

“Among the ITPs already on the market, de Mora admired the minimality of HOL Light, which had a very small kernel. Back in 2006, there was loads of duplicate effort at Microsoft.”

Claim: De Mora admired HOL Light for its minimal design and very small kernel.

“Among the ITPs already on the market, de Mora admired the minimality of HOL Light, which had a very small kernel. Back in 2006, there was loads of duplicate effort at Microsoft.”

Claim: In 2006, Microsoft had substantial duplicated effort, with some people building theorem provers and others working on obsolete ones.

“Some were building their own theorem provers, some were working on obsolete theorem provers, and it was at that point that Leo decided to start working on Z3.”

Claim: Leo began developing Z3 during a period of duplicated theorem-prover work at Microsoft.

“Leo built Z3 in order to provide a systematic way of checking that software had no bad pathways. Um, and he could kind of do it in, in the style of a mathematical proof.”

Claim: Leo built Z3 to systematically check software for bad pathways using a method resembling mathematical proof.

“Like, he could kind of prove with Z3 where you construct, you construct a pathway through the software as a series of variables, and you prove that those variables can never take the right combination of values that would make a statement, uh, true.”

Claim: Z3 can model a software pathway as variables and prove that the variables cannot take a combination of values that would make a specified statement true.

“And if you prove that it cannot take, the software cannot arrive at that state, that set of variables, then you just have ruled out categorically a bug, at least in this, like, one particular direction.”

Claim: Proving that software cannot reach a specified state rules out a bug along that particular pathway.

“Le- Leo built Z3 as a way to automatically check different pathways through Microsoft software for bugs, prove, guarantee that there were no bugs.”

Claim: Leo built Z3 to automatically check pathways through Microsoft software for bugs and provide a guarantee that no bugs were present.

“Z3 is a type of program called an automated theorem prover, because all of this work, once you set things up, is done automatically. The- there's not a lot of human input at that point.”

Claim: Z3 is an automated theorem prover that performs its work automatically with little human input once configured.

“Z3 was quite powerful. It caught lots of bugs and saved Microsoft hundreds of millions of dollars in the early 2000s. Leo, though, following the great success of Z3, not just for Microsoft, but, like, he and his collaborator entered it into these automated theorem prover comp- competitions where all the ATPs from all over the world come together, and they're given a bunch of problems and a set amount of time, and whichever ATP can kind of correctly prove true or false for those problems, uh, most accurately wins.”

Claim: In the early 2000s, Z3 caught many bugs and saved Microsoft hundreds of millions of dollars.

“Z3 was quite powerful. It caught lots of bugs and saved Microsoft hundreds of millions of dollars in the early 2000s. Leo, though, following the great success of Z3, not just for Microsoft, but, like, he and his collaborator entered it into these automated theorem prover comp- competitions where all the ATPs from all over the world come together, and they're given a bunch of problems and a set amount of time, and whichever ATP can kind of correctly prove true or false for those problems, uh, most accurately wins. Z3 was the world champion at. So he essentially had climbed to the top of the automated theorem prover mountain. But he also was disfa- dissatisfied with the, kind of the fundamental limitations of automated theorem prover technology.”

Claim: Z3 became the world champion in automated theorem-prover competitions.

“Z3 was the world champion at. So he essentially had climbed to the top of the automated theorem prover mountain. But he also was disfa- dissatisfied with the, kind of the fundamental limitations of automated theorem prover technology.”

Claim: After Z3's success, Leo remained dissatisfied with fundamental limitations of automated theorem-prover technology.

“Like, there's just kind of a limited range of things that, uh, programs of that sort can prove. A limited range of knowledge that they can verify is correct, if you wanna go a little broader.”

Claim: Automated theorem provers can prove and verify only a limited range of claims and knowledge.

“And so he turns his attention to building a related but more powerful type of program called an interactive theorem prover, where you have a much richer expressive language.”

Claim: Leo turned to developing an interactive theorem prover, which offers a richer expressive language and greater power than an automated theorem prover.

“There's kind of just a wider range of truths you can try to encode and verify. And interactive in the sense that the human, uh, kind of a human user can, um, can nudge the program towards greater expressiveness.”

Claim: Interactive theorem provers support encoding and verifying a wider range of truths, with human users able to guide the program toward greater expressiveness.

“Uh, it makes it a much more powerful thing. So what my book is, is ultimately the story of how Lean, this interactive theorem prover that de Mora builds to verify the correctness of software programs in a richer way than he could with Z3. gets, in a sense, co-opted by mathematicians who see the potential in it, and for the first time an ITP breaks through into a more mainstream way of working at math.”

Claim: De Mora built Lean to verify software correctness more expressively than Z3, and mathematicians later adopted it, bringing an interactive theorem prover into more mainstream mathematical practice for the first time.

“But, um, in Lean, because it uses this dependent type theory, it can be used for solving many, many other problems in abstract mathematics, which are significantly more complex.”

Claim: Lean's use of dependent type theory enables it to address many significantly more complex problems in abstract mathematics.

“Jeremy Avigad, a mathematician and philosopher at Carnegie Mellon, has been corresponding with Leo for many years.”

Claim: Jeremy Avigad, a mathematician and philosopher at Carnegie Mellon, has corresponded with Leo for many years.

“I'm a mathematician by training, specifically a logician. Uh, and so, you know, what I like about logic is that it's somewhere between mathematics, computer science, and philosophy.”

Claim: The speaker values logic because it occupies a space between mathematics, computer science, and philosophy.

“I'm a mathematician by training, specifically a logician. Uh, and so, you know, what I like about logic is that it's somewhere between mathematics, computer science, and philosophy.”

Claim: The speaker is trained as a mathematician and specializes in logic.

“So here at Carnegie Mellon, my primary appointment is in the philosophy department. Proof assistants started just kind of as a hobby, just messing around with them because I thought they were interesting around the year 2000.”

Claim: Around 2000, the speaker began exploring proof assistants as a hobby because they found them interesting.

“So here at Carnegie Mellon, my primary appointment is in the philosophy department. Proof assistants started just kind of as a hobby, just messing around with them because I thought they were interesting around the year 2000.”

Claim: The speaker's primary appointment at Carnegie Mellon is in its philosophy department.

“I'm still trying to understand the alternatives, he wrote. I've been reading about all of these proof assistants and studying their implementations.”

Claim: De Mora said he was still evaluating alternatives by reading about proof assistants and studying their implementations.

“When I questioned the need for dependent types or any other feature, it's because I'm really impressed with HOL Light's design and implementation.”

Claim: De Mora questioned the need for dependent types and other features because he was impressed by HOL Light's design and implementation.

“In my opinion, it's the most elegant by far. He acknowledged that this perspective was at odds with Avigad's.”

Claim: De Mora regarded HOL Light as by far the most elegant option, a view that differed from Jeremy Avigad's.

“I understand Jeremy's point when he says HOL Light would be really inconvenient for doing abstract algebra. The design of Lean was being negotiated in real time.”

Claim: De Mora acknowledged Avigad's view that HOL Light would be very inconvenient for work in abstract algebra.

“I want to use higher-order logic. It's a simpler foundation, much easier to implement. And for many software verification tasks, it's enough, right?”

Claim: Higher-order logic is sufficient for many software verification tasks.

“I want to use higher-order logic. It's a simpler foundation, much easier to implement. And for many software verification tasks, it's enough, right?”

Claim: The speaker preferred higher-order logic because it has a simpler foundation and is much easier to implement.

“But for doing abstract mathematics, it's not.”

Claim: Higher-order logic is insufficient for doing abstract mathematics.

“It's important to have a good library, a math library. For verifying software, for example, cryptography, we need lots of math. Differential privacy is another example.”

Claim: A good mathematical library is important for software verification, including cryptography and differential privacy.

“Having a good mathematical library is important, even if you only care about software verification. And in my point of view, you have-- it's important to have users.”

Claim: Having users is important for a project or tool.

“Having a good mathematical library is important, even if you only care about software verification. And in my point of view, you have-- it's important to have users.”

Claim: A good mathematical library is important even for software verification alone.

“Jeremy as a user. I knew others would come and pay off. I mean, many people, many of my colleagues that work on cryptography, they say, for example, one of them is a former colleague of mine, Cedric Fournet. He uses Lean now. And he told me, look, the math lib, the Lean mathematical library, have the right abstractions I need for verifying cryptography, right?”

Claim: Cedric Fournet uses Lean and said Lean's mathematical library has the abstractions he needs to verify cryptography.

“Because of all the generality that having dependent type theory provided, we have a library that's more expressive, that has the right abstractions, is cleaner.”

Claim: The speaker says dependent type theory enabled Lean's mathematical library to be more expressive, cleaner, and equipped with the right abstractions.

“Yeah, it paid off long term. In the long term, it paid off. It was a lot of extra work at the beginning. And to get it right was also a lot of work.”

Claim: Adopting dependent type theory required substantial additional work initially and considerable effort to implement correctly.

“Yeah, it paid off long term. In the long term, it paid off. It was a lot of extra work at the beginning. And to get it right was also a lot of work. But I think it paid off.”

Claim: The speaker believes adopting dependent type theory paid off over the long term.

“Before starting the Lean project, um, I had worked in 2009 and 2010. I spent a sabbatical year working on the, the formalization of the Feit-Thompson theorem.”

Claim: Before starting Lean, the speaker spent a sabbatical year in 2009–2010 formalizing the Feit–Thompson theorem.

“Uh, and that is in a proof assistant known as Roc. Uh, and Roc is based on dependent type theory. Um, uh, before that I had worked with Isabelle extensively, which is a proof assistant based on, uh, on a simpler logical framework called simple type theory.”

Claim: Before working with Roc, the speaker worked extensively with Isabelle, which is based on simple type theory.

“Uh, and that is in a proof assistant known as Roc. Uh, and Roc is based on dependent type theory. Um, uh, before that I had worked with Isabelle extensively, which is a proof assistant based on, uh, on a simpler logical framework called simple type theory.”

Claim: The speaker used Roc, a dependent-type-theory-based proof assistant, to formalize the Feit–Thompson theorem.

“Um, Isabelle is a wonderful system. And so for many things, it's, it's absolutely ideal. It still to this day, um, has, uh, excellent automation, automated support.”

Claim: The speaker considers Isabelle excellent for many uses and says it continues to provide excellent automation.

“So for certain types of mathematics, it, it was really a great system. Um, but then for certain types of things, you hit a wall. So, um, in modern mathematics, mathematicians talk about algebraic structures, um, you know, axiomatically characterized.”

Claim: Modern mathematics widely uses algebraic structures characterized by axioms.

“So for certain types of mathematics, it, it was really a great system. Um, but then for certain types of things, you hit a wall. So, um, in modern mathematics, mathematicians talk about algebraic structures, um, you know, axiomatically characterized.”

Claim: Isabelle works well for some kinds of mathematics but reaches limitations for others.

“Um, they're really ubiquitous. There are these complex networks of algebraic structures, um, and simple type theory is just not good for that.”

Claim: Complex networks of algebraic structures are common, and simple type theory is poorly suited to representing them.

“And so after my year working with Roc, it became clear to me that this was the framework that was capable of, of doing that type of mathematics. Um, and I think other mathematicians who had experimented with Isabelle and other systems were coming to similar conclusions that to do the mathematics that they wanted to do, they needed this very expressive framework.”

Claim: The speaker believed mathematicians who had experimented with Isabelle and other systems were similarly concluding that their desired mathematics required a highly expressive framework.

“And so after my year working with Roc, it became clear to me that this was the framework that was capable of, of doing that type of mathematics. Um, and I think other mathematicians who had experimented with Isabelle and other systems were coming to similar conclusions that to do the mathematics that they wanted to do, they needed this very expressive framework.”

Claim: After working with Roc for a year, the speaker concluded that dependent type theory could support the mathematics he wanted to formalize.

“So the thing about dependent type theory is that it's very powerful, um, and very expressive. Um, but I like to quote, um, from, you know, the Spider-Man franchise, you know, with great power comes great responsibility.”

Claim: Dependent type theory is powerful and expressive.

“You know, the very powerful language, um, it's also very hard to implement. Uh, it can be more difficult to use. There are a lot of gotchas and kind of corner cases.”

Claim: The speaker says a very powerful language can be difficult to implement and use, with many gotchas and corner cases.

“Um, and so it was a more weighty and complicated and difficult framework. Um, and when Leo first started the project, he was aiming for simplicity, you know, a very simple, formal, you know, foundation.”

Claim: Leo initially aimed to build Lean on a simple formal foundation.

“Um, and so it was a more weighty and complicated and difficult framework. Um, and when Leo first started the project, he was aiming for simplicity, you know, a very simple, formal, you know, foundation.”

Claim: The speaker characterizes dependent type theory as a weighty, complicated, and difficult framework.

“Um, and so he needed convincing there that the trade-off was worth it. I think, you know, in the end he came around. I mean, now he's one of the, the biggest proponents of dependent type theory.”

Claim: Leo later became one of the strongest proponents of dependent type theory.

“Um, and so he needed convincing there that the trade-off was worth it. I think, you know, in the end he came around. I mean, now he's one of the, the biggest proponents of dependent type theory.”

Claim: Leo initially needed convincing that dependent type theory's benefits justified its added complexity.

“He, you know, um, um, you know, soon after he would say that, you know, it's, it's really beautiful. And so he, he recognized the benefits. Um, but again, coming, coming from the outside and, uh, uh, you know, without the familiarity, um, yeah, he, he needed convincing at first.”

Claim: Leo came to recognize dependent type theory's benefits and describe it as beautiful, despite initially needing persuasion.

“But ultimately, Leo emails Jeremy back during that summer of 2013 and tells him, "I've decided to go with dependent type theory," and Jeremy basically does a dance at home in Pittsburgh because he just knows the, the seeds are there now for Lean to be useful in math in the way he's always wanted an interactive theorem prover to potentially be useful.”

Claim: Jeremy believed dependent type theory gave Lean the potential to support mathematics as he had long wanted an interactive theorem prover to do.

“But ultimately, Leo emails Jeremy back during that summer of 2013 and tells him, "I've decided to go with dependent type theory," and Jeremy basically does a dance at home in Pittsburgh because he just knows the, the seeds are there now for Lean to be useful in math in the way he's always wanted an interactive theorem prover to potentially be useful.”

Claim: In summer 2013, Leo told Jeremy by email that he had decided to adopt dependent type theory for Lean.

“When you're using the developer hats, usually you want to go to whatever is simpler to implement, and you forget that you sometimes will be the user of this tool too.”

Claim: Developers often favor simpler implementation and overlook that they may also be users of the tool.

“I, I always joke, I mean, if I'm using my user hats, I want this feature. If I'm using the developer hats, I don't want it.”

Claim: The speaker says his preferences about a feature differ depending on whether he is acting as its user or developer.

“Oh, yeah. So Leo is, like, extremely self-critical. I mean, just there, there are many moments in the story of the development of Lean where he has some users and they love it, and he says it's shit. I mean, he just thinks it's terrible. He-- all he sees is its flaws. He wants to very doggedly fix those flaws.”

Claim: The speaker describes Leo as highly self-critical: despite users loving Lean, Leo sees its flaws, calls it terrible, and persistently tries to fix them.

“At Microsoft, Leo feared a poor annual rating would jeopardize his research. His manager never gave him one, but the fear persisted.”

Claim: Leo feared that a poor annual performance rating at Microsoft would jeopardize his research, although his manager never gave him one; the fear persisted.

“At Microsoft, Leo feared a poor annual rating would jeopardize his research. His manager never gave him one, but the fear persisted.”

Claim: Leo feared at Microsoft that a poor annual performance rating could jeopardize his research; the fear persisted although his manager never gave him one.

“Leo is just a researcher in computer science at Microsoft Research. He's not a project manager. He's not a product manager. He doesn't have, like, a team of engineers working with him.”

Claim: Leo works as a computer science researcher at Microsoft Research, not as a project or product manager, and has no team of engineers working with him.

“Through Jeremy, suddenly Lean very quickly gets a number of mathematicians who wanna start using it. They love it. They don't think it's shit. They think it's way better than Leo does, but they also have all these additional feature requests.”

Claim: After Jeremy's involvement, Lean quickly attracted mathematicians who liked it and considered it much better than Leo did, while asking for additional features.

“Wouldn't it be great if we could do this? It would be much easier if we could do that. Can we have, like, a richer UI? Uh, Leo wants to please the, the users. He's extremely, like, users-oriented in that way. It's very hard for him to receive a piece of feedback, especially if he recognizes it's kinda fundamentally correct, and ignore it. So he finds himself kind of responding rapidly to all these users who are not even the users he intended to be building for, who are doing something that's not even what he planned Lean to be useful for.”

Claim: Leo is strongly user-oriented and finds it difficult to disregard feedback when he recognizes it as fundamentally correct.

“It's very hard for him to receive a piece of feedback, especially if he recognizes it's kinda fundamentally correct, and ignore it. So he finds himself kind of responding rapidly to all these users who are not even the users he intended to be building for, who are doing something that's not even what he planned Lean to be useful for.”

Claim: Leo found himself rapidly responding to users who were not his intended audience and were using Lean for purposes he had not planned for it.

“But he starts fulfilling the requests. I think he's, like, barraged by emails, ultimately later by Slack messages. He can't really say no to them, but he becomes intensely frustrated because he feels like they're taking him for granted.”

Claim: Leo fulfilled users' requests but became intensely frustrated because he felt they were taking him for granted.

“He feels like they think that he has more time than he does, and most importantly, he has, like, a vision for where he wants Lean to go. There ultimately are four v- four versions of Lean.”

Claim: Leo felt users underestimated how limited his time was, while he had a vision for Lean's future direction.

“He feels like they think that he has more time than he does, and most importantly, he has, like, a vision for where he wants Lean to go. There ultimately are four v- four versions of Lean. We're currently on Lean 4, but for years, you know, we were at Lean 2. And J- uh, Leo saw where he wanted it to go, and he felt inhibited in his ability to actually find the time to do it because he was answering all these essentially, like, user support questions and, uh, queries from mathematicians.”

Claim: Lean has had four versions; it is currently at Lean 4, and it remained at Lean 2 for years.

“We're currently on Lean 4, but for years, you know, we were at Lean 2. And J- uh, Leo saw where he wanted it to go, and he felt inhibited in his ability to actually find the time to do it because he was answering all these essentially, like, user support questions and, uh, queries from mathematicians.”

Claim: Leo felt that responding to user-support questions and mathematicians' queries left him unable to find time to move Lean toward his intended vision.

“One of the earliest adopters of Lean and kind of most enthusiastic evangelists for Lean is a mathematician at Imperial College in London named Kevin Buzzard.”

Claim: Kevin Buzzard, a mathematician at Imperial College London, was among Lean's earliest adopters and most enthusiastic advocates.

“My name's Kevin Buzzard. I'm a number theorist working at Imperial College London. I spent some time at the beginning of this century bringing up three kids. When that was sort of over and they were able to look after themselves a lot more, uh, I wanted to get back into doing hard research mathematics, and I realized that there was a huge amount of material that I was gonna have to sort of catch up on.”

Claim: Once his three children were more able to look after themselves, Kevin Buzzard wanted to return to hard research mathematics.

“My name's Kevin Buzzard. I'm a number theorist working at Imperial College London. I spent some time at the beginning of this century bringing up three kids.”

Claim: Kevin Buzzard works as a number theorist at Imperial College London.

“When that was sort of over and they were able to look after themselves a lot more, uh, I wanted to get back into doing hard research mathematics, and I realized that there was a huge amount of material that I was gonna have to sort of catch up on.”

Claim: When returning to research mathematics, Kevin Buzzard realized he had a substantial body of material to catch up on.

“I had some kind of midlife crisis around that time because I was trying to read it, and I couldn't understand all of it, and I would find what I thought were mistakes in the literature.”

Claim: Kevin Buzzard experienced what he called a kind of midlife crisis while struggling to understand some mathematical literature and believing he had found errors in it.

“Then I started thinking, "Well, wait a minute," like, "what are we..." Like, what-- this is very abstract stuff. It's not immediately clear there's any sort of concrete applications, so there's nothing that we can sort of test these things on in reality.”

Claim: Kevin Buzzard saw the mathematical material as highly abstract, with no immediately clear concrete applications or straightforward way to test it against reality.

“And if they're not right, then almost, you know, what is the point of this stuff at all? So I had some kind of crisis, and I started thinking, you know, would it be possible to check mathematics using machines?”

Claim: Concerned that the mathematics might be incorrect, Kevin Buzzard questioned its point and began asking whether machines could check mathematical proofs.

“'Cause, you know, technology's moving very fast. And so I went down some kind of rabbit hole just kind of exploring the software that was out there that was claiming, you know, that it could check mathematics at superhuman accuracy, and it absolutely could check mathematics at superhuman accuracy.”

Claim: Kevin Buzzard explored mathematical-checking software that claimed—and, in his assessment, was able—to verify mathematics with superhuman accuracy.

“But the problem was the mathematic-- ninety-nine percent of what it was checking was really, really basic material known hundreds or maybe even thousands of years ago.”

Claim: According to Kevin Buzzard, 99% of the mathematics checked by the software was basic material already known for hundreds or possibly thousands of years.

“So the-- but, but by that stage, I kind of got hooked 'cause I realized that there was this weird new way of doing mathematics. I'd never really seen anything like it before, and I started to realize that actually doing mathematics in the software, even though it was very basic mathematics, was a huge amount of fun, you know, very different to doing it on paper and pencil.”

Claim: Kevin Buzzard found computer-based formal mathematics to be a novel approach and much more enjoyable than working with paper and pencil, which drew him in.

“"What can we actually get this software to do?" Uh, and at the time it was just like we could barely get it to do undergraduate-level mathematics. But because it was great fun using it, you know, that was how I ended up switching.”

Claim: When Kevin Buzzard switched to working with mathematical software, it could barely handle undergraduate-level mathematics, but he found using it enjoyable enough to make the switch.

“By two thousand and sixteen, Kevin Buzzard had time to return to the p-adic Langlands program. A young talent named Peter Scholze had transformed the geometry of numbers with perfectoid spaces, and Buzzard wanted to be part of the revolution.”

Claim: By 2016, Kevin Buzzard had time to return to the p-adic Langlands program and wanted to participate in the developments around Peter Scholze's perfectoid spaces.

“But as he read the papers that followed Scholze's work, his enthusiasm gave way to concern. Buzzard liked to see every detail spelled out, disliked vagueness and assurances from authority, what he called the opinion of the elders, and that perspective could bless promising ideas before they were fully defined.”

Claim: Kevin Buzzard valued fully explicit details and disliked vagueness and appeals to authority, which he thought could legitimize promising ideas before they were fully defined.

“But in the papers he reviewed, Buzzard thought that it had become a permission slip for sloppiness. His critique was not of Scholze's work, which he actually found brilliant and rigorous, but of the results built on top of it.”

Claim: Kevin Buzzard believed that appeals to authority had enabled sloppiness in results built on Peter Scholze's work, while he regarded Scholze's own work as brilliant and rigorous.

“He noticed mistakes in some papers and logical gaps in others, and experts just brushed him off, assuring him that the thrust was correct, even if the particular arguments were loose.”

Claim: Kevin Buzzard identified errors and logical gaps in some papers, but experts brushed off his concerns, saying the main ideas were correct despite imprecise arguments.

“Buzzard understood that young fields can be inexact while mathematicians work out how all of the pieces fit together. He saw one sloppy, incomplete paper building atop another and worried that his area of mathematics was turning into a house of cards.”

Claim: Kevin Buzzard accepted that young fields may be inexact as their ideas develop, but worried that one sloppy, incomplete paper building on another could make his mathematical field unstable.

“So to him, that was the draw of Lean, was he wanted to take these papers that had developed in his field, formalize them, like convert them into this computer programming language, determine with complete certainty whether, whether they were correct, and if they weren't, fix them, but if they were, then it would just kind of give him, uh, renewed confidence to kind of proceed in research in this area.”

Claim: Kevin Buzzard wanted to use Lean to formalize papers in his field, establish with complete certainty whether they were correct, repair incorrect papers, and regain confidence to continue research when the formalized results checked out.

“So here's a small example. The ring tactic constructs a proof of this algebraic identity using machinery from Mathlib. Lean then checks the proof, and it says no goals, which means the task is complete.”

Claim: In the example, Lean's ring tactic uses Mathlib machinery to construct a proof of an algebraic identity, and Lean's “no goals” output indicates that the proof task is complete.

“When Lean-- when you boot up Lean, Lean does not know any mathematics. It's equipped with basic axioms and rules for math, so it has some kind of just, like, some under-some understanding of mathematical logic.”

Claim: A newly booted Lean system has basic mathematical axioms and rules but does not initially know mathematics.

“So what you need to do is equip it with a library of definitions. And this is at the parallel story in my book. There are kind of two key stories, two dreams almost, that are very dependent on each other, sometimes in tension with each other.”

Claim: Lean needs a library of definitions in order to express mathematics.

“So what you need to do is equip it with a library of definitions. And this is at the parallel story in my book. There are kind of two key stories, two dreams almost, that are very dependent on each other, sometimes in tension with each other. So one is Leo's vision for Lean, the software he wants to build. The other is the development of what comes to be called Mathlib, a library of digital mathematics, which is spearheaded by several of the main characters in the book.”

Claim: The book presents Leo's vision for Lean and the development of Mathlib as two interdependent stories that are sometimes in tension.

“So one is Leo's vision for Lean, the software he wants to build. The other is the development of what comes to be called Mathlib, a library of digital mathematics, which is spearheaded by several of the main characters in the book.”

Claim: Mathlib is a digital mathematics library developed by several people who are among the book's main characters.

“People like Kevin Buzzard, Johan Commelin, Patrick Masso, Jeremy Avigad's very involved. M-Mario Carneiro is another figure who's very important in the development of Mathlib.”

Claim: Kevin Buzzard, Johan Commelin, Patrick Masso, Jeremy Avigad, and Mario Carneiro are involved in Mathlib's development, and Mario Carneiro is an important figure in that development.

“The vision for that is it will be a crowdsourced effort to define, in Lean language, basic concepts in math from the ground up.”

Claim: Mathlib is intended as a crowdsourced project to define basic mathematical concepts from the ground up in Lean.

“So starting with even just, like, high school-level math to college-level math, so that you have the ingredients to then later encode more sophisticated forms of math.”

Claim: Mathlib begins with high-school- and college-level mathematics to provide ingredients for encoding more sophisticated mathematics later.

“That's kind of the re-- that's how Lean breaks beyond just these combinatorial results like the four-color theorem and Kepler's conjecture and becomes a place where you can express very deep, kind of frontier-level abstract math.”

Claim: Developing Mathlib enables Lean to express deep, frontier-level abstract mathematics beyond combinatorial results such as the four-color theorem and Kepler's conjecture.

“It's through the development of Mathlib. And actually, I got in-interested in this story back in twenty twenty when I was assigned an article for Quanta Magazine on the development of Mathlib when it was still quite early days.”

Claim: The speaker became interested in Mathlib's development in 2020 while assigned to write a Quanta Magazine article about the project in its early days.

“In that article, I say, I said that Mathlib had the spirit of a barn raising. It was just, like, this, like, community effort to get this massive thing done without any central authority, no central resources.”

Claim: The speaker characterized Mathlib's development as a community barn-raising effort that built a large project without central authority or central resources.

“And so slowly, this library of digital mathematics is created.”

Claim: Mathlib was built gradually as a library of digital mathematics.

“Mathlib is Lean's mathematics library. So it was born about the same time that I started working in the field. It was thirty thousand lines of code containing a bunch of completely basic theorems about finite sets, uh, and some very basic undergraduate-level mathematical definitions, and that was it.”

Claim: When the speaker began working in the field, Mathlib contained about 30,000 lines of code covering basic finite-set theorems and some basic undergraduate-level mathematical definitions.

“It didn't even have a definition of the real numbers when I started, or it, it, it just got this concept of the real numbers, which is something known to, you know, known to the ancient Greeks and the Babylonians.”

Claim: When the speaker started working with Mathlib, the library lacked a definition of the real numbers and had only just gained the concept.

“You know, it's, uh, you know, thousands of years old. Uh, and it didn't have the complex numbers, which are, I guess, from about five hundred years ago.”

Claim: When the speaker started working with Mathlib, it lacked the complex numbers; the speaker estimates that complex numbers date from about 500 years ago.

“And, uh, one of the things we teach them is how to define the complex numbers, which are this basic number system that goes back to Descartes. So I kind of thought, "Oh, this thing doesn't have the complex numbers. Let's teach it the complex numbers." So there we go. We define the complex numbers, prove basic things about it, and it was great. And I made a pull request.”

Claim: The speaker defined the complex numbers in Mathlib, proved basic results about them, and submitted the contribution as a pull request.

“You know, this is a free open source maths library. So I made a pull request to this maths library, and then it got merged into the main branch. And suddenly we've got complex numbers, copyright twenty seventeen Kevin Buzzard.”

Claim: The speaker's pull request was merged into Mathlib's main branch, adding a definition of the complex numbers to the library.

“Why don't we just contribute to this library? But of course, there's so much stuff that one person can't do it, so I roped the undergraduates in. It was absolutely critic-- We'd just got to the point where all my kids could make their way to school by themselves.”

Claim: The speaker recruited undergraduates to contribute to Mathlib because one person could not complete all the needed work alone.

“So, so I could stay late at work. Like, one evening a week, I'd stay late at work and just let the kids muddle on by themselves, and, uh, and I would teach undergraduates how to use this software.”

Claim: The speaker stayed late at work one evening each week to teach undergraduates how to use Lean.

“And then I would get them to start, you know, transcribing what they were learning in their, in their undergraduate degree, just, just teaching it to this machine.”

Claim: The speaker asked undergraduates to encode the mathematics they were learning in their degree in Lean.

“So the library just like-- I mean, there was lots of other people around the world do-- Well, not lots, but there were plenty of other people around the world doing the same thing. You know, I, I was treating this thing as an undergraduate at the time.”

Claim: At the time, other people around the world were also contributing to the library, although the speaker qualifies that there were not many.

“So it's twenty seventeen, and the question was, you know, let's just imagine you've enrolled on our degree. You know, can we, can we actually teach you at the same rate as we teach the undergraduates?”

Claim: In 2017, the speaker explored whether Lean could learn mathematics at the same rate as undergraduate students.

“And it was, it was just about possible, you know, the, the, the thing was learning at the same rate as our students at the time. But, you know, three years later, we could sort of step back and say, "Well, actually, you do basically know most of the things we teach our undergraduates now."”

Claim: By about 2020, the speaker judged that Lean knew most of the material taught to undergraduates.

“And it was, it was just about possible, you know, the, the, the thing was learning at the same rate as our students at the time. But, you know, three years later, we could sort of step back and say, "Well, actually, you do basically know most of the things we teach our undergraduates now."”

Claim: In 2017, Lean was learning mathematics at approximately the same rate as the speaker's undergraduate students.

“Mathematics is, is an interesting object. It's this gigantic abstract object that humans have created. And at the boundary, there are things that haven't, you know, they're not quite fully formed.”

Claim: Mathematics is a vast abstract object created by humans, and some ideas at its frontier are not yet fully formed.

“There are ideas which sort of, sort of work or work in some cases, and, you know, we, we need to think about how these ideas should mature, what they should really look like.”

Claim: Some frontier mathematical ideas work only in certain cases and need further development to mature into a clearer form.

“So m-mathematics needs to mature. Sometimes at the boundary, it's, it's not material that's ideal for the library. You know, what we want in the library is ideas which are really well understood and there's a-- exist in the correct generality.”

Claim: Some mathematics at the frontier needs to mature before it is suitable for inclusion in the library.

“So m-mathematics needs to mature. Sometimes at the boundary, it's, it's not material that's ideal for the library. You know, what we want in the library is ideas which are really well understood and there's a-- exist in the correct generality.”

Claim: The mathematical library should contain ideas that are well understood and stated at the appropriate level of generality.

“You know, we want polished, we want polished mathematics. Stuff which is still a bit chaotic, you know, one can attempt to teach it to the mach-- you know, we can teach it to the software, but we don't necessarily want to add it to the library.”

Claim: The mathematical library should contain polished mathematics rather than still-chaotic material, even when that material can be taught to software.

“The library wants to take sort of fully formed, well thought out, you know, beautiful conceptual ideas, uh, which sort of know their place.”

Claim: The mathematical library should include fully formed, well-considered conceptual ideas that are coherent and appropriately situated.

“Essentially all of the library now is, uh- is, is well thought out, beautiful ideas. Some of the things in the library are actually stuff that happened in the last few years, but a lot of it is much more basic stuff, uh, that we feel like we understand well because that's, you know, that's when you want to commit, right?”

Claim: The mathematical library currently consists almost entirely of well-considered, elegant ideas.

“Essentially all of the library now is, uh- is, is well thought out, beautiful ideas. Some of the things in the library are actually stuff that happened in the last few years, but a lot of it is much more basic stuff, uh, that we feel like we understand well because that's, you know, that's when you want to commit, right?”

Claim: Some material in the mathematical library was developed in the last few years, while much of it is more basic mathematics considered sufficiently well understood for inclusion.

“Th- this is part of the work of our community, trying to understand what humans have done and to get it into the correct, you know, most abstract, most useful form for future work.”

Claim: A task of the mathematical community is to understand existing human mathematical work and express it in the most abstract, useful form for future research.

“Because you don't really want to put some concept in the library, and then it gets generalized and simplified a bit, and then somehow you need to rework the entire thing. This- we, we try and avoid this.”

Claim: The mathematical community tries to avoid adding concepts to the library prematurely, since later generalization or simplification could require reworking the entire concept.

“We, we like to get things right first time. Uh, occasionally we have had to go through and change a fundamental definition. This can be a huge amount of work because then, you know, many thousands of files, uh, then break and need to be fixed.”

Claim: The mathematical community aims to get definitions right initially because changing a fundamental definition can break thousands of files that must then be repaired.

“Kevin Buzzard has, like, the instincts of a showman. He's like a natural marketer, and he comes up with a couple, um, essentially schemes or stunts for doing this.”

Claim: Kevin Buzzard is a natural marketer with showman-like instincts.

“Kevin Buzzard has, like, the instincts of a showman. He's like a natural marketer, and he comes up with a couple, um, essentially schemes or stunts for doing this.”

Claim: Kevin Buzzard has showman-like instincts and is a natural marketer.

“And one of them actually is to formalize a mathematical object called schemes, which is an algebraic geometry. It, uh, comes from Alexander Grothendieck in the mid-20th century.”

Claim: Kevin Buzzard pursued formalization of schemes, an algebraic-geometry object introduced by Alexander Grothendieck in the mid-20th century.

“And one of them actually is to formalize a mathematical object called schemes, which is an algebraic geometry. It, uh, comes from Alexander Grothendieck in the mid-20th century.”

Claim: Schemes are mathematical objects in algebraic geometry that originated with Alexander Grothendieck in the mid-20th century.

“And one of them actually is to formalize a mathematical object called schemes, which is an algebraic geometry. It, uh, comes from Alexander Grothendieck in the mid-20th century.”

Claim: Kevin Buzzard pursued formalizing schemes, an object from algebraic geometry, in Lean as a strategy for demonstrating the value of formalization.

“He says to himself, "If we can formalize schemes in Lean and I can tell the world about it, then mathematicians will suddenly start to believe that this is useful for the types of-- type of, like, frontier math that they themselves care about."”

Claim: Kevin Buzzard expected that formalizing schemes in Lean and publicizing the result would persuade mathematicians that Lean could support frontier mathematics relevant to them.

“He says to himself, "If we can formalize schemes in Lean and I can tell the world about it, then mathematicians will suddenly start to believe that this is useful for the types of-- type of, like, frontier math that they themselves care about."”

Claim: Kevin Buzzard expected that formalizing schemes in Lean and publicizing the result would persuade mathematicians that Lean could support the frontier mathematics they cared about.

“He does it and he's met with, like, a collective yawn because people tell him, "Kevin, schemes are old math," right? "Sixty, eighty years old. I knew this when I was in graduate school. This is not frontier math." And Kevin's like, "Okay, that's true. What is frontier math?" And in this period, uh, around 2018, frontier math is this object called perfectoid spaces, which is something that was created by a German mathematician named Peter Schulze, who is today and then as well considered maybe the greatest living mathematician.”

Claim: Mathematicians showed little interest in the formalization of schemes, regarding schemes as 60–80-year-old mathematics they had encountered in graduate school rather than frontier mathematics.

“He does it and he's met with, like, a collective yawn because people tell him, "Kevin, schemes are old math," right? "Sixty, eighty years old. I knew this when I was in graduate school. This is not frontier math." And Kevin's like, "Okay, that's true. What is frontier math?" And in this period, uh, around 2018, frontier math is this object called perfectoid spaces, which is something that was created by a German mathematician named Peter Schulze, who is today and then as well considered maybe the greatest living mathematician.”

Claim: Mathematicians told Kevin Buzzard that schemes were old mathematics—about 60 to 80 years old—and were not frontier mathematics.

“This is not frontier math." And Kevin's like, "Okay, that's true. What is frontier math?" And in this period, uh, around 2018, frontier math is this object called perfectoid spaces, which is something that was created by a German mathematician named Peter Schulze, who is today and then as well considered maybe the greatest living mathematician.”

Claim: Peter Scholze, a German mathematician, created perfectoid spaces and was considered perhaps the greatest living mathematician at the time.

“This is not frontier math." And Kevin's like, "Okay, that's true. What is frontier math?" And in this period, uh, around 2018, frontier math is this object called perfectoid spaces, which is something that was created by a German mathematician named Peter Schulze, who is today and then as well considered maybe the greatest living mathematician.”

Claim: Perfectoid spaces were created by German mathematician Peter Scholze, who was regarded at the time as perhaps the greatest living mathematician.

“This is not frontier math." And Kevin's like, "Okay, that's true. What is frontier math?" And in this period, uh, around 2018, frontier math is this object called perfectoid spaces, which is something that was created by a German mathematician named Peter Schulze, who is today and then as well considered maybe the greatest living mathematician.”

Claim: Around 2018, perfectoid spaces were regarded as frontier mathematics.

“This is not frontier math." And Kevin's like, "Okay, that's true. What is frontier math?" And in this period, uh, around 2018, frontier math is this object called perfectoid spaces, which is something that was created by a German mathematician named Peter Schulze, who is today and then as well considered maybe the greatest living mathematician.”

Claim: Around 2018, perfectoid spaces were considered frontier mathematics.

“Perfectoid spaces are truly state-of-the-art objects in, in math. And Kevin says, "All right, if we can formalize them, if we can show Lean is capable, capable of expressing perfectoid spaces, we'll have indisputable proof that it can do anything."”

Claim: Kevin Buzzard believed that formalizing perfectoid spaces would prove indisputably that Lean could express anything.

“Perfectoid spaces are truly state-of-the-art objects in, in math. And Kevin says, "All right, if we can formalize them, if we can show Lean is capable, capable of expressing perfectoid spaces, we'll have indisputable proof that it can do anything."”

Claim: Perfectoid spaces are state-of-the-art mathematical objects.

“Perfectoid spaces are truly state-of-the-art objects in, in math. And Kevin says, "All right, if we can formalize them, if we can show Lean is capable, capable of expressing perfectoid spaces, we'll have indisputable proof that it can do anything."”

Claim: Kevin Buzzard believed that formalizing perfectoid spaces in Lean would prove that Lean could express any mathematics.

“Perfectoid spaces are truly state-of-the-art objects in, in math. And Kevin says, "All right, if we can formalize them, if we can show Lean is capable, capable of expressing perfectoid spaces, we'll have indisputable proof that it can do anything."”

Claim: Perfectoid spaces are state-of-the-art objects in mathematics.

“And so he and Massó and Kamlin start this effort, just the three of them, to create a blueprint, essentially a kind of, um, a guide to the things they would need to define in Lean in order to be able to-- in or- in order to be able to write the definition of a perfectoid space.”

Claim: Kevin Buzzard, Massó, and Kamlin began drafting a blueprint listing the definitions needed to define a perfectoid space in Lean.

“And so he and Massó and Kamlin start this effort, just the three of them, to create a blueprint, essentially a kind of, um, a guide to the things they would need to define in Lean in order to be able to-- in or- in order to be able to write the definition of a perfectoid space.”

Claim: Kevin Buzzard, Massó, and Kamlin began a three-person project to blueprint the Lean definitions needed to define a perfectoid space.

“So it's essentially a punch list, like a construction project. You know, we would need you to define this and then this and this and this, and ultimately we'd get perfectoid spaces. They succeed at that.”

Claim: The group successfully created a checklist of definitions needed in Lean to define perfectoid spaces.

“And what that, uh-- I think kind of a, an important point to emphasize is Mathlib is all of the math that anyone working in Lean can draw on.”

Claim: Mathlib contains the mathematics available for anyone working in Lean to use.

“And what that, uh-- I think kind of a, an important point to emphasize is Mathlib is all of the math that anyone working in Lean can draw on.”

Claim: Mathlib is the body of mathematics available for use by people working in Lean.

“At the moment, it's essentially maybe first-year graduate-level math. They have all of undergraduate math, modulo a few things here and there. They have about all of first-year graduate-level math.”

Claim: At the time of the conversation, Mathlib contained nearly all undergraduate mathematics and about all first-year graduate-level mathematics.

“At the moment, it's essentially maybe first-year graduate-level math. They have all of undergraduate math, modulo a few things here and there. They have about all of first-year graduate-level math.”

Claim: At the time described, Mathlib covered nearly all undergraduate mathematics, with a few gaps, and approximately all first-year graduate-level mathematics.

“Then there are these extreme spikes from grad math to the far frontier of the field, which is like extremely far from graduate school math. Perfectoid spaces is one of the first examples of we have this foundation, now we're gonna build this like narrow skyscraper to the frontier.”

Claim: Perfectoid spaces were among the first examples of using a broad mathematical foundation to build a narrow path to the field's distant frontier.

“Then there are these extreme spikes from grad math to the far frontier of the field, which is like extremely far from graduate school math. Perfectoid spaces is one of the first examples of we have this foundation, now we're gonna build this like narrow skyscraper to the frontier.”

Claim: Formalizing perfectoid spaces exemplifies building a narrow extension from foundational graduate-level mathematics to the far frontier of mathematics.

“Perfectoid spaces is that-- is the first example of that. That stunt works the way Buzzard hopes it will work. It got-- it, it, it captures a lot of people's attention.”

Claim: The perfectoid-spaces formalization effort worked as Kevin Buzzard hoped and attracted substantial attention.

“Perfectoid spaces is that-- is the first example of that. That stunt works the way Buzzard hopes it will work. It got-- it, it, it captures a lot of people's attention.”

Claim: The perfectoid-spaces project worked as Kevin Buzzard hoped and attracted substantial attention.

“Perfectoid spaces is that-- is the first example of that. That stunt works the way Buzzard hopes it will work. It got-- it, it, it captures a lot of people's attention.”

Claim: The perfectoid-spaces project was the first example of building a narrow extension from foundational mathematics to the frontier of the field.

“Perfectoid spaces is that-- is the first example of that. That stunt works the way Buzzard hopes it will work. It got-- it, it, it captures a lot of people's attention.”

Claim: Formalization of perfectoid spaces was the first example described of extending a mathematical foundation through a narrow construction to the frontier.

“It boosts Lean's profile. Uh, and it kind of starts to convince people. It starts the process described in the book of convincing people Lean can be used for real math.”

Claim: The perfectoid-spaces project began persuading people that Lean could be used for real mathematics.

“It boosts Lean's profile. Uh, and it kind of starts to convince people. It starts the process described in the book of convincing people Lean can be used for real math.”

Claim: The perfectoid-spaces project raised Lean’s profile.

“It boosts Lean's profile. Uh, and it kind of starts to convince people. It starts the process described in the book of convincing people Lean can be used for real math.”

Claim: The perfectoid-spaces effort raised Lean's profile.

“It boosts Lean's profile. Uh, and it kind of starts to convince people. It starts the process described in the book of convincing people Lean can be used for real math.”

Claim: The perfectoid-spaces effort began persuading people that Lean could be used for substantive mathematics.

“So I was just beginning. This was back, back-- So back in 2017, I was having this midlife crisis and, uh, trying to work out what was going on in the area of, you know, computers proving theorems. And I discovered, to my amusement, that there was a big conference in the area that I was far too late to register for, uh, in Cambridge taking place in two years' time.”

Claim: In 2017, Kevin Hartnett was exploring computer theorem proving and discovered that a Cambridge conference on the subject was scheduled for 2019.

“But, um, Ca- this was at the Newton Institute in Cambridge and they were ahead of the game. This is pre-COVID. Uh, but they were already, uh, recording and live streaming, uh, their talks on the internet.”

Claim: Before COVID, the Newton Institute in Cambridge recorded and live-streamed its talks online.

“So, uh, even though I couldn't go to the conference, I could still watch the talks. And the first talk was given by Tom. And I imagined, uh, that he would be, uh, by, by Tom Hales.”

Claim: Although Kevin Hartnett could not attend the Cambridge conference, he could watch its talks online; the first talk was given by Tom Hales.

“And I imagined that he would be talking about his proof of the Kepler conjecture. But in fact, that only formed a very small, uh, part of his talk. Uh, he was talking about, you know, exactly the thing that I'd become worried about.”

Claim: Kevin Hartnett expected Tom Hales to discuss his proof of the Kepler conjecture, but the proof formed only a small part of Hales's talk.

“He, he was talking about formalizing modern mathematics, you know, perhaps all of modern mathematics. Uh, and one of the things he suggested was that perhaps it was time, uh, that we got mathematicians not to learn enough about these computer theorem proving languages to actually type in all their proofs, but just to literally type in the statements of their theorems, because that's a much easier job just saying, "Okay, I claim that I've proved this and here's what it looks like in English, but here's what the statement of the theorem looks like in a formal language." And then the proof is one hundred pages long. Uh, and, and translating the proof into this language would be a, you know, would, would be like a PhD thesis worth of work, you know, a gigantic problem.”

Claim: Tom Hales discussed formalizing modern mathematics, possibly all of modern mathematics, and proposed that mathematicians enter theorem statements in a formal language without necessarily translating their proofs.

“looks like in a formal language." And then the proof is one hundred pages long. Uh, and, and translating the proof into this language would be a, you know, would, would be like a PhD thesis worth of work, you know, a gigantic problem.”

Claim: Translating a 100-page mathematical proof into a formal language could require work comparable to a PhD thesis.

“Uh, but perhaps we should start persuading mathematicians, uh, to state what they're doing in this formal language because then there's no ambiguity. You see, in, in reality, you, you would imagine that maths was this sort of perfect language where everything can be expressed, you know, in a, in a completely unambiguous way.”

Claim: Tom Hales suggested encouraging mathematicians to state their work in a formal language to eliminate ambiguity.

“Uh, but perhaps we should start persuading mathematicians, uh, to state what they're doing in this formal language because then there's no ambiguity. You see, in, in reality, you, you would imagine that maths was this sort of perfect language where everything can be expressed, you know, in a, in a completely unambiguous way. But in practice, this is not, uh, this is not what happens. In practice, you, you read, you read section three of the paper. In section three it says, "From this point, P will be a prime number which is at least five."”

Claim: Although mathematics may seem capable of expressing everything unambiguously, mathematical papers do not always communicate that way in practice.

“But in practice, this is not, uh, this is not what happens. In practice, you, you read, you read section three of the paper. In section three it says, "From this point, P will be a prime number which is at least five." And then you read something in section seven of the paper and it's just talking about a number called P and you know from reading lots of number theory papers that P will be a prime number.”

Claim: A mathematical paper can state in one section that P is a prime number at least five and later refer to P without repeating that condition.

“But this, this, this fact that P is at least five that was sort of slipped in to section three, if you start reading in section seven you don't notice this hypothesis.”

Claim: A reader who begins with a later section of a mathematical paper may miss a condition introduced earlier, such as the requirement that P be at least five.

“Uh, and so it looks like the theorem says something. You know, the theorem isn't The theorem, if you read the whole paper, then the theorem is correctly stated.”

Claim: Missing an earlier hypothesis can make a theorem appear to assert something different, even if the theorem is correctly stated when the entire paper is read.

“But if you're just trying to work out, you know, what's going on in section seven, uh, then you might make an error. And Hales was like, "We need to fix these errors. We've got tools that can do this now."”

Claim: Readers who interpret a section without the full paper's context may make errors; Tom Hales argued that existing tools could help prevent them.

“Uh, and I just thought, "This is a great idea." You're trying to, trying to translate all the-- I'd, I'd re- I was two weeks in, and I'd realized that the systems knew nothing.”

Claim: After two weeks of work, Kevin Hartnett concluded that the systems he was considering knew nothing.

“But somehow the idea of teaching the systems basic mathematical definitions seemed to be much more viable than teaching it, you know, one hundred-page long proofs of theorems.”

Claim: Kevin Hartnett considered teaching systems basic mathematical definitions more viable than teaching them proofs that are 100 pages long.

“Because many mathematical definitions are quite short. In fact, that was what the library looked like in twenty seventeen. It contained some, some definitions that mathema- that, you know, undergraduates find quite difficult.”

Claim: Many mathematical definitions are short; the 2017 library included definitions of topics that undergraduates can find difficult.

“You know, second year and third year fancy things like topological spaces and noetherian rings and things like this. Um, but actually just writing the definition down is only a few lines of code in the computer.”

Claim: A computer representation of a definition for an advanced mathematical concept, such as a topological space or a Noetherian ring, can take only a few lines of code.

“It's proving all the theorems about it where all the work is. So if you can just write down the definitions, then we can start stating the theorems and, uh, this just seemed to me like a viable way to move forwards whilst engaging, you know, with interesting material.”

Claim: In formalizing mathematics, proving theorems about a concept requires most of the work, while writing down its definition can be brief.

“It's proving all the theorems about it where all the work is. So if you can just write down the definitions, then we can start stating the theorems and, uh, this just seemed to me like a viable way to move forwards whilst engaging, you know, with interesting material.”

Claim: Kevin Hartnett considered entering mathematical definitions and then formal theorem statements a viable way to advance formalization while engaging with interesting material.

“So it, it was just a completely y- my idea was just like, let's check these modern papers remark, that's completely impossible. Whereas Hales' idea was viable.”

Claim: Kevin Hartnett initially considered checking the remarks in modern mathematical papers completely impossible, while Tom Hales's proposal to formalize theorem statements seemed viable.

“Uh, in fact, it was somehow not quite viable at that moment. You know, Ha- Hales pushed for, Hales pushed for it to be happening in twenty seventeen. Uh, and it was somehow too difficult to do in twenty seventeen.”

Claim: Tom Hales advocated carrying out the theorem-statement formalization project in 2017, but it was too difficult then.

“But actually, seven years later, um, I wrote a grant proposal to do exactly what Hales had said, you know, just to do the same thing.”

Claim: Seven years after Hales's 2017 proposal, Kevin Hartnett wrote a grant proposal to formalize theorem statements in a formal language.

“And, uh, and we've spent a year working on this now, and it now is sort of, it's becoming viable. We're taking, uh, theorems published in, you know, the top pure maths journal, uh, this decade, and we're trying to translate just the statements of the theorems, uh, into the language of the software.”

Claim: After a year of work, Kevin Hartnett's team was translating statements of theorems published in leading pure-mathematics journals during the current decade into a formal software language, and the project was becoming viable.

“And, uh, yeah, we're twenty percent through. So that's some indication, uh, that at least, you know, this dream is sort of slowly becoming a reality.”

Claim: Kevin Hartnett's team had completed 20% of its theorem-statement formalization project, which he viewed as evidence that the goal was gradually becoming real.

“And I would imagine that in a year's time, we're gonna be far more than twenty percent through. So some- so, so Hales had these ideas which have taken years, uh, to become real.”

Claim: Kevin Hartnett expected his team to have completed more than 20% of the project one year later.

“And I would imagine that in a year's time, we're gonna be far more than twenty percent through. So some- so, so Hales had these ideas which have taken years, uh, to become real.”

Claim: Tom Hales's ideas about formalizing theorem statements took years to become reality.

“But now, you know, now they are beco- so t- you know, I, I would say that Hales was really a, you know, this, this was a visionary talk. Uh, and now, uh, his vision is coming to fruition.”

Claim: Kevin Hartnett regarded Tom Hales's talk as visionary and believed Hales's vision was beginning to come to fruition.

“Formalizing a proof or writing math in this formal language, right, is very kind of tedious. You have to spell out every little detail. Um, even things that are kind of trivial or obvious to mathematicians, you need to kind of convince the computer, uh, the, of their correctness.”

Claim: Formalizing proofs in Lean is tedious because users must spell out every detail, including seemingly trivial steps, to establish correctness to the computer.

“They want, they wanna formalize it in Lean. And what they discover is often it's the most trivial statements that are most obviously true to humans are the hardest to convince Lean are correct.”

Claim: In the speaker’s account, statements that seem most trivial and obvious to humans are often the hardest to verify in Lean when formalizing informal proofs.

“Things like one plus one is two. Like, Kevin Buzzard confronts the difficulty of formalizing simple statements in just the first few weeks he's using Lean, where he wants to just convince the program that one plus one is two.”

Claim: Kevin Buzzard encountered difficulty formalizing simple statements in Lean during his first few weeks using it, including proving that one plus one equals two.

“It's hard. Terry Tao, much later, when he is formalizing some of his own work in Lean, he confronts a similarly elementary fact that is just, you know, obvious on its surface to mathematicians, but convincing Lean it's correct is difficult.”

Claim: Terry Tao found it difficult to convince Lean of an elementary fact while formalizing some of his own work.

“So the point is, there's a, there are lots of, lots of steps when writing math in this formal language that become kind of tedious and difficult. One of Leo de Mora's ideas for Lean is it would have these little helper programs called tactics, which will automate some of those repeated steps, those kind of things, steps that happen regularly in proofs.”

Claim: Writing mathematics in a formal language involves many tedious and difficult steps.

“So the point is, there's a, there are lots of, lots of steps when writing math in this formal language that become kind of tedious and difficult. One of Leo de Mora's ideas for Lean is it would have these little helper programs called tactics, which will automate some of those repeated steps, those kind of things, steps that happen regularly in proofs.”

Claim: Leo de Mora proposed Lean tactics—helper programs that automate repeated steps commonly needed in proofs.

“Instead of having to explain to Lean why one plus one is two, you can invoke a certain tactic that just does those type of arithmetic guarantees that kind of proves equalities, numerical equalities, and then you don't have to do it yourself.”

Claim: Lean tactics can automate arithmetic steps, including proving numerical equalities, so users need not establish those steps manually.

“So Leo builds out the capability. He writes some specific tactics that are useful for Lean, but he also builds out the capability for people in the community, Lean users, to write their own tactics.”

Claim: Leo developed useful Lean tactics and built the capability for Lean users to create their own tactics.

“That becomes one way in which Lean becomes much more powerful, and this pain of writing proofs in Lean starts to diminish.”

Claim: The development of tactics made Lean more powerful and began to reduce the difficulty of writing proofs in it.

“Scholze was the mathematician others turned to when they needed their proofs checked. So in, in November twenty twenty, I was contacted by, uh, the Fields medalist, Peter Scholze.”

Claim: Peter Scholze contacted the speaker in November 2020, and Scholze was a mathematician whom others asked to check their proofs.

“This was back when the library had just basically graduated in some sense. You know, we had sort of-- it, it, it knew a lot of undergraduate level mathematics, but not too much else.”

Claim: At the time Peter Scholze contacted the speaker, the library knew a substantial amount of undergraduate mathematics but little beyond that.

“You know, we'd had a study group on it at my university. In fact, a London-wide study group. There were people from other universities in London. We would meet every week, and we would read another section from this, you know, spend two hours reading another section from this paper.”

Claim: Before Scholze contacted the speaker, a London-wide study group met weekly and spent about two hours reading a section of Scholze's paper at each meeting.

“And during the term, uh, we'd read the entire, we'd read the entire paper. That was the term before Peter got in touch with me. And, uh, so I said yes.”

Claim: The study group completed reading Scholze's entire paper during the term before Scholze contacted the speaker.

“So th-this was a second email from him, you know, asking specifically about checking the details of one, of one of the arguments in this paper. So I went back and looked at the paper, which is a big paper, and, uh, and, uh, we had not read the details of this. We'd read the statement of the theorem. We'd understood what it was trying to say until, you know, the point of it, where it fitted into the grander scheme of things.”

Claim: The speaker's study group understood the statement and role of Scholze's theorem but had not carefully read the proof's details.

“And the proof was just sort of six pages of technical calculations that we had skimmed through at best, you know. Oh, it's, you get the hang of the general idea of what's going on.”

Claim: The proof was six pages of technical calculations, and the study group had skimmed those details at best.

“So we had not read the details at all. So I emailed him back, said, you know, "We looked at it. Uh, we didn't read the details." And he said, "That's what everybody says." And he'd asked people at, you know, at Princeton and at Harvard, uh, "That's what everybody says." Like, that-- And, uh, he'd become convinced that nobody had actually read his work.”

Claim: After people at Princeton and Harvard said they had not read the details, Peter Scholze became convinced that nobody had actually read his work.

“You know, people had skimmed over his work. But, and of course, the devil is in the details in mathematics. So he said, "At the end of the day, uh, this material is-- it sort of looks technical, but at the end of the day, a lot of it is undergraduate level material.”

Claim: Peter Scholze said that much of the technical-looking material in his paper was undergraduate-level mathematics.

“So, um, maybe it would be possible, uh, for your system to check this material." And I thought that would be a great test because this is interesting.”

Claim: The speaker considered checking Scholze's material a great test for the system.

“So, um, maybe it would be possible, uh, for your system to check this material." And I thought that would be a great test because this is interesting.”

Claim: Peter Scholze suggested that the speaker's system might be able to check the material in his paper.

“All we have, you know, is, is undergraduate level stuff. And all of a sudden, I've got this Fields medalist suggesting that we could check part of his most recent paper.”

Claim: At the time Scholze proposed the challenge, the system's library contained only undergraduate-level mathematics.

“And, and I was just, you know, part of-- At, at the time, nobody was taking this software seriously. Maybe people were just beginning to take it seriously.”

Claim: At the time, people generally were not taking the software seriously, although the speaker thought they might just be beginning to take it seriously.

“The year before, we'd, we'd taken one of his definitions. As I said, definitions are much easier than proofs of one hundred page theorems. The year before, we'd taken one of his definitions and taught it to the machine, and we got a certain amount of traction.”

Claim: The year before the proof-checking challenge, the team taught the machine one of Peter Scholze's definitions and achieved some progress.

“The year before, we'd, we'd taken one of his definitions. As I said, definitions are much easier than proofs of one hundred page theorems. The year before, we'd taken one of his definitions and taught it to the machine, and we got a certain amount of traction.”

Claim: The speaker said that formalizing definitions is much easier than formalizing proofs of theorems that are one hundred pages long.

“You know, in, in people are beginning to notice, uh, that the software was able to do more complex material. But this is, um, you know, this was a complex proof of a complex theorem.”

Claim: People were beginning to notice that the software could handle increasingly complex mathematical material.

“It was only, it was only six pages long, uh, but the community at that time was small. So we did wonder, we did wonder whether it would be feasible, uh, to, uh, to actually plow through these six pages.”

Claim: The team was uncertain whether it would be feasible to formalize and check the six-page proof.

“It was only, it was only six pages long, uh, but the community at that time was small. So we did wonder, we did wonder whether it would be feasible, uh, to, uh, to actually plow through these six pages.”

Claim: The mathematical software community was small at the time of the proof-checking challenge.

“And I asked various people, and they were just like, "Well, could we make this email public?" So I asked Peter if he would write a blog post for my blog. I'd started a blog that was sort of promoting the software. So Peter wrote a blog post on my blog putting this as a challenge, and then people started popping up in the community saying, "Actually, I'd pr- be prepared to spend a substantial amount of time doing this."”

Claim: After the speaker asked Peter Scholze to publish the proof-checking challenge on the speaker's blog, community members volunteered to devote substantial time to it.

“And at, at the time, we imagined it would be about a year's worth of work. But then we started reading. We had to start reading the material, and we had to start reading it pro-- We, we were really the first people to be reading it, possibly.”

Claim: The team initially estimated that the proof-checking project would take about one year.

“And at, at the time, we imagined it would be about a year's worth of work. But then we started reading. We had to start reading the material, and we had to start reading it pro-- We, we were really the first people to be reading it, possibly. Uh, the first people not to skim through it. And, uh, we started going through it with a fine-tooth comb, and we found a simplification. Johan Commelin, in particular, found a simplification.”

Claim: The team began carefully reading Scholze's material and may have been the first group to read it in depth rather than skim it.

“Uh, the first people not to skim through it. And, uh, we started going through it with a fine-tooth comb, and we found a simplification. Johan Commelin, in particular, found a simplification.”

Claim: Johan Commelin found a simplification as the team carefully worked through Scholze's material.

“And, uh, six mo- So that cut the, that cut the time down by a factor of two. And six months later, we'd, we'd checked the key thing that Peter was-- You know, Peter was worried that the thing was wrong.”

Claim: The simplification found by Johan Commelin reduced the project's required time by half.

“And, uh, six mo- So that cut the, that cut the time down by a factor of two. And six months later, we'd, we'd checked the key thing that Peter was-- You know, Peter was worried that the thing was wrong. You know, Peter's like, "No, I think it's right. My co-author thinks it's right, Dustin Clausen. No one else has read it. Maybe it's wrong." So six months later, we'd read it through and was like, "It's okay.”

Claim: Six months after beginning the work, the team checked the key part of Scholze's proof that he feared might be incorrect.

“You know, Peter's like, "No, I think it's right. My co-author thinks it's right, Dustin Clausen. No one else has read it. Maybe it's wrong." So six months later, we'd read it through and was like, "It's okay.”

Claim: Peter Scholze and his co-author Dustin Clausen believed the proof was correct, but Scholze remained concerned that it might be wrong because nobody else had read it.

“You know, Peter's like, "No, I think it's right. My co-author thinks it's right, Dustin Clausen. No one else has read it. Maybe it's wrong." So six months later, we'd read it through and was like, "It's okay. It's right. The machine says it's right." And Peter got very excited, was just like, "Okay, so these systems are actually useful because they taught me something about how the proof works.”

Claim: The team and the machine concluded that the checked proof was correct.

“It's right. The machine says it's right." And Peter got very excited, was just like, "Okay, so these systems are actually useful because they taught me something about how the proof works.”

Claim: Peter Scholze became excited because the proof-checking systems were useful and taught him something about how the proof worked.

“You know, we've, we've found a more conceptual argument, a part of it, and, uh, and something is now actually finally read it." So he got excited and wrote a second blog post, which then, which then went viral in the community.”

Claim: The team found a more conceptual argument for part of Scholze's proof.

“You know, we've, we've found a more conceptual argument, a part of it, and, uh, and something is now actually finally read it." So he got excited and wrote a second blog post, which then, which then went viral in the community.”

Claim: Peter Scholze's second blog post about the work went viral within the mathematical community.

“And the next thing we know, you know, Quanta was on the, you know, you know, and, and Nature was cal- calling me up. And I-- It's at this point I realized that we had arrived now that, you know, now the sort of the big league people were taking an interest.”

Claim: After Scholze's blog post went viral, Quanta and Nature contacted the speaker, signaling that prominent people were taking an interest in the project.

“And, uh, and then it sort of, you know, it went on from there. Then, of course, once, you know, once we have some visibility, more and more people start coming into the community, professional mathematicians saying, "Well, can we actually do some stuff in my area here?"”

Claim: As the project became more visible, professional mathematicians increasingly joined the community and asked to formalize mathematics in their own fields.

“You know, an expert would come along, and their first question would be like, "Can we do my latest theorem?" And the answer was, "No, but we can do, you know, the basics in your area. And so here's where to start." And so the library started growing much more quickly then. The o- the other thing, of course, that happened around that time was COVID. Uh, so people were sort of stuck at home, and, uh, playing computer games was sort of an appealing way.”

Claim: The mathematical library began growing much faster as professional mathematicians contributed material in their areas.

“You know, an expert would come along, and their first question would be like, "Can we do my latest theorem?" And the answer was, "No, but we can do, you know, the basics in your area.”

Claim: At that stage, the system could not handle experts' latest theorems, but it could support formalizing basic material in their fields.

“And so here's where to start." And so the library started growing much more quickly then. The o- the other thing, of course, that happened around that time was COVID. Uh, so people were sort of stuck at home, and, uh, playing computer games was sort of an appealing way. Uh, you know, playing computer games while simultaneously engaging with interesting mathematics was-- some mathematicians found that a very appealing way to spend their time.”

Claim: During COVID, some mathematicians found it appealing to play computer games while simultaneously engaging with interesting mathematics.

“So there was a sort of a, a big sort of jump in the, the rate of growth of the library.”

Claim: The library's growth rate increased substantially during this period.

“When you have a mathematical proof in Lean fully spelled out, you can kind of click into elements of it, investigate, uh, and see how different parts of an argument really relate to each other.”

Claim: Lean allows users to interactively inspect elements of a fully formalized mathematical proof and examine how its parts relate.

“This ability to interact with the proof is something that Lean provides that a static PDF does not.”

Claim: Lean enables interaction with a mathematical proof, unlike a static PDF.

“So I was recently talking with some mathematicians at a book launch party for The Proof in the Code, and kind of late into the evening we start talking about whether you could apply the Alpha zero approach, the zero knowledge approach to like having an LLM recreate mathematics if you just give it kind of the basic axioms.”

Claim: The speaker and mathematicians discussed whether an AlphaZero-style, zero-knowledge approach could enable an LLM to recreate mathematics from basic axioms.

“Question we were talking about was would an LLM rediscover essentially kind of human mathematics or how far along would it get? And there was, uh, the kind of the consensus among these three mathematicians I was talking with was that it would not necessarily discover more than the rational numbers.”

Claim: Three mathematicians the speaker spoke with thought an LLM might not discover mathematics beyond the rational numbers.

“If you were kind of advancing along the kind of the human understanding of math, starting at the rational, it's almost at the very, very, uh, beginning. They expected computer math would diverge from kind of what has become, you know, human discovered math.”

Claim: The mathematicians expected computer-generated mathematics to diverge from human-discovered mathematics, beginning near the rational numbers on the progression of human mathematical understanding.

“And I think the reason is like we have this feel for the right abstractions, these kind of like satisfying concepts and definitions that, that feel right to us, that feel complete, that feel expansive in what they can-- in the kind of the work they can do when you, you know, when you start applying them in different scenarios.”

Claim: Humans have an intuition for mathematical abstractions and definitions that feel right and complete and prove broadly useful across different scenarios.

“And I think you're right to say that a computer doing this kind of search for things that are just like correct in some strict sense, some concrete sense would not be, um, its search would not be informed by th-those same kind of values.”

Claim: A computer searching only for strictly correct results would not be guided by the human values that inform mathematical intuition.

“And I think it would not stumble on the same things that the same mathematical concepts that have ultimately become meaningful to us.”

Claim: A computer searching for mathematically correct results would not necessarily discover the same concepts that became meaningful to humans.

“I don't think that's just like a weird artifact of like the reasoning about mathematics process. The idea that it felt right, I think that's probably native to, to cognition.”

Claim: The feeling that an idea is right is probably a general feature of cognition, not merely an artifact of mathematical reasoning.

“Very early on, there's this interest in using AI to do mathematics. Um, can AI solve math problems? It's a- um, it's both kind of just like an obvious like test because math is, you know, the pinnacle of human thought.”

Claim: The speaker describes AI's ability to solve mathematics as an obvious test because mathematics is the pinnacle of human thought.

“Very early on, there's this interest in using AI to do mathematics. Um, can AI solve math problems? It's a- um, it's both kind of just like an obvious like test because math is, you know, the pinnacle of human thought.”

Claim: Mathematics is an obvious test of AI because it represents the pinnacle of human thought.

“If AI can do that, perhaps it can do almost anything. Also, math is a very effective training environment for AI because you get a clear reward signal at the end. Has it done the problem correctly or not? That enables reinforcement learning, where you can have, uh, an AI system solve a problem, receive signal, did it do it correctly or not, do that very quickly, iterate a lot, get a lot better.”

Claim: Mathematics is an effective training environment for AI because solutions provide a clear reward signal indicating whether a problem was solved correctly.

“If AI can do that, perhaps it can do almost anything. Also, math is a very effective training environment for AI because you get a clear reward signal at the end.”

Claim: If AI can perform mathematics, it may be capable of doing almost anything.

“If AI can do that, perhaps it can do almost anything. Also, math is a very effective training environment for AI because you get a clear reward signal at the end.”

Claim: Mathematics provides an effective training environment for AI because solutions can receive a clear correctness-based reward signal.

“If AI can do that, perhaps it can do almost anything. Also, math is a very effective training environment for AI because you get a clear reward signal at the end.”

Claim: The speaker suggests that if AI can solve mathematics, it may be capable of doing almost anything.

“Has it done the problem correctly or not? That enables reinforcement learning, where you can have, uh, an AI system solve a problem, receive signal, did it do it correctly or not, do that very quickly, iterate a lot, get a lot better.”

Claim: In reinforcement learning, an AI system can solve a problem, receive a correctness signal, and iterate rapidly to improve.

“Has it done the problem correctly or not? That enables reinforcement learning, where you can have, uh, an AI system solve a problem, receive signal, did it do it correctly or not, do that very quickly, iterate a lot, get a lot better.”

Claim: In mathematics, reinforcement learning can improve an AI system through repeated problem-solving, correctness feedback, and rapid iteration.

“You need then to identify certain targets in math to set your AI against. And early on, one of the targets that's established is the International Math Olympiad.”

Claim: The International Math Olympiad was established early on as a target for AI mathematics systems.

“You need then to identify certain targets in math to set your AI against. And early on, one of the targets that's established is the International Math Olympiad.”

Claim: The International Math Olympiad was an early benchmark target for AI systems attempting mathematics.

“It's the premier pre-college math competition in the world. These are high school-aged students doing things that only require high school math. Those are the, the problems on the competition, but extraordinarily sophisticated versions of those questions.”

Claim: The International Math Olympiad is the leading pre-college mathematics competition worldwide, featuring highly sophisticated problems that require only high-school mathematics.

“It's the premier pre-college math competition in the world. These are high school-aged students doing things that only require high school math. Those are the, the problems on the competition, but extraordinarily sophisticated versions of those questions.”

Claim: The International Math Olympiad is the world's leading pre-college mathematics competition, featuring highly sophisticated problems that require only high-school mathematics.

“So early on, it set out, can AI achieve a gold medal-level score on the International Math Olympiad? Google DeepMind picks up this quest themselves.”

Claim: An early goal for AI mathematics research was to determine whether an AI system could earn a gold-medal-level score on the International Math Olympiad.

“So early on, it set out, can AI achieve a gold medal-level score on the International Math Olympiad? Google DeepMind picks up this quest themselves.”

Claim: An early benchmark for AI mathematics was whether a system could achieve a gold-medal-level score on the International Math Olympiad.

“In the book, I talk about the 2024 IMO, which is where Google DeepMind designs a system called AlphaProof, which is based on the same architecture as AlphaGo from a decade earlier almost.”

Claim: Google DeepMind designed AlphaProof for the 2024 International Math Olympiad using an architecture based on AlphaGo's, which had been developed nearly a decade earlier.

“In the book, I talk about the 2024 IMO, which is where Google DeepMind designs a system called AlphaProof, which is based on the same architecture as AlphaGo from a decade earlier almost.”

Claim: Google DeepMind designed AlphaProof for the 2024 International Math Olympiad using an architecture based on AlphaGo, which had been developed almost a decade earlier.

“They set it to work on the IMO. They train it to answer competition math-level problems, starting with basic middle school-level things. They do reinforcement learning, just like slowly re-reward climb until it is within range of IMO-level problems, and then they essentially administer the 2024 exam to AlphaProof.”

Claim: Google DeepMind trained AlphaProof with reinforcement learning, starting from basic middle-school mathematics and progressing toward International Math Olympiad-level problems.

“They set it to work on the IMO. They train it to answer competition math-level problems, starting with basic middle school-level things. They do reinforcement learning, just like slowly re-reward climb until it is within range of IMO-level problems, and then they essentially administer the 2024 exam to AlphaProof.”

Claim: DeepMind trained AlphaProof with reinforcement learning, beginning with middle-school-level problems and gradually progressing to International Math Olympiad-level problems before giving it the 2024 exam.

“Uh, they receive the questions after the competitors have finished their work to-- There's a kind of concern about the machine upstaging the human participants, so it receives the questions after the, the human competitors complete their work.”

Claim: At the 2024 International Math Olympiad, AlphaProof received the questions only after human competitors finished, amid concern that the machine could upstage them.

“Uh, they receive the questions after the competitors have finished their work to-- There's a kind of concern about the machine upstaging the human participants, so it receives the questions after the, the human competitors complete their work.”

Claim: AlphaProof was given the 2024 International Math Olympiad questions only after human competitors finished, in part because of concern that the machine might upstage them.

“It has more time than the human competitors. It has massive amounts of compute. Ultimately, it gets a silver medal-level score, and the way in which it, it solves the problems is by outputting Lean proofs and then using Lean to verify them.”

Claim: At the 2024 International Math Olympiad, AlphaProof had more time and substantially more compute than human competitors, earned a silver-medal-level score, and solved problems by generating proofs verified by Lean.

“It has more time than the human competitors. It has massive amounts of compute. Ultimately, it gets a silver medal-level score, and the way in which it, it solves the problems is by outputting Lean proofs and then using Lean to verify them.”

Claim: AlphaProof produced proofs in Lean and used Lean to verify its solutions to the competition problems.

“It has more time than the human competitors. It has massive amounts of compute. Ultimately, it gets a silver medal-level score, and the way in which it, it solves the problems is by outputting Lean proofs and then using Lean to verify them.”

Claim: At the 2024 International Math Olympiad, AlphaProof had more time and substantially more compute than human competitors and achieved a silver-medal-level score.

“DeepMind used Lean in both the, the reinforcement learning stages and then the actual problem-solving in the competition stages of, uh-- for the IMO.”

Claim: Google DeepMind used Lean in both AlphaProof's reinforcement-learning training and its competition-stage problem solving for the International Math Olympiad.

“DeepMind used Lean in both the, the reinforcement learning stages and then the actual problem-solving in the competition stages of, uh-- for the IMO.”

Claim: DeepMind used Lean in both AlphaProof's reinforcement-learning training and its competition-stage problem-solving for the International Math Olympiad.

“AlphaProof could not read the problems it was meant to solve. It took statements expressed in Lean and devised proofs in Lean, but competition problems arrive in natural language.”

Claim: AlphaProof could not directly read natural-language competition problems; it operated on statements and proofs expressed in Lean.

“DeepMind needed potentially millions of training problems. Formalizing each one by hand would create an impossible bottleneck, so the team had to find a way to translate competition mathematics into Lean automatically.”

Claim: Because manually formalizing the potentially millions of training problems DeepMind needed would create an impossible bottleneck, the team needed to translate competition mathematics into Lean automatically.

“The translation itself had structure. Algebra and number theory were easier because their natural language statements already contained equations and notation.”

Claim: Competition problems in algebra and number theory were easier to auto-formalize in Lean because their natural-language statements already included equations and notation.

“DeepMind eventually auto-formalized about eighty percent of questions in those areas nearly perfectly. Combinatorics was harder. Its questions read like stories full of natural language and relatively little notation.”

Claim: Google DeepMind eventually auto-formalized approximately 80 percent of algebra and number-theory questions with near-perfect accuracy.

“DeepMind eventually auto-formalized about eighty percent of questions in those areas nearly perfectly. Combinatorics was harder. Its questions read like stories full of natural language and relatively little notation.”

Claim: Combinatorics problems were harder to auto-formalize than algebra and number theory because they were presented as natural-language stories with relatively little notation.

“The mathematics could be discrete and computational, yet the human presentation made the formalization difficult. Despite that limitation, DeepMind produced on the order of tens of millions of problems stated in Lean.”

Claim: Even when combinatorics problems were discrete and computational, their human-readable presentation made them difficult to formalize.

“The mathematics could be discrete and computational, yet the human presentation made the formalization difficult. Despite that limitation, DeepMind produced on the order of tens of millions of problems stated in Lean.”

Claim: Despite difficulties in formalizing some mathematics, Google DeepMind generated on the order of tens of millions of problems expressed in Lean.

“Only then could AlphaProof's proof search begin. By September 2026, AI systems were tackling open research problems.”

Claim: AlphaProof's proof search could begin only after the Lean-formatted problem set had been produced.

“Only then could AlphaProof's proof search begin. By September 2026, AI systems were tackling open research problems.”

Claim: By September 2026, AI systems were working on open research problems.

“In Epoch AI's fixed budget test, a pre-release OpenAI model proved Erdős problem one hundred and twenty-six and disproved problem seventy-four by finding a counterexample.”

Claim: In Epoch AI's fixed-budget test, a pre-release OpenAI model proved Erdős problem 126 and disproved Erdős problem 74 by finding a counterexample.

“Both results were checked in Lean. It resolved two of sixty-eight problems. The other four models resolved none. And on September the eighth, OpenAI also published a claimed resolution of the Navier-Stokes millennium problem alongside a Lean formalization, but unfortunately not under the best circumstances.”

Claim: On September 8, OpenAI published what it claimed was a resolution of the Navier–Stokes millennium problem, accompanied by a Lean formalization.

“Both results were checked in Lean. It resolved two of sixty-eight problems. The other four models resolved none. And on September the eighth, OpenAI also published a claimed resolution of the Navier-Stokes millennium problem alongside a Lean formalization, but unfortunately not under the best circumstances.”

Claim: The other four models in Epoch AI's fixed-budget test resolved zero problems.

“Both results were checked in Lean. It resolved two of sixty-eight problems. The other four models resolved none. And on September the eighth, OpenAI also published a claimed resolution of the Navier-Stokes millennium problem alongside a Lean formalization, but unfortunately not under the best circumstances.”

Claim: The OpenAI model's two results in Epoch AI's test were checked in Lean, and it resolved two of the 68 problems.

“But that's outside the scope of this particular video. Back in September 2024, Terence Tao launched Equational Theories, an open collaboration mapping which algebraic laws imply others, with Lean checking the results.”

Claim: Terence Tao launched Equational Theories in September 2024 as an open collaboration to map implications among algebraic laws, with results checked in Lean.

“Within a month, the Equational Theories group had narrowed twenty-two million questions down to two hundred and thirty-eight. By late November, they were down to a hundred and thirty-eight.”

Claim: The Equational Theories collaboration narrowed 22 million questions to 238 within a month and to 138 by late November.

“By the end of March, they'd been stuck for several weeks on just four. But settling every implication had never really been the goal.”

Claim: The Equational Theories project was not primarily intended to settle every implication among algebraic laws.

“By the end of March, they'd been stuck for several weeks on just four. But settling every implication had never really been the goal.”

Claim: By the end of March, the Equational Theories group had spent several weeks unable to make progress on its remaining four questions.

“Tao viewed Equational Theories as a pilot project for a fundamentally new way of doing mathematics, and in that regard, it was an unqualified success.”

Claim: Terence Tao regarded Equational Theories as a pilot for a fundamentally new approach to mathematics and judged it an unqualified success as such.

“He imagined an experimental branch of mathematics analogous to modern physics, massive collaborations generating huge volumes of data, not replacing theory, but complementing it.”

Claim: Terence Tao envisioned an experimental branch of mathematics, analogous to modern physics, where large collaborations generate extensive data to complement—not replace—theory.

“The space of algebraic laws was a vast, largely unexplored planet. Familiar islands such as commutativity and associativity had been thoroughly studied, but most potential laws were unknown.”

Claim: The space of algebraic laws is vast and mostly unexplored; commutativity and associativity are well studied, while most potential laws remain unknown.

“Hidden among them might be structures strange and unlike anything mathematics had seen before, what Tao sometimes calls math from Mars.”

Claim: The largely unexplored space of algebraic laws might contain structures unlike anything previously encountered in mathematics, which Terence Tao sometimes calls “math from Mars.”

“As the team crossed implications off its immense table, it stumbled onto genuinely new constructions, including Magma cohomology.”

Claim: The Equational Theories team discovered new mathematical constructions, including Magma cohomology, while examining implications among algebraic laws.

“John Baez, an expert in cohomology who had initially called the project a colossal waste of time, admitted that he had never encountered it.”

Claim: John Baez, a cohomology expert and initial critic of Equational Theories, said he had never encountered Magma cohomology.

“To Tao, that was exactly the point. The project had demonstrated the efficacy of a new kind of mathematical machine.”

Claim: Terence Tao regarded the discovery as evidence that a new kind of mathematical machine could be effective.

“In July 2025, Google DeepMind and OpenAI reported gold-level scores on the International Mathematical Olympiad using natural language proofs.”

Claim: In July 2025, Google DeepMind and OpenAI reported gold-medal-level International Math Olympiad scores using proofs written in natural language.

“Google's result was officially graded by the IMO, and OpenAI's was separately evaluated. Neither relied on Lean to verify those competition answers.”

Claim: The International Math Olympiad officially graded Google DeepMind's result, whereas OpenAI's result was evaluated separately.

“Google's result was officially graded by the IMO, and OpenAI's was separately evaluated. Neither relied on Lean to verify those competition answers.”

Claim: Neither Google DeepMind's nor OpenAI's 2025 International Math Olympiad answers were verified using Lean.

“I think it's clearly gonna be elements of both, that Lean and reinforcement learning in that environment is gonna create these, the engines. It's gonna be, like, essential for model training.”

Claim: The speaker thinks both Lean and reinforcement learning in the relevant environment will be essential to creating engines for model training.

“I think it's clearly gonna be elements of both, that Lean and reinforcement learning in that environment is gonna create these, the engines. It's gonna be, like, essential for model training.”

Claim: The speaker expects both Lean-based verification and natural-language proofs to be used, and considers Lean combined with reinforcement learning essential for model training.

“I think it's also extremely useful for exploring a wide variety of possible proofs. I mean, that's kind of the value of an LLM, that it can output, you know, millions of potential proofs, but you need to then quickly sort among them to the ones that are plausible or correct.”

Claim: Lean is highly useful for filtering large sets of candidate proofs generated by an LLM, potentially millions, to identify plausible or correct proofs.

“I think it's also extremely useful for exploring a wide variety of possible proofs. I mean, that's kind of the value of an LLM, that it can output, you know, millions of potential proofs, but you need to then quickly sort among them to the ones that are plausible or correct. Lean can tell you which ones those are. Uh, at the same time, right, the expressive power of the models is getting so much better that you don't need everything to be outputted in Lean code to verify its correctness.”

Claim: The speaker thinks Lean is useful for exploring many candidate proofs because it can identify which candidates are plausible or correct.

“Lean can tell you which ones those are. Uh, at the same time, right, the expressive power of the models is getting so much better that you don't need everything to be outputted in Lean code to verify its correctness.”

Claim: Lean can identify which candidate proofs are correct or plausible.

“Lean can tell you which ones those are. Uh, at the same time, right, the expressive power of the models is getting so much better that you don't need everything to be outputted in Lean code to verify its correctness.”

Claim: As AI models become more expressive, it is not necessary for every proof to be expressed in Lean code in order to verify its correctness.

“Lean can tell you which ones those are. Uh, at the same time, right, the expressive power of the models is getting so much better that you don't need everything to be outputted in Lean code to verify its correctness.”

Claim: The speaker says models are becoming expressive enough that correctness can be verified without requiring every output to be in Lean code.

“So the philosophy of the library, uh, uh, has always been find the right abstraction and develop everything in that correct generality.”

Claim: The speaker says the library’s longstanding philosophy is to find the right abstraction and develop its contents at the correct level of generality.

“And what seems to be happening now is you can have an AI tool which just sees something in a book, doesn't think about it at all, just blindly translates that human-written, uh, mathematics into, you know, into Lean, the language, you know, the, the language that the software uses, and, uh, doesn't really care about making things easy.”

Claim: The speaker says AI tools can translate book mathematics into Lean without considering whether the resulting formalization is easy to work with.

“But AI in its current state doesn't really care about redesigning, and it's very happy to just plow through. So, you know, as, as an example, if we did want to change a fundamental definition in the library now, AI would be great at that.”

Claim: The speaker says current AI tools do not independently care about redesigning a library’s structure and will instead work through it as it is.

“But AI in its current state doesn't really care about redesigning, and it's very happy to just plow through. So, you know, as, as an example, if we did want to change a fundamental definition in the library now, AI would be great at that. AI would just cha- it would fiddle around at the roots, you know, break everything, and then it would just plow through and fix everything. And so now we have these new tools.”

Claim: The speaker says that if a fundamental definition in the library were changed, AI would be capable of modifying the foundations and repairing the resulting breakages throughout the library.

“You know, one, one can now question this fundamental design principle that, you know, do we, do we have to find the right level of generality? The Mathlib maintainers, you know, this, this fundamental maths library which everything is building on, we are still absolutely of the, the opinion that to get into our library, it needs to be, it needs to be, you know, conceptually, uh, the right, the right way of doing things.”

Claim: The speaker says Mathlib’s maintainers still require contributions to be conceptually well-founded and the right way of doing the mathematics.

“But, you know, in a year's time, there will be AI-developed libraries that will be much more poorly thought out in those terms because somehow trying to make it easy seems to be less of an issue.”

Claim: The speaker predicts that within a year AI-developed libraries will be less carefully designed conceptually, as ease of use appears to receive less attention.

“If you're prepared to just pour tokens into the problem, then we don't necessarily need to find, you know, the correct conceptual way of thinking about these things.”

Claim: The speaker says that when substantial tokens are spent on a problem, finding the conceptually correct approach may no longer be necessary.

“Uh, we could just bash something out and formalize a paper that came out last week. You know, and indeed this is what's happening. You know, companies like OpenAI and Anthropic are doing mathematics and then just translating it into Lean and not really thinking about whether this is all done in the correct generality.”

Claim: The speaker says OpenAI and Anthropic are doing mathematics and translating it into Lean without necessarily considering whether the work uses the correct level of generality.

“So the world is changing, and it's, and it's, it's not entirely clear it's gonna be better. It's just gonna be different.”

Claim: The speaker says AI-driven changes in mathematics are not clearly improvements, though they will make the field different.

“It's in two ways. A, right, I mentioned the kind of writing the fiddly Lean syntax is a real barrier to entry for mathematicians. Obviously, with, like, agentic coding, you don't need to, like, learn all that Lean.”

Claim: The speaker says agentic coding can let mathematicians use Lean without learning its detailed syntax, which is a barrier to entry.

“You can just kind of code it the way you would write, you know, JavaScript. There, there's an understanding that AI will make writing Lean code a lot easier and help probably bring more mathematicians into using the program.”

Claim: The speaker says AI is expected to make Lean coding much easier and probably increase the number of mathematicians who use Lean.

“There's enthusiasm about that. And then second, I mentioned that you need this library of digital mathematics, Mathlib, and all of that is very hand-curated material defined very manually.”

Claim: The speaker says Mathlib is a digital mathematics library whose contents have been manually curated and defined.

“There's a dream that you could take, uh, a full math textbook, show it to an AI, and have it automatically translate it, convert it into Lean code. This is the, the process of autoformalization.”

Claim: The speaker describes autoformalization as automatically translating a full mathematics textbook into Lean code using AI.

“There is hope in May of 2025 that autoformalization will dramatically, uh, accelerate the r- the rate at which new math is added to Mathlib.”

Claim: As of May 2025, there was hope that autoformalization would dramatically increase the rate of adding new mathematics to Mathlib.

“What's been interesting since the book came out, it came out in the States in June of this year. It's gonna come out in Europe later this month. What's been interesting is autoformalization is now happening. You can now give, uh, an LLM a math paper and it can spit out the Lean code version of it in, you know, a fraction of the time it would've taken a team of humans to do the same thing.”

Claim: The speaker says that autoformalization is occurring and that an LLM can convert a mathematics paper into Lean code in a fraction of the time required by a human team.

“The Mathlib community actually finds that this, there is a little bit of a Trojan horse, like there's kind of a downside to LLM autoformalization, and that is you just end up with this profusion of Lean mathematics that are, is not always defined with exactly, like, the precision, the economy with which you want these canonical objects in Mathlib to be expressed.”

Claim: The speaker says LLM autoformalization can generate large amounts of Lean mathematics that are not always expressed with Mathlib’s desired precision and economy for canonical objects.

“everything, in this case lean code you might admit to Mathlib is not always at the standard the community itself wants, and they have to figure out how to kind of sift through all of this new material.”

Claim: The speaker says the Mathlib community has to filter AI-generated Lean code because some of it falls below the community’s desired standard.

“So we have a real serious problem now with the spaghetti monster, right? We are writing code that we no longer understand. We don't understand our code bases anymore, and we need to have some kind of way of building specifications which are computer checkable.”

Claim: The speaker says people are writing code they no longer understand and need computer-checkable specifications.

“But a checked proof can still be a proof of the wrong thing. When an AI produces a lean proof of a famous conjecture, someone must still establish that the formal statement captures the intended conjecture with appropriate definitions and assumptions.”

Claim: The speaker says a formally checked proof may prove the wrong proposition, so a person must verify that an AI-generated Lean statement accurately represents the intended conjecture, definitions, and assumptions.

“But a checked proof can still be a proof of the wrong thing. When an AI produces a lean proof of a famous conjecture, someone must still establish that the formal statement captures the intended conjecture with appropriate definitions and assumptions.”

Claim: A proof checker can verify a derivation without ensuring that the formal statement correctly represents the intended conjecture, definitions, and assumptions.

“The checker certifies the derivation, but it doesn't certify the human choice of target. This is the formalization gap.”

Claim: A proof checker certifies a derivation but not whether humans chose the intended target, a limitation described as the formalization gap.

“The checker certifies the derivation, but it doesn't certify the human choice of target. This is the formalization gap.”

Claim: The speaker says a proof checker verifies the derivation but not whether the human-selected formal target is the intended one, a problem called the formalization gap.

“The trust has basically moved upstream.”

Claim: The speaker says trust in formal proof workflows has largely shifted upstream, toward the earlier choices involved in formalization.

“The trust has basically moved upstream.”

Claim: The speaker says trust in formal proof workflows has shifted upstream, toward the choice and formulation of the target being proved.

“Mathematics is a, you know, is a well-specified formal language. Uh, and that's exactly why, that's exactly why we can write, uh, computer programs that understand this math-- you know, that understand, uh, what, what humans mean when they speak in mathematical terms.”

Claim: The speaker describes mathematics as a well-specified formal language that enables computer programs to interpret mathematical statements as humans intend them.

“So mathematics should contain no ambiguities at all. Uh, so in theory, in, in theory, mathematics is completely well specified and, and thus perfect for this kind of game, you know, writing it down in a formal system, uh, using a computer program.”

Claim: The speaker says that, in theory, mathematics has no ambiguity and is completely well specified, making it suitable for formalization in a computer system.

“But in practice, uh, reading recent mathematical papers, we, we do see that there's a certain amount-- there is a certain amount of people speaking to other experts and just knowing-- Experts sort of know what humans mean when they say things.”

Claim: The speaker says mathematical papers in practice rely partly on expert readers inferring intended meaning through shared understanding.

“So sometimes what ends up on paper is sort of ninety-nine percent, but not a hundred percent representative, uh, of what humans mean by mathematics.”

Claim: The speaker says mathematical writing sometimes represents intended meaning only about 99 percent, rather than 100 percent, accurately.

“And a few years ago, I would not have said that. A few years ago, I would have said, "Humans are excellent. Humans are perfect. You know, the, the experts, they write down, they write down exactly what they mean at all times."”

Claim: The speaker says that a few years earlier, they believed mathematical experts always wrote exactly what they meant.

“Uh, so we wrote down the statements of fifty, um, fifty theorems from this top pure math journal, the Annals of Mathematics.”

Claim: The speaker's team formalized the statements of 50 theorems published in the Annals of Mathematics.

“Uh, and we're going to make them public this week. But before we made them public, we ran them, we ran them through an AI and asked an AI to check them.”

Claim: The speaker's team planned to publish its formalized theorem statements that week and used an AI to check them before publication.

“And the AI found s- and the AI found errors, and the errors were of two forms. There were errors that my team had made. You know, we'd, um, we'd f-failed to correctly translate what it said on the page, uh, into the language of the software.”

Claim: An AI checker found errors where the speaker's team had incorrectly translated theorem statements from papers into the formal software language.

“But there were more interesting errors where we had faithfully translated exactly what it said in the paper, but what it said in the paper was just not true because they were just, they were just slips.”

Claim: An AI checker found theorem statements that the team had translated faithfully but that were false as written because of author errors or omissions.

“They were-- The humans hadn't bothered to mention that obviously N had to be at least three, or obviously this set should be non-empty.”

Claim: Some theorem statements omitted necessary conditions, such as requiring N to be at least 3 or requiring a set to be non-empty.

“There, there were, there were things that, that hu-- And this was Fields Medals, right? We found, we found four Fields medallists have actually proved theorems in the Annals of Mathematics, and if you actually read the statement of the theorem, then strictly speaking, that theorem is not true, right?”

Claim: The speaker says the team found that theorem statements by four Fields Medalists, published in the Annals of Mathematics, were strictly false as written.

“It, it's-- strictly speaking, what they've written is false. And it is obviously not true, in fact. If you're an expert in the area, you would say, "Well, obviously they mean this."”

Claim: The speaker says subject-matter experts can infer the intended meaning when a theorem is false as literally written.

“So the, the process of-- You know, I think this is quite humbling. I think as the c-- as a community, uh, you know, we should take a look and we, we should step back and think, well, actually, you know, we say we've got this precise formal language where we can express exactly what we mean.”

Claim: The speaker believes the mathematical community should reconsider its assumption that mathematical writing always expresses intended meaning exactly, describing the evidence as humbling.

“Uh, but in practice, uh, we're only using it at sort of ninety-nine percent capacity. And one of the things that machines will offer you is the chance to upgrade that to a hundred percent capacity.”

Claim: The speaker says mathematical practice uses its formal language at roughly 99 percent capacity, and machines could help bring its use to 100 percent.

“You know, the machines will say, "Well, this theorem as you've written it isn't actually true, is it?" And then the human will, "Well, obviously not. Obviously, everybody knows that we mean this." But now-- But why don't we just write that down now?”

Claim: The speaker says machines can identify false theorem statements and prompt mathematicians to state their intended meaning explicitly.

“So, you know, this is one of the ways in which the software is making mathematics better. It's getting you from ninety-nine percent to a hundred percent. You know, humans are not as smart as we think we are.”

Claim: The speaker says software improves mathematical precision by helping move practice from about 99 percent to 100 percent, and that humans are less smart than they believe.

“In the early days of interactive proof assistance, like I said, the argument that we need these because they're gonna check correctness and get the details right, that got no traction in the mathematics community.”

Claim: The speaker says early arguments for interactive proof assistants based on checking correctness and details were not persuasive to the mathematics community.

“'Cause mathematicians, they'd push back and they'd say, "Look, mathematics isn't about formalism, isn't about axioms and rules. It's not about checking the details. It's about the ideas.”

Claim: The speaker says mathematicians have argued that mathematics is fundamentally about ideas and understanding rather than formalism and detail-checking.

“It's about the understanding." Um, and, you know, you come up with ideas. You know, when you go to formalize a proof, that, that's where the mathematics just, is, is just, it's just dying. I mean, it's just you gotta do it. You gotta check, you know, you gotta check carefully. But that's not what we really care about. We care about the ideas, and often the ideas, they are about coming up with the new representations, ways of thinking about things that will let you solve harder problems and, and get further.”

Claim: The speaker says mathematical progress comes from developing ideas and representations that enable solutions to harder problems.

“Um, so um, I mean, that said, one of the things that characterizes mathematics is the level of rigor and precision and the fact that, you know, we can come to consensus about whether a proof is correct or not, and that's a matter of checking the details and the rules at the bottom.”

Claim: The speaker says mathematics is characterized by rigor and precision, with proof correctness established through checking details and foundational rules.

“So, you know, the way I like to think about it is mathematics and that level of precision and rigor, that, that's the medium. That's the language, right, in which, you know, mathematicians work.”

Claim: The speaker characterizes mathematical precision and rigor as the medium in which mathematicians work.

“And within that medium, then you have this, you know, you have this platform on which to build these incredibly creative ideas and modes of representation and understandings. So what we really love are the ideas, but they're couched in, in this form, in this framework where we can be very precise.”

Claim: The speaker says mathematical rigor provides a precise framework for developing creative ideas, representations, and understanding, which are what mathematicians value.

“To my surprise, you know, around 2000, after, you know, Kevin Buzzard started blogging and, you know, his blog went viral, a lot of very talented mathematicians came to the subject and got really excited about formalization.”

Claim: Around 2000, Kevin Buzzard's viral blog helped bring many talented mathematicians to mathematical formalization and made them excited about it.

“And I think what they liked about it was, you know, when you go back to a piece of mathematics that you think you understood, but now you have to represent it formally, you have to represent it in a way that the computer can, can understand and check every detail, you find yourself getting very efficient about how you represent concepts and put them together.”

Claim: The speaker thinks formalizing familiar mathematics for computer checking encourages mathematicians to represent concepts and combine them more efficiently.

“What's the kind of the internals? And so I think mathematicians found it useful to think about mathematics in this kind of software engineering, you know, kind of way of thinking about, okay, you know, what are the different modules? What are the pieces? How do they interact? What are the, the interfaces? I think that they found that this gave them a way of coming back and, and understanding, you know, the mathematics in, in, in new and interesting ways.”

Claim: The speaker thinks software-engineering concepts such as modules, interfaces, and interactions help mathematicians understand mathematics in new ways.

“So it's really just, yeah, exploring the, the structure of, of mathematics and how the pieces get put together. I mean, we, we build up these, these, these very complex edifices on top of these, you know, kind of very, very precise rules and understanding how you get that level of complexity, you know, down to the, the very simple rules at the bottom, um, is really remarkable.”

Claim: Formalization explores how complex mathematical structures are assembled from precise, simple rules.

“In many ways, coming up with the right definition for an object is the whole game in mathematics. When mathematicians define new objects or new frameworks and abstractions, they are equipping the field with new tools and perspectives.”

Claim: Choosing definitions for mathematical objects is often central to mathematics because new definitions, frameworks, and abstractions provide new tools and perspectives.

“And Schultze worried that if the definitions were wrong in Lean, nobody could tell. Lean might verify the proof as correct even when it wasn't.”

Claim: Schultze worried that incorrect definitions in Lean might go unnoticed, allowing Lean to verify a proof as correct even when the proof was not correct.

“He summed up the conundrum on Zulip. "I'm just currently feeling that mathematics remains a human activity, because if I were to truly check that the computer did the right thing, I would have to unravel the whole proof in my head and check that it really adds up."”

Claim: Schultze said mathematics remains a human activity because independently checking a computer's work would require him to mentally reconstruct and verify the entire proof.

“Lean could verify proofs, but it couldn't check definitions because, logically speaking, definitions aren't right or wrong. They're just what you say they are.”

Claim: Lean can verify proofs but cannot determine whether definitions are correct, since definitions are stipulations rather than logically true or false statements.

“So Comerlin and Topaz looked for another form of reassurance. They created a file of concrete examples, unit tests for the most important definitions.”

Claim: Comerlin and Topaz used a file of concrete examples as unit tests to provide reassurance about important Lean definitions.

“If the definitions yielded objects that looked like a duck and quacked like a duck, perhaps they really were defining a duck. The examples were not watertight evidence, but Comerlin thought they were at least as reliable as reading definitions in a mathematical paper, perhaps even more so, given how easy it is for mathematicians to see what they expect to see when reviewing one another's work.”

Claim: Comerlin thought testing definitions with concrete examples was at least as reliable as reading definitions in mathematical papers, and perhaps more reliable, because reviewers may see what they expect to see.

“And the choice is really unique. Concepts that look equivalent on paper can be represented in several formally valid ways.”

Claim: Mathematical concepts that appear equivalent on paper may have multiple formally valid representations.

“A choice that works locally can become brittle or even unrecognizable when a library grows around it. Mathematics has its own integration hell, and every plausible-looking contribution creates a review burden for somebody else.”

Claim: A mathematical representation that works locally can become brittle or unrecognizable as the surrounding library grows.

“A choice that works locally can become brittle or even unrecognizable when a library grows around it. Mathematics has its own integration hell, and every plausible-looking contribution creates a review burden for somebody else.”

Claim: Each plausible-looking contribution to a mathematical library imposes a review burden on another person.

“I was trying to build something that works. Some people were there in the Slack channel having fun, uh, throwing ideas on the wall, right?”

Claim: The speaker was focused on building a working project, while some Slack-channel participants were casually proposing ideas.

“I mean, it's cheap. I mean, you can throw ideas on the wall a-a-and the other side has to keep telling you, "No, this doesn't work."”

Claim: Casually proposing ideas is low-cost for the proposer because others must spend effort explaining why they fail.

“Something that's, for me, one frustrating scenario. You throw an idea. You, you didn't spend five minutes thinking about it. Then I find a hole. I send back to you. Then you polish a little bit, send back. Now it takes ten minutes to find the hole, the next hole.”

Claim: The speaker found it frustrating when people proposed ideas without thinking them through, leaving the speaker to identify their flaws.

“It keeps taking exponentially longer to find the holes on the half-baked idea. Uh, for the person coming up with them, it's fun.”

Claim: The speaker said identifying flaws takes exponentially longer as a half-baked idea is incrementally revised and resubmitted.

“It keeps taking exponentially longer to find the holes on the half-baked idea. Uh, for the person coming up with them, it's fun. I mean, but it's not fun from the receiver, right? You have to do your work now. You spend time telling people why this is not a good idea, why it's not the time you should do it.”

Claim: Proposing half-baked ideas may be fun for the proposer but burdens the recipient with explaining why the ideas are unsuitable or mistimed.

“So we, we should come up with a concrete example here. So, um, apparently Kim Morrison used a Claude agent to produce a Lean implementation of the compression format zlib and, um, and, and prove some specific properties of it.”

Claim: Kim Morrison used a Claude agent to create a Lean implementation of zlib and prove specific properties of the implementation.

“But the AI managed to translate from C to Lean, the code, then managed to keep fixing the Lean implementation to each passage that has suites that comes w-with the C version.”

Claim: The AI translated zlib's C code into Lean and iteratively corrected the Lean implementation to pass the C version's test suites.

“And then it proves that for any compression level, for any data, if you compress the data and then decompress, you get the original data back.”

Claim: The Lean proof establishes that zlib compression followed by decompression returns the original data for any data and any compression level.

“And I, I don't know whether there is a similar thing with this zlib, whether it actually encompassed the whole or just some perspective of it. But I, I suppose the problem when you only have a, a perspective of a bigger complex whole, you, you get problems in terms of, you know, we're talking about reward hacking and, um, you know, like Goodhart's law and, and all, all kinds of, you know, degenerate behavior can happen if you optimize only part of a system.”

Claim: Optimizing only part of a larger system can produce reward hacking, Goodhart-like effects, and other degenerate behavior.

“And I, I don't know whether there is a similar thing with this zlib, whether it actually encompassed the whole or just some perspective of it. But I, I suppose the problem when you only have a, a perspective of a bigger complex whole, you, you get problems in terms of, you know, we're talking about reward hacking and, um, you know, like Goodhart's law and, and all, all kinds of, you know, degenerate behavior can happen if you optimize only part of a system.”

Claim: The speaker is uncertain whether the zlib formalization covered the entire algorithm or only a partial perspective of it.

“And I, I don't know whether there is a similar thing with this zlib, whether it actually encompassed the whole or just some perspective of it. But I, I suppose the problem when you only have a, a perspective of a bigger complex whole, you, you get problems in terms of, you know, we're talking about reward hacking and, um, you know, like Goodhart's law and, and all, all kinds of, you know, degenerate behavior can happen if you optimize only part of a system.”

Claim: Optimizing only one part of a larger system can produce reward hacking, Goodhart effects, and other degenerate behavior.

“Suppose that, that was the only property we ask is the, the, the AI to show, to demonstrate to us that was achieved. The AI could hack by saying, "Compression, you just return the data. It's the identity function. You just return. Decompression, you return it back." You prove the property, right? But then you, you can put more properties, like saying, you, you... the outputs should be smaller than inputs, right?”

Claim: If an AI is evaluated only on demonstrating compression and decompression, it could satisfy the stated property by returning the input unchanged during compression and returning it back during decompression.

“It's the identity function. You just return. Decompression, you return it back." You prove the property, right? But then you, you can put more properties, like saying, you, you... the outputs should be smaller than inputs, right? Then you, you should also tell the, uh, uh, the AI, you have to show that you compress as much as the Rust implementation in the test suites.”

Claim: Requiring compressed outputs to be smaller than inputs and requiring compression performance comparable to the Rust implementation in the test suites can constrain an AI's ability to exploit an underspecified compression task.

“But you're completely right. It is really easy to give properties that do not cover the whole thing, right? And if you want to do-- If you see the AI as an assistant to you, that's...”

Claim: It is easy to define properties that fail to cover all aspects of a task.

“You're in the loop looking at the codes, I, I think this is not super concerning, this problem you raised.”

Claim: The risk from incomplete specifications is not very concerning when a human remains in the loop and reviews the code.

“But if you let, want to let the AI go wild, and you don't even want to look at the codes, it's really important to cover all aspects, right?”

Claim: When an AI operates without human code review, its specifications need to cover all aspects of the task.

“Otherwise, you can have implementation that satisfies all your properties, but you do not fully specify what you wanted. You, you're not really getting what you want.”

Claim: An implementation may satisfy every stated property yet fail to meet the user's intent when the specifications do not fully describe the desired behavior.

“The utility of agentic coding is completely bottlenecked right now on this review and verification phase. Uh, I think that AI itself makes software verification kind of much more powerful because you can use AI to write these specifications themselves.”

Claim: The current utility of agentic coding is bottlenecked by code review and verification.

“The utility of agentic coding is completely bottlenecked right now on this review and verification phase. Uh, I think that AI itself makes software verification kind of much more powerful because you can use AI to write these specifications themselves.”

Claim: AI can make software verification more powerful by helping write software specifications.

“They don't have to be written by hand. But it's, uh, I think kind of formal verification of software programs will, like, increasingly have a role to play in the new AI-powered software development life cycle.”

Claim: Formal verification of software programs will play an increasingly important role in AI-powered software development.

“There are places like Harmonic, which believe that if you can train an AI model to write math proofs, that same intelligence will be useful for writing proofs about software, for verifying the, the output of, um, of LLMs.”

Claim: Harmonic and similar proponents believe that AI models capable of writing mathematical proofs could also write software proofs to verify LLM outputs.

“So I don't know. That, that kind of bet is underway. Whether or not it pans out, I don't know.”

Claim: The speaker is uncertain whether using AI proof-writing to verify software and LLM outputs will succeed.

“So AI is coming for mathematics. This is absolutely clear. And what it's gonna do to it, uh, nobody really knows.”

Claim: AI's impact on mathematics is inevitable, but its eventual effects are unknown.

“Uh, all that we know is it's getting really good really quickly, and no one has any understanding of how much better it's gonna get. So mathematicians have had various different reactions to this, ranging from, uh, you know, what could only be described as grief, uh, that, uh, that the subject is changing and, uh, and that they're gonna have to adapt or, or die. Uh, so ranging from grief to excitement, and I'm very much at the excitement end of the scale. I think mathematics is gonna be hugely accelerated by this software because remember, it's already doing interesting things, and the thing you have to remember is it's, it's worse.”

Claim: Mathematicians' reactions to AI range from grief over changes to their field and pressure to adapt to excitement.

“Uh, all that we know is it's getting really good really quickly, and no one has any understanding of how much better it's gonna get. So mathematicians have had various different reactions to this, ranging from, uh, you know, what could only be described as grief, uh, that, uh, that the subject is changing and, uh, and that they're gonna have to adapt or, or die.”

Claim: AI capabilities are improving rapidly, but the extent of future improvement is unknown.

“Uh, so ranging from grief to excitement, and I'm very much at the excitement end of the scale. I think mathematics is gonna be hugely accelerated by this software because remember, it's already doing interesting things, and the thing you have to remember is it's, it's worse.”

Claim: The speaker is strongly excited about AI's effects on mathematics.

“Uh, so ranging from grief to excitement, and I'm very much at the excitement end of the scale. I think mathematics is gonna be hugely accelerated by this software because remember, it's already doing interesting things, and the thing you have to remember is it's, it's worse.”

Claim: The speaker expects AI software to greatly accelerate mathematics, noting that it is already producing interesting results.

“You know, today is the worst it will be, right? Going forward, it's gonna be much better. It is already awesome, and it's much worse than what it will be this time next year.”

Claim: AI capabilities will be substantially better next year than they are today.

“So I think AI opens up huge new possibilities for mathematics. It will change many things about it, but at the end of the day, uh, we're gonna end up with more understanding, we're gonna end up with more theorems proved, and we're gonna end up, you know, with just a better overview of what mathematics is and, uh, and, and great tools where we can explore new dark corners, uh, and enlighten them and enlighten, uh, our community.”

Claim: AI creates major new possibilities for mathematics and will change many aspects of the field.

“So I think AI opens up huge new possibilities for mathematics. It will change many things about it, but at the end of the day, uh, we're gonna end up with more understanding, we're gonna end up with more theorems proved, and we're gonna end up, you know, with just a better overview of what mathematics is and, uh, and, and great tools where we can explore new dark corners, uh, and enlighten them and enlighten, uh, our community.”

Claim: The speaker expects AI to increase mathematical understanding and the number of proved theorems, improve the overview of mathematics, and provide tools to explore previously obscure areas.

“So going forward, things look very exciting.”

Claim: The speaker views the future of AI and mathematics as very exciting.

“What, what makes our goals special is that they're ours. They're our goals. I mean, you and I are having this conversation, right? And the conversation is what should we do?”

Claim: The speaker says human goals are special because they belong to the people pursuing them.

“What, what makes our goals special is that they're ours. They're our goals. I mean, you and I are having this conversation, right? And the conversation is what should we do?”

Claim: Human goals are special because they are the goals of humans.

“What should we make of AI, and how should we res-respond to AI, and what should we do with AI, right? We're having this conversat-- I mean, I'm happy to let AI have its discussion on the side about what, what its goals are and what it should be trying to do, right? That doesn't interest me, right? I mean, you tell me that there's some server in the corner and it's doing whatever it's doing and proving theorems and so on. You know, again, what I care about is how, how am I gonna interact with it?”

Claim: The speaker cares about how humans interact with AI, not about AI discussing its own goals.

“So, um, yeah, I... it's not that... I, I don't know. It's, uh, again, the questions I think that we should be interested in are what are our goals and what should we be doing to achieve them?”

Claim: People should focus on identifying their own goals and deciding what actions will achieve them.

“So, um, yeah, I... it's not that... I, I don't know. It's, uh, again, the questions I think that we should be interested in are what are our goals and what should we be doing to achieve them?”

Claim: People should focus on identifying their goals and deciding what actions to take to achieve them.

“Um, so I mean, it's anthropocentrism only in that that's what we are, right? Um, so yeah, I, I think we should be at the center of the debate just because we're the ones having the debate.”

Claim: Humans should remain at the center of the AI debate because humans are the participants in that debate.

“Um, so I mean, it's anthropocentrism only in that that's what we are, right? Um, so yeah, I, I think we should be at the center of the debate just because we're the ones having the debate.”

Claim: The speaker thinks humans should be at the center of the AI debate because humans are conducting that debate.

“If, if it's our, insofar as it's our debate, it... we, we can't help it make it about, help but make it about what you know, what we want.”

Claim: The speaker says a debate conducted by humans inevitably becomes focused on human wants.

“If, if it's our, insofar as it's our debate, it... we, we can't help it make it about, help but make it about what you know, what we want.”

Claim: Because humans are conducting the debate, they inevitably frame it around what humans want.

“Not like for the world, but just like as a kind of an ethical contract almost between me and the sources, which is this was Leo's life work, and he cared a tremendous amount about it.”

Claim: Leo Demora regarded the work discussed as his life's work and cared deeply about it.

“And my book was likely to be the only kind of start to finish story of the development of Lean and just started to feel extremely important to tell the story well.”

Claim: The speaker believed his book was likely to be the only comprehensive account of Lean's development and therefore felt it was important to tell that story well.

“And I was contacted by a guy called Kevin Hartnett, uh, who at the time worked for Quanta Magazine and wanted to run a piece on, on Lean's, Lean and its mathematics library, uh, for Quanta.”

Claim: Kevin Hartnett worked for Quanta Magazine when he approached the speaker about an article on Lean and its mathematics library.

“So I, I ran into Kevin around then and we, you know, we became friends and, uh, and he interviewed me several times about several things.”

Claim: Kevin Hartnett and the speaker became friends, and Hartnett interviewed the speaker multiple times on different subjects.

“And, uh, then later on decided that this was such an interesting story that it was sort of worth writing a book on. Uh, uh, you know, a decision which I thought was quite an interesting one, but he, he went for it.”

Claim: Kevin Hartnett later decided that the story was sufficiently interesting to warrant a book.

“And during that time he interviewed me many more times and tried to get some kind of idea as to sort of how it happened.”

Claim: While writing the book, Kevin Hartnett interviewed the speaker repeatedly to understand how the events unfolded.

“He, you know, he wanted to put together, you know, the people behind the story and what was going on. And so my midlife crisis, uh, where I started worrying about human generated mathematics and asking whether machines could do it better somehow played a role, uh, in Kevin's, uh, in the story that Kevin decided to tell.”

Claim: The speaker's concerns about whether machines could produce mathematics better than humans became part of Kevin Hartnett's account of the story.

“Um, as I met more, more figures in the book, more mathematicians, I similarly understood how important it was to them. I spent a lot of time with the six or seven key core sources for the book.”

Claim: Meeting more mathematicians featured in the book helped the speaker understand how important the work was to them.

“It was also very useful to me that this group of people left a tremendous digital record of all of their work. They, um, were initially a- very active over email and they shared a large, you know, a large number of their private emails with me.”

Claim: The group documented much of its work digitally, and its members shared many private emails with the speaker.

“They also then later migrated to this chat platform called Zulip, where they conducted a lot of their work in these public threads and then also in private DMs, which they shared with me.”

Claim: The group later used Zulip for work in public threads and private direct messages, and shared those messages with the speaker.

“And so I was able to kind of reconstruct a lot of the work as if I was like there observing it and in the moment it was taking place. So that was like a tremendous benefit to writing the book.”

Claim: Access to the group's digital records enabled the speaker to reconstruct its work in near-contemporaneous detail, greatly benefiting the book's writing.

“You know, you don't wanna air your dirty laundry, uh, you know, in, in public. I mean, the, the thing about the people working on Lean, it's just a wonder-- it's like family.”

Claim: The speaker describes the Lean project’s contributors as a close-knit, family-like community.

“You know, you don't wanna air your dirty laundry, uh, you know, in, in public. I mean, the, the thing about the people working on Lean, it's just a wonder-- it's like family.”

Claim: The speaker describes the Lean community as being like a family.

“You know? It's just a wonderful community of, of good friends, and e- everybody working on the project was kind of young and idealistic and excited about it, and, you know, we all felt that we were doing something interesting and important.”

Claim: The speaker characterizes the Lean community as close-knit, idealistic, and enthusiastic about the project.

“You know? It's just a wonderful community of, of good friends, and e- everybody working on the project was kind of young and idealistic and excited about it, and, you know, we all felt that we were doing something interesting and important.”

Claim: The speaker says that Lean project contributors were young, idealistic, and excited, and felt their work was interesting and important.

“y- you know, there were, there were the, the, the bumpy spots along the way, and there were the, um, you know, the, there were these tensions and-- But we don't wanna dwell on them, right?”

Claim: The Lean project experienced difficulties and tensions, which its participants preferred not to emphasize publicly.

“And so an outside reporter, you know, journalist comes in, and so we were very guarded at first. Uh, but I think we, we came to trust Kevin when it really became clear that he wasn't looking for, you know, good guys and bad guys or an exposé or a scandal story or anything like that, that he was really trying to tell a s- tell the story in a way that was respectful to everyone, uh, involved.”

Claim: The speaker says Lean project participants came to trust Kevin Hartnett after recognizing that he aimed to tell their story respectfully rather than produce an exposé or scandal story.

“And so an outside reporter, you know, journalist comes in, and so we were very guarded at first. Uh, but I think we, we came to trust Kevin when it really became clear that he wasn't looking for, you know, good guys and bad guys or an exposé or a scandal story or anything like that, that he was really trying to tell a s- tell the story in a way that was respectful to everyone, uh, involved.”

Claim: The speaker says that Lean project participants were initially guarded toward outside journalist Kevin Hartnett.

“And so an outside reporter, you know, journalist comes in, and so we were very guarded at first. Uh, but I think we, we came to trust Kevin when it really became clear that he wasn't looking for, you know, good guys and bad guys or an exposé or a scandal story or anything like that, that he was really trying to tell a s- tell the story in a way that was respectful to everyone, uh, involved.”

Claim: The Lean group initially approached Kevin Hartnett cautiously, then came to trust him because he aimed to tell the story respectfully rather than pursue an exposé or assign heroes and villains.

“Um, so when that, when that was the case I think, uh, I mean, he really spoke to a lot of people, um, and I think he really did a good job of capturing the feel and the excitement of, of working on the project.”

Claim: The speaker believes Kevin Hartnett interviewed many people and effectively conveyed the atmosphere and enthusiasm of working on Lean.

“Um, so when that, when that was the case I think, uh, I mean, he really spoke to a lot of people, um, and I think he really did a good job of capturing the feel and the excitement of, of working on the project.”

Claim: The speaker believes Kevin Hartnett effectively captured the atmosphere and excitement of working on Lean.

“Um, and, uh, um, and when there were tensions involved, uh, sort of, you know, making them, making it come across that, again, it wasn't a matter of good guys and bad guys but just people looking, uh, for different things.”

Claim: The speaker characterizes tensions within the Lean project as conflicts among people with different aims, rather than a struggle between good and bad people.

“Um, and, uh, um, and when there were tensions involved, uh, sort of, you know, making them, making it come across that, again, it wasn't a matter of good guys and bad guys but just people looking, uh, for different things.”

Claim: Kevin Hartnett portrayed tensions within the project as differences in what people wanted, rather than as a conflict between good and bad actors.

“There was this experience I had reporting it where for a period around 2018, Leo goes off and builds Lean 4 and simultaneously all the math activity and math lib is still c- continuing at pace.”

Claim: Around 2018, Leo worked on building Lean 4 while mathematical activity and Mathlib development continued at pace.

“Ultimately what I learned is there had been a, a somewhat decisive fracture between Leo and the math community where he says, "I'm gonna go off on my own and build Le- Lean 4.”

Claim: The reporter says he learned that Leo’s decision to build Lean 4 independently marked a decisive fracture between Leo and the mathematics community.

“Please leave me alone," in so many words. And they kind of, they kind of actually, they get the message. They're a little wary of like angering this guy who they admire and is so, is so important to them.”

Claim: The reporter says Leo communicated that he wanted to build Lean 4 independently and be left alone, and the mathematicians understood that message.

“There's some particular personality conflicts that I talk about in the book between Leo and this guy, Mario Carneiro, who both are-- just have strong visions for what they want this kind of emerging world to look like.”

Claim: The reporter says Leo and Mario Carneiro had personality conflicts and strong, differing visions for the emerging Lean ecosystem.

“Mario's vision is what he wants math lib to look like. He's very much a big open source believer. Leo's vision is for like Lean. The two of them clash quite a lot and in certain ways kind of, uh, that friction pushes Leo away from the mathematicians in this way in this 2018 to 2022 period.”

Claim: The reporter says Mario Carneiro’s open-source vision for Mathlib clashed with Leo’s vision for Lean, and that this friction contributed to Leo’s distance from mathematicians between 2018 and 2022.

“Leo was mad and kind of had left, left this sphere for a little while. Uh, and of course once, once you get one person to, to explain their side of the story, others, um, are kind of more forthcoming about theirs as well.”

Claim: The reporter says that hearing one person’s account made other people more willing to share their own accounts.

“Leo was mad and kind of had left, left this sphere for a little while. Uh, and of course once, once you get one person to, to explain their side of the story, others, um, are kind of more forthcoming about theirs as well.”

Claim: The reporter says Leo was angry and had withdrawn from the Lean community for a period.

“Oh, so, so, uh, so if, if you read the book, there was a, a period where Leo was just kind of frustrated with, with, uh, well really all users but especially the mathematical users.”

Claim: The speaker says that during a period of Lean 4 development, Leo was frustrated with users generally and particularly with mathematical users.

“And while he was working on Lean 4 he kind of holed off and, you know, he kind of needed his distance. Um, and you know, e- every once in a while I would send him a, an email and get a quick response, but it was clear that he, he wanted some distance.”

Claim: The speaker says Leo kept his distance from others while working on Lean 4, although he occasionally replied quickly to the speaker’s emails.

“Uh, and that was hard. You know, I, I missed him because he's, he's a very good friend and, uh, uh, um, and I, I missed just kind of constantly being able to bounce off ideas and so on.”

Claim: The speaker says he missed Leo and their regular exchanges of ideas while Leo was distant.

“Um, and so, um, so Leo arranged the dinner. It was, uh, o- other people were in town for the conference, he decided to take the opportunity to bring together advisors for the Lean-focused research org.”

Claim: The speaker says Leo arranged a dinner during the conference to bring together advisors to the Lean-focused research organization who were in town.

“So it wasn't, it wasn't a birthday dinner, it was, it was really just bringing together people, uh, you know, interested in Lean and, and, uh, uh, supporting Lean. But, um, but I told him that my birthday was that week and he decided to make it coincide with my birthday.”

Claim: The speaker says Leo arranged the Lean-related dinner for another purpose and then made it coincide with the speaker’s birthday after learning the birthday was that week.

“Um, but, um, but what I really was looking forward to was not, not, not that dinner but the next day. Um, he just took an a- afternoon off from work, I took an afternoon off from the conference, and we just met at, uh, um, uh, at, uh, Pike's Place, uh, and we just k- kind of just walked and just walked and walked.”

Claim: The speaker says he and Leo spent the following afternoon walking together at Pike Place.

“Um, and yeah, it was, it was just, I don't know, it was just, it was great, great talking to him again. Um, you know, we, we talked about Lean but we talked about things that were not Lean.”

Claim: The speaker says he and Leo enjoyed reconnecting and discussed both Lean and topics unrelated to Lean.

“Um, um, I mean, for both of us it's been, I mean, the last several years has been surreal. I mean, we c- we just remember the early days of Lean. You know, I, yeah, again, I can remember when it was just me and some students, and I, I remember my time visiting Leo at Microsoft and working on the project.”

Claim: The speaker recalls that Lean began with him and some students and that he visited Leo at Microsoft to work on the project.

“And so looking, looking back on all that it, it almost seems surreal. I mean, it, it, it seems d- very surreal, you know, how far we've come.”

Claim: The speaker says Lean’s progress from its early days to the present seems surreal in retrospect.

“Now, Kevin Hartner really brought this story to life. He spent, I think, years researching this story, speaking with all of these guys, so I highly recommend you read Kevin's book.”

Claim: The speaker says Kevin Hartnett spent years researching the Lean story and interviewing people involved.