Comment by auggierose

There is nothing wrong with learning from CS research, but mathematicians are just better at thinking about mathematics than computer scientists are. Would you think in types if you didn't have to do it on a computer in a system designed by computer scientists? No way. Would you think in ZFC? Not really, either. We are now in a moment that might decide for the foreseeable future how we think about math, and we better get it right.