1977: The first mathematical theorem to be proven by a computer: No more than four colors are required to color the regions of any given regional map so that no two adjacent regions have the same color.

2005: Following disputes among mathematicians about the validity of computerized proofs, development of Coq – an interactive theorem prover,.

To the MNS presentation