Math

The same week that Claude finished formalizing the proof of Fermat’s Last Theorem in Lean, a paper landed in my inbox titled, The Spherical Hadwiger Theorem. The Spherical Hadwiger Conjecture1, which has been open since about 1974, describes a niche-but-important piece of integral-geometric machinery. I’m not going to get into the details of the conjecture here; if you are interested you can see a discussion in my previous post where the theorem (then still a conjecture2) greatly simplifies the proof of a little lemma of mine from grad school. ...

Drop a needle of length $L$ onto a hardwood floor with floorboards of width $W$. On average, the needle crosses $2L / \pi W$ lines between floorboards, a classic result of Buffon. But that $\pi$ in the formula means there’s a circle hiding somewhere. The trick to finding it? Bend the needle into a noodle. A single noodle, before being dropped Floor with ruled lines, with one noodle highlighted Drops K 0 Avg crossings (observed) — 2L / πW — Total turn Θ° 75° Segments N 4 Length L/W 2.0 Drops K 200 Reset Needle (Θ = 0°) π-circle From needle to noodle The usual approach to Buffon’s problem involves a double integral. Respectable, but this hides the circle at the heart of the solution, and frankly, I don’t love doing integrals. Instead, we’ll derive the result1 by going from a straight needle, to a curvy noodle, to a circle. All we need is some basic geometric reasoning and probability. ...

Note: This is an edited version of the original post. Thanks to Prof. Rolf Schnieder for alerting me that the Spherical Hadwiger conjecture remains open. Note 2 (2026-09-05): A recent preprint appears to resolve the Spherical Hadwiger Conjecture in the affirmative! I’m not going to edit the post again, but see this post for more discussion around how AI is affecting research mathematics. Sometime in late 2012 or early 2013, Joel Tropp, Martin Lotz, Dennis Amelunxen, and I were all discussing some integral-geometric problem or another, and the topic of projections of convex cones came up. One of us made the observation that taking the linear image of a subspace in general position yields one of two results: ...

With my first guitar, I also got my first guitar tuner, a device that I have mixed feelings about. I can’t tune my guitar without it, but the tuner exposes just how fickle the concept of being “in tune” really is. The author with his guitar, trying to look cool, circa 2021. There are many reasons that it’s hard to tune your guitar, from the weather to number theory.1 This post adds another reason to this already long list: ...