Mr Honner

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.

Teaching Technology

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 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.

Appreciation Photography

Math Photo — Snow Array

A snow day snow array! I thought of punching out that one stubborn entry, but let it be in the spirit of wabi-sabi. It’s like the Great British Baking Show’s missing raspberry.

Geometry Numbers Teaching

Angle Sums and Pythagorean Triples

I’ve always found it cool that if you double the smaller acute angle in a 3-4-5 triangle you get the larger acute angle in a 7-24-25 right triangle. You can see this as a consequence of the double angle formula for sine. If $\alpha$ is the smaller acute angle in a 3-4-5 triangle, then

$\sin (2\alpha) = 2\sin\alpha\cos\alpha=2\frac{3}{5}\frac{4}{5}=\frac{24}{25}$

In fact, if the sine and cosine of an angle are both rational, then so will be the sine and cosine of twice that angle. This gives a way to turn Pythagorean triples into new Pythagorean triples!

For example, suppose $\alpha$ is an acute angle in a right triangle with $a^2 + b^2 = c^2$ . Then

$\sin 2\alpha = \frac{2ab}{c^2}$
$\cos 2 \alpha = \frac{a^2-b^2}{c^2}$

By the Pythagorean identity

$\left(\frac{2ab}{c^2} \right)^2 + \left(\frac{a^2-b^2}{c^2} \right)^2 = 1$

And so

$\left(2ab \right)^2 + \left(a^2-b^2 \right)^2 = \left(c^2\right)^2$

which of course also follows directly from algebra.

For example, using this process

$(3,4,5) \mapsto (7,24,25) \mapsto(336,527,625)$

Originally posted on Mastodon.

Resources Teaching

2025 — Year in Review

Here are some highlights from what has been another busy professional year.

In September I published a new series in the New York Times that turns Steven Strogatz’s wonderful “Math, Revealed” essays into teaching and learning resources. I got to write about favorite topics like taxicab geometry, triangular numbers, the golden ratio, and packing problems. Best of all, I got to collaborate directly with Strogatz himself! It was an honor to work with him, even if this doesn’t officially make my Erdős number four.

I’ve been thinking and writing about AI in education and math this year. I wrote about how students are using AI, how it is impacting the college admissions process, about experts calling AI-errors “sophisticated”, and how it’s affecting me as a book author. I’ve been through a few hype-bubbles in my time, and am generally skeptical by nature, but there’s no denying the impact these technologies will have in how we learn, teach, and even do math.

I’m wrapping up my 20th, and final, year as a Math for America Master Teacher, and I was proud to run one more workshop for teachers through MfA. “A One-Problem Tour of Statistics” was the story of what I learned by writing Painless Statistics, but also an homage to the kinds of math problems that you keep going back to. It was a fun and satisfying end to a string of nearly 30 workshops I’ve run in my time at MfA.

The applied mathematics and modeling program I run at my school had unprecedented success in 2025. We had a team win the NCTM Award in the 2024 High School Mathematical Contest in Modeling (HiMCM) and finish in the top ten worldwide in the 2025 International Mathematical Modeling Challenge (IMMC). Another team won the MAA Award in the 2025 MCM, finishing among the top of over 12,000 entries worldwide, nearly all of which were college teams! We also had a team earn an “Outstanding” designation — the highest honor — in the 2025 SCUDEM competition, a college-level differential equations modeling competition. I was very proud to be profiled on the COMAP website for “teaching, modeling, and mentoring at the highest level”!

This past summer I was invited to present to the Alliance for Decision Education on my work with student forecasting, after our students made impressive showings in two individual forecasting competitions in 2024 and 2025. I also appeared on MoMath’s QED and spoke with mathematician-in-residence David Reimann about math and math education.

It’s been a good year professionally, and I’m looking forward to more to look back on in 2026!

Book Review: The Proof in the Code

Connecting Classroom Math to AI — NCTM New Orleans

Math Photo — Snow Array

Angle Sums and Pythagorean Triples

2025 — Year in Review

Follow Mr Honner