Comment by CJefferson

In the future I feel one parallel to this is my research area, SAT solving.

People used to solve logic problems by hand, verify logic. Now you pile it into a computer. The problem has been around for a while, no-one fully ‘understands’ the proof of the four colour theorem as a big chunk is computer proved.

We are now just changing (admittedly greatly) what we can put in a box marked ‘checked by computer.