Machine-verified formal mathematical proofs
A departure from my usual topics, in remembrance of my college math classes (and with a nod to Mozilla folks working on related areas like automated testing and software verification): Via Eric Drexler via Emergent Chaos comes this interesting review paper on formal proofs in mathematics and software to verify them. As a dual math/physics major I was well acquainted with jokes about the lack of mathematical rigor on the part of physicists, who often engaged in rather slapdash simplifications in their drive to get formulas they could use to explain experimental data and make further predictions. However physicists who cut corners are ultimately saved by the fact that nature will check their work and let them know if they’ve made bonehead mistakes. ...