Tag Archives: Formal proof


Now available as eBook and paperback

What makes something sentient?  What does it take for an entity to be aware of its own existence and to want to interact with the world of its own accord?  Is it a gift from God or hard science?  Is it something fundamentally human or animal in nature or is it a simple technological principle based on brain size?  There are many models, of course.  But, if consciousness is simply a natural product of neural complexity then eventually, in theory, we might build something – a computer or a machine – that was actually big enough to wake up!

Oh, wait …!

The widespread ramblings, which have appeared on this blog over the years, now make a partial contribution to a novel.  (See http://www.lulu.com/spotlight/vicgrout)


Vic Grout’s Conscious is set a year or three into the future.  The ‘Internet of Everything’ is making the world a more connected place than ever before.  People’s lives are becoming increasingly automated.  But something odd is happening … ‘Things’ are beginning to misbehave and no-one can work out why.  What starts as an amusing inconvenience quickly becomes very serious indeed!

A ragged bunch of academics, scientists and philosophers are on the case – and may know the answer.  But now they have to convince people that their crazy explanation is true.  And that’s only the start.  Against a backdrop of a world suddenly beginning to fall apart, they’re in a race against time to get someone to do anything about it.  And not everyone is on their side!

Continue reading

Clear as Maths!

This post follows on (loosely) from a previous discussion on maths and computing and asks what it really means to ‘prove’ something in each discipline.

An apocryphal story has an Oxbridge maths don lecturing to a group of undergraduates … After some time completely filling a huge blackboard with heavy calculus – with accompanying commentary, he turns to the class and casually notes, “So then, it’s clear that …” (the exact claim isn’t important). As he turns to resume his chalk-work, a particularly bold student enquires, “Excuse me, Professor; but is that really ‘clear’?” The don steps back and surveys his work; studying the entire board from top-left to bottom-right, with numerous head and eye movements to-and-fro – even some pointing – to cross-check various parts with each other. After a full five minutes of silent contemplation, he turns back to the students, smiles, announces, “Yes!”, and carries on as before.

So who’s defining ‘clear’ here?

Continue reading

Maths and Programming Working Together

When the Four Colour Theorem (FCT) was finally ‘proved’ in 1976, it upset a lot of mathematicians.  It was the first significant mathematical concept to be proved with a good deal of help from a computer and, for many, that didn’t make it a real proof.  Although we’re largely (maybe not entirely) OK with it now, the objections at the time weren’t just theorists’ snobbery.  At the heart of it all were some fundamental questions about the role a computer could or should play in formal logic.

Essentially, the FCT says that the maximum number of different colours needed to colour a map, so that no bordering countries are the same colour, is four.  (Colours can touch at a point but not at an edge.)  It’s easy to show that five will always do the trick and, in fact, most normal maps only need three.  However, certain types of map certainly seemed to need four so was four always enough? Continue reading