[math-fun] strip mining to find nice provably irrational numbers?