Book Review: The Proof in the Code

In just a few years artificial intelligence tools have progressed from solving formulaic math contest problems to generating novel proofs of long-standing open conjectures. The way math is done is changing, and more change is coming. Anyone interested in math should be paying attention to the unfolding story of AI-assisted mathematics, and this is especially true for math teachers, whose current students will enter a world where “doing math” is likely to mean something dramatically different than it does today.

Kevin Hartnett’s “The Proof in the Code” is an excellent entry point into that world. Hartnett tells the origin story of Lean, a mathematical formalization tool playing part in the AI-assisted mathematics revolution. Originally developed by researchers at Microsoft to debug code, Lean is now being used in synthesis with generative AI tools like large language models to debug mathematical proofs. The results have been astonishing.

“The Proof in the Code” is the story of the people and the ideas behind Lean, but it’s also the story about how we’ve arrived at a place where one of the world’s leading mathematicians recently felt obligated to say “It’s not necessarily the end of mathematics”. Hartnett’s book is a satisfying read for anyone interested in science and technology, but for teachers and learners of math, “The Proof in the Code” isn’t just a compelling tale of recent theoretical advances. It’s part of the backstory of the next chapter of human mathematics.

Related Posts

Connecting Classroom Math to AI — NCTM New Orleans

I’m excited to be presenting Connecting Classroom Math to AI at the upcoming NCTM meeting in New Orleans. I think math teachers are uniquely positioned to help students develop healthy, productive, and realistic attitudes toward artificial intelligence tools by making sure that these tools are understood as applications of mathematics.

Here’s the session description:

Artificial Intelligence tools are everywhere and are likely to affect our lives in profound and lasting ways. To help prepare our students for an AI-driven future, let’s make sure they recognize that these tools are fundamentally applications of mathematics. In this session, we’ll see how topics from the MS/HS curriculum lead directly to the math that underlies technologies like LLMs, chatbots, and more, and we’ll discuss how to make these connections clear and compelling for our students.

You can find all the session details here.

Related Posts

AI-Generated Letters of Recommendation

I write around 30 recommendation letters a year. These are mostly for students applying to college, but increasingly I’m asked to write recs for competitive summer programs, private schools, scholarships, even internships. It’s a lot of work. I estimate that I spend around 100 hours a year on it

And it’s uncompensated work. Almost all of these hours come directly from my personal time, which colleges treat as a free resource. There is nothing to stop them from making me fill out one more form, complete one more ranking, respond to one more school-specific prompt. I often feel like collateral damage in the school admissions arms race.

Some teachers simply refuse to do it. I have come to empathize with that position, but ultimately these recommendations are important to my students, so I put in the time and effort, even though the process is frustrating.

What’s most frustrating is that I’m not sure all this effort makes any difference. Do letters of recommendation really matter in college applications? I find it hard to believe they do. Last year 30,000 students applied to MIT. Who reads those 60,000 letters of recommendation?

I’ve long assumed that these letters just get passed through some kind of sentiment analysis software, where a large language model produces a score, appends it to the student’s profile, and the admissions process grinds on, one automated step at a time. I even recently speculated that colleges were feeding my letters to LLMs without my consent. What’s to stop them?

So when I logged into Naviance, the now-universal portal for college admissions, I shouldn’t have been surprised to see a new feature under the “Letters of Recommendation” tab: a compose-with-AI button.

But I was surprised. Isn’t this an admission that letters of recommendation aren’t that important? If colleges will accept an algorithmically-generated, averaged-out narrative as a substitute for whatever I might have said, how could they possibly value what have I say? Why shouldn’t I just click “Compose”, fill in a couple of blanks, and reclaim my time?

I guess there’s a part of me that still believes a good letter of recommendation can have an impact. Maybe that’s naïve, but if it’s true, then anything less than my full effort would put my students at a disadvantage. I respect them too much to do that, even if the process doesn’t respect me.

For now, I’ll hope that my carefully considered letters will give my students an edge in a world of AI-powered chatbots processing AI-generated recommendations. But I’ll be watching this AI-powered arms race closely.

Related Posts

Good AI, Bad AI

At the start of the school year I asked my students to let me know how they are using AI in my courses. I’ve seen some Good AI, and some Bad AI.

Good AI

I make mathematical computing a part of my year-long Linear Algebra course. The varying levels of computer programming experience among my students makes this a challenge: some could intern at Google and some can’t remember how a for loop works. AI Coding Assistants, used appropriately, provide invaluable support for students with limited experience. If they can’t successfully write a program to add two rows of a matrix together, they can have the Coding Assistant do it, check to see if it works, and then review the code themselves and try to learn something. Good AI! Here, “appropriate use” means making an honest effort to complete the challenge yourself first: This builds context for learning from whatever code the AI produces, and it also better positions the student to evaluate whether or not the code actually does what they asked it to do.

Bad AI

At the beginning of my Calculus course I ask students to write about a “mathematical observation” they’ve had. I am intentionally vague about what a “mathematical observation” is. Some students write about analyzing their commute to school, some about optimizing a video game strategy, some about a number theory course they took in a summer program. One goal of the assignment is to learn about my students as individuals and as mathematicians, so knowing what they think constitutes a “mathematical observation” tells me something about them.

One student began their paper by disclosing that they first asked ChatGPT to define “Mathematical Observation” for them. This immediately struck me as Bad AI. Thinking about what constitutes a mathematical observation was the point. Not only did the student ask an AI tool to do their thinking for them, but doing so undermined the very purpose of the assignment: Instead of learning what the student thinks as an individual, I got some averaged-out sentiment from a non-random group of authors.

For the record, the student did write a lovely and thoughtful mathematical observation, but afterwards we had a good conversation about the role of AI tools. “Don’t use AI to do your thinking for you,” I said, which seems like a good place to start in navigating this new landscape.

ChatGPT in Geometry Class

I gave my geometry students some ChatGPT-generated “proofs” this week to review. There were several examples, each designed to illustrate a different point. One was a “proof” that the diagonals of a rectangle are congruent, which contained several errors. I was proud that several students immediately identified how dangerous it was: “It sounds like it is correct, until you look more closely at it.”

Originally posted on Mastodon.

Follow

Get every new post delivered to your Inbox

Join other followers: