[math-fun] Shanks' 707 digits