My first thought when I read this title was that there should be a site like Hoogle for mathematical proofs, where one could search by type signature for existing proofs. I'm not sure if people often think of proofs in terms of their type signature, but by Curry-Howard it would be doable.
This is a complicated problem. I know some Coq developers are trying to build a search tool, but the problem is there are many ways to state a theorem and you want to not only find statements that exactly correspond to your request, but also those that are convertible to it. And there it gets ugly.
May be tangential, but take a look at the Mizar project [1]. It has a huge repository of around 50k machine verified non-trivial theorems in human readable syntax (e.g. Gödel's completeness theorem for first-order logic).
Also check out the journal Formalized Mathematics [2]. The idea is that every major new theorem in a paper has a machine verified proof attached.
I completely agree about the interconnectedness of different branches of mathematics and think it is difficult to visualize and intuit because we don't yet have the language.
My guess: Eventually, as we begin to understand mathematics better, we will elucidate the underlying properties of theorems and there will be better "tagging"; the underlying language must also change. This will not happen for a minimum of 30+ years as new advances must be made and institutional faculty will object lest their life be rendered irrelevant.
Category theory by Tom LaGatta[1] is also a nice introduction. He suggests taking a look at the nLab website[2], a wiki of Maths and Physics from the categorical point of view.
The way this is presented in the blog post is as if this is a really insightful but now under-appreciated gem of mathematics.
But all that description is saying is, when a 2D shape is made by rotation, its area is the multiple of the 1D generator and the 1D path it takes? You don't say!
And then volumes! when a 3D volume is made, its a 2D shape going through 1D path ...wow.
Forgive me if I am not impressed. This is not an unknown theorem but a trivial mathematical fact that one learns somewhere around Grade 7 in school. Of course, Pappus deserves credit for discovering in 300 AD, and the paper by the Goodmans is nice to have a general formal proof of. But even that paper concedes that they are simply proving a general proof for completeness.
But it isn't that simple. The insight is in the importance of using the centroid of the shape and the path it traces. It can't be any other point for the simpler form to work.
That's the cleverness, and the reason the centroid has that property is interesting enough, and not immediately obvious. But by understanding why it works, we can see we can apply it for much more general cases than surfaces of revolution, which is usually the only treatment the theorem gets out there. The purpose of the post was to illustrate the generality of the theorem.
The centroid is the average of all points of a shape. It is therefore the only point that contains information about the entire shape. Any other point doesn't. Naturally, since paths are distances and can also be averaged in the same way, it is actually quite obvious that the path travelled by the centroid of a shape is also the average path of all the points on that shape. In fact, it directly follows from the definition of a centroid consider that the path of a shape is the addition of one more dimensional coordinate to each of the points on that shape.
Sorry,I still do not see what makes this so special.
