"I very much agree that mathematics is a human activity. But I also think that using a computer is a human activity."

Johan Commelin, director of mathlib