Tao, Kontsevich & others on HLAI in Math — LessWrong