CS4FN Advent 2023 – Day 11: the proof of the pudding… mathematical proof

A mathematical proof and a maths puzzle (but no hard sums, promise).

Thank you to everyone who’s been reading our Advent Calendar and said nice things about it and shared it with others. If you’re new to our pages you can see all our previous posts at the end.

We’re doing a post every day from the 1 – 25 December, loosely connected (if we can manage it!) to the theme suggested by the picture on the CS4FN Christmas Computing Advent Calendar.

Today’s picture on the Advent Calendar door is a Christmas pudding. Thanks to the phrase “the proof of the pudding is in the eating” (which I think means you have to eat all the chocolate puddings to know if they’re any good) I have chosen to match this picture with one of the CS4FN articles from the archives that is all about PROOF. Sadly we don’t seem to have any articles about pudding.

People sometimes pour brandy on Christmas puddings and set fire to it but this one has been iced instead and is not a fire hazard. Image drawn and digitised by Jo Brodie.

1. Proof without words

by Paul Curzon, QMUL. This article was originally published on the CS4FN website.

Graphic news images often help sway public opinion. Images of famine in Africa led to LiveAid, a massive relief effort in 1985. Images from war zones of civilians can be disturbing enough that war leaders lose or gain political support as a result (depending on who did the bad stuff). Images can have far more power than words to argue a case … to persuade.

Mathematical proofs are just arguments intended to persuade too. They aim to leave no element of doubt that some fact is true, not for emotional reasons but by logic. Mathematicians use mathematical notation – special symbols used in precise ways – to represent things in their proofs. That’s just a way of making sure the arguments are precise, with no room for doubt. Sometimes that can make them seem arcane and difficult to follow, though that’s only until you’ve learnt the mathematical language being used.

Mathematical proofs don’t have to use words and symbols though. In fact people have been presenting proofs as pictures at least since the Ancient Greeks, and just as with news images a diagrammatic proof can be much more persuasive. Sometimes just by looking at a diagram the truth of a fact can become obvious.

For example, here is a mathematical ‘fact’ we might want to prove:

“The square of any number is equal to the sum of consecutive odd numbers.”

That may sound a bit hairy. To get even hairier (if you aren’t a mathematician), we can write this precisely in mathematical notation as:

n2 = 1 + 3 + 5 + …+ (2n – 1)

Don’t worry about the notation though. Just look at the picture below. It shows what we mean by the fact and should persuade you it’s true.

The square of a number can be drawn as a picture of dots in a square. In other words one way to work out 102, say, is to create a square of dots with sides of length 10 and then count the dots. That’s why it’s called ‘squaring’!

A graphical representation of squaring numbers. Image by Paul Curzon / CS4FN.

One way to draw the dots to make up a square is as follows. First draw one dot in the corner, then draw three dots in an L-shape round it, then draw 5 dots in an L-shape round that…and keep going. Add a new L-shape (including the first dot) 10 times, say, once for each dot along the side, and you get a square of size 10 with 100 dots altogether. Notice that at every step you still have a square, though. Also notice that each L-shape is 2 bigger than the one before. That’s because you can make it by adding one dot on the end of each arm of the last L-shape.

That means the number of dots in a square can be calculated by adding a sequence of odd numbers, one for each L-shape added: 1 + 3 + 5 + … As you add L-shapes you work up through squares of all sizes, so all squares can be made by adding odd numbers in this way.

We’ve just explained it in words, but actually it’s all in the picture, so it’s possible to see without needing the words at all.

At least it may be possible for a person to see perhaps, but what about a computer? Could a computer ‘see’ a proof from a diagram? Computers are now very good at helping humans do logical proof using mathematical notation – after all they work themselves by pushing ‘symbols’ about and following rules blindly, which is all logical proof is. Seeing a proof in a diagram is different altogether though…or is it?

Mateja Jamnik, of the University of Cambridge has been tackling this problem. In fact her system, DIAMOND, can already check diagrammatic proofs created by a person to see if they really do convince. With DIAMOND you could, for example, take a series of L shape pictures like ours above and build them up step-by-step giving squares of different sizes. The system can then pull out the structure of this step-by-step proof and from that automatically obtain the equation that it proves.

DIAMOND needs a person to develop a diagrammatic proof for it to check. In the future, if Mateja has her way, the computers will be devising new diagrammatic proofs themselves that then convince we humans.

2. Today’s puzzle – Logic and Proof FUNdamentals

(This text, by Paul Curzon, was originally published over several pages at the CS4FN website)

It is often said that being good at Maths is important for Computer Scientists. So what’s the link? Well a lot of the more obviously fun sides of maths are actually computer science too, like how to do puzzles such as Rubik’s Cubes, puzzles about weird and wonderful characters crossing rivers, how to win at strategy games, and doing Sudoku. The Maths you do in solving a Sudoku is the same kind of reasoning as that behind getting computer programs to work.

It is not so much the actual Maths you learn at school that is important. It is more that a similar way of thinking is important: logical reasoning. Doing Maths at school is one good way to start to learn how to think that way. So if you are good at Maths you will probably be good at Computer Science, though (using a bit of logical reasoning) that doesn’t mean the opposite follows of course.

Kakuro, Logic and Computer Science

To be a good computer scientist you have to enjoy problem solving. That is what it’s all about: working out the best way to do things. You also have to be able to think in a logical way: be a bit of a Vulcan. But what does that mean? It just means being able to think precisely, extracting all the knowledge possible from a situation just by pure reasoning. It’s about being able to say what is definitely the case given what is already known…and it’s fun to do. That’s why there is a Sudoku craze going on as I write. Sudoku are just pure logical thinking puzzles. Personally I like Kakuro better. They are similar to Sudoku, but with a crossword format.

What is a Kakuro?

A Kakuro is a crossword-like grid, but where each square has to be filled in with a digit from 1-9 not a letter. Each horizontal or vertical block of digits must add up to the number given to the left or above, respectively. All the digits in each such block must be different. That part is similar to Sudoku, though unlike Sudoku, numbers can be repeated on a line as long as they are in different blocks. Also, unlike Sudoku, you aren’t given any starting numbers, just a blank grid.

Where does logic come into it? Take the following fragment:

There is a horizontal block of two cells that must add up to 16. Ways that could be done using digits 1-9 are 9+7, 8+8 or 7+9. But it can’t be 8+8 as that needs two 8s in a block which is not allowed so we are left with just two possibilities: 9+7 or 7+9. Now look at the vertical blocks. One of them consists of two cells that add up to 17. That can only be 9+8 or 8+9. That doesn’t seem to have got us very far as we still don’t know any numbers for sure. But now think about the top corner. We know from across that it is definitely 9 or 7 and from down that it is definitely 9 or 8. That means it must be 9 as that is the only way to satisfy both restrictions.

Kakuro image above by Paul Curzon / CS4FN.

A Kakuro for you to try

Here is a full Kakuro to try. The answer will be in tomorrow’s post.

Being able to think logically is important because computer programming is about coming up with precise solutions that even a computer can follow. To do that you have to make sure all the possibilities have been covered. Reasoning very much like in a Kakuro is needed to convince yourself and others that a program does do what it is supposed to.

Kakuro puzzle image above by Paul Curzon / CS4FN.


Advert for our Advent calendar
Click the tree to visit our CS4FN Christmas Computing Advent Calendar

EPSRC supports this blog through research grant EP/W033615/1.

Lego computer science: pixel pictures

by Paul Curzon, Queen Mary University of London

It is now after Christmas. You are stuffed full of turkey, and the floor is covered with lego. It must be time to get back to having some computer science fun, but could the lego help? As we will see you can explore digital images, cryptography, steganography, data compression, models of computing, machine learning and more with lego (and all without getting an expensive robot set which is the more obvious way to learn computer science with lego though you do need lots of lego). Actually you could also do it all with other things that were in your stocking like a bead necklace making set and probably with all that chocolate, too.

First we are going to look at understanding digital images using lego (or beads or …)

Raster images

Digital images come in two types: raster (or bitmap) images and vector images. They are different kinds of image representation. Lego is good for experimenting with the former through pixel puzzles. The idea is to make mosaic-like pictures out of a grid of small coloured lego. Lego have recently introduced a whole line of sets called Lego Art should you want to buy rather amazing versions of this idea, and you can buy an “Art Project” set that gives you all the bits you need to make your own raster images. You can (in theory at least) make it from bits and pieces of normal lego too. You do need quite a lot though.

Raster images are the basic kind of digital image as used by digital cameras. A digital image is split into a regular grid of small squares, called pixels. Each pixel is a different colour.

To do it yourself with normal lego you need, for starters, to collect lots of the small circle or square pieces of different colours. You then need a base to put them on. Either use a flat plate piece if you have one or make a square base of lego pieces that is 16 by 16. Then, filling the base completely with coloured pieces to make a mosaic-like picture. That is all a digital image really is at heart. Each piece of lego is a pixel. Computer images just have very tiny pieces, so tiny that they all merge together.

Here is one of our designs of a ladybird.

A ladybird image made of pixels
A pixel image of a ladybird
Image by Paul Curzon

The more small squares you have to make the picture, the higher the resolution of the image With only 16 x 16 pixels we have a low resolution image. If you only have enough lego for an 8×8 picture then you have lower resolution images. If you are lucky enough to have a vast supply of lego then you will be able to make higher resolution, so more accurate looking images.

Lego-by-numbers

Computers do not actually store colours (or lego for that matter). Everything is just numbers. So the image is stored in the computer as a grid of numbers. It is only when the image is displayed it is converted to actual colours. How does that work. Well you first of all need a key that maps colours to numbers: 0 for black, 1 for red and so on. The number of colours you have is called the colour depth – the more numbers and linked colours in your key, the higher the colour depth. So the more different coloured lego pieces you were able to collect the larger your colour depth can be. Then you write the numbers out on squared paper with each number corresponding to the colour at that point in your picture. Below is a version for our ladybird…

A grid of numbers representing colours
The number version of our ladybird picture
Image by Paul Curzon

Now if you know this is a 16×16 picture then you can write it out (so store it) as just a list of numbers, listed one row after another instead: [5,5,4,4,…5,5,0,4,…4,4,7,2] rather than bothering with squared paper. To be really clear you could even make the first two numbers the size of the grid: [16,16,5,5,4,4,…5,5,0,4,…4,4,7,2]

That along with the key is enough to recreate the picture which has to be either agreed in advance or sent as part of the list of numbers.

You can store that list of numbers and then rebuild the picture anytime you wish. That is all computers are doing when they store images where the file storing the numbers is called an image file.

A computer display (or camera display or digital tv for that matter) is just doing the equivalent of building a lego picture from the list of numbers every time it displays an image, or changes an old one for something new. Computers are very fast at doing this and the speed they do so is called the frame rate – how many new pictures or frames they can show every second. If a computer has a frame rate of 50 frames per second, then it as though it can do the equivalent of make a new lego image from scratch 50 times every second! Of course it is a bit easier for a computer as it is just sending instructions to a display to change the colour shown in each pixels position rather than actually putting coloured lego bricks in place.

Sharing Images

Better still you can give that list of numbers to a friend and they will be able to rebuild the picture from their own lego (assuming they have enough lego of the right colours of course). Having shared your list of numbers, you have just done the equivalent of sending an image over the internet from one computer to another. That is all that is happening when images are shared, one computer sends the list of numbers to another computer, allowing it to recreate a copy of the original. You of course still have your original, so have not given up any lego.

So lego can help you understand simple raster computer images, but there is lots more you can learn about computer science with simple lego bricks as we will see…


More on …


This post was funded by UKRI, through grant EP/K040251/2 held by Professor Ursula Martin, and forms part of a broader project on the development and impact of computing.

Lego Computer Science

Part of a series featuring featuring pixel puzzles,
compression algorithms, number representation,
gray code, binary and computation.

QMUL CS4FN EPSrC logos