Is mathematics about to enter the conservatory?
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. ...