Revisiting examples of computer assisted mathematics

I'm in the middle of a finishing off some last things for a brand new course we're teaching at +Cardiff University starting in October. I plan on using my first lecture to explain to our new students how important computing/programming/coding is for modern mathematicians.

I will certainly be talking about the 4 colour theorem which states that any map can be coloured using 4 colours. I'll probably demo a bit of what +Sage Mathematical Software System can do. Here's a sage cell that will demo some of this (click evaluate and you should see the output, feel free to then play around with the code).

There I've written some very basic code to show a colouring of a graph on 9 vertices.

I expect that Students might find that interesting in particular if I show colourings for non planar graphs. For example here's another cell showing the procedure on complete graph on 9 vertices:

That is just a couple of 'qwerky' things that don't really go near the complexities of the proof of the 4 colour theorem.

I took to social media in the hope of asking for more examples of cool things that mathematicians use computers for. Here's a link to the blog post but without a doubt the most responses I got was on this G+ post.

You can see all the responses on that post but I thought I'd try to compile a list and quick description of some of the suggestions that caught my eye:

• This wiki was pointed out by +Kevin Clift which contains a large amount of great animations (like the one below) made by 'Keiff':

• Kevin also pointed out that +Luis Guzman had shared a link to this great article that does not only mention Hale's 'proof' of the Kepler conjecture but also discusses some of the negative sides of computer assisted proofs.
  
• On a similar note +Artem Kaznatcheev pointed out a great blog post of his. In this post Artem discuss the 4 color theorem and also points out 'the curse of computing':

'This is the curse of computing: giving up understanding for an easy verification.'

• +Joerg Fliege mentioned chess endgame tablebases which I think would be a cool thing to point out to students.
  
• +David Ketcheson, +Dima Pasechnik and others pointed out how computer algebra systems are more or less an everyday tool for mathematicians nowadays. When I'm finding my way through a new project I normally always have a sage terminal open to try out various algebraic relationships as I go...

There are a couple of other things that I'm not listing above (mainly because I don't know enough about them to be able to comment), but interestingly enough +Timothy Gowers posted the other day a link to a paper that he has co-authored entitled: 'A fully automatic problem solver with human-style output'. In that paper a new program is described able to produce human style proofs of theorems. A blog post that +Timothy Gowers put up a while back was actually an experiment for this paper.

I'm obviously missing a large amount of other stuff so please do let me know :)