Month: March 2000

After discovering that a Ralph Rowlett was in charge of the Royal Mint in 1540, Peter Rowlett runs the genealogy calculations to find out if he could be related.

In 1540, Henry VIII’s coins were made in the Tower of London. One of the Masters of the Mint was Ralph Rowlett, a goldsmith from St Albans with six children. I wondered: am I descended from Ralph? My Rowlett ancestors were Sheffield steelworkers, ever since my three-times great grandfather moved north in search of work. The trail goes cold in a line of Bedfordshire farm labourers in the 18th century, offering no evidence of a direct relationship.

My instincts as a mathematician led me to investigate this in a more mathematical way. I have two parents. They each have two parents, so I have four grandparents. So, I have eight great-grandparents, 16 great-great-grandparents and 2ⁿ ancestors n generations ago. This exponential growth doubles each generation and takes 20 generations to reach a million ancestors.

Ralph lived 20 to 25 generations before me in an England of about 2 million people. The exponential growth argument says I have several million ancestors in his generation, so, because we run out of people otherwise, he is one of them.

But this model is based on the assumption that everyone is equally likely to reproduce with anyone else. In reality, especially at certain points in history, people were likely to reproduce with someone from the same geographic area and demographic group as themselves.

But I am not sure this makes a huge difference here because we are dealing with something called a small-world network: most people are in highly clustered groups, tending to pair up with nearby people, but a small number are connected over greater distances. An illegitimate child of a nobleman would have a different social class to their father. A migrant seeking work could reproduce in a different geographic area.

We don’t need many of these more remote connections to allow a great amount of spread around the network. This is the origin of the six degrees of separation concept – that you can link two people through a surprisingly short chain of friend-of-a-friend relationships.

I ran a simulation with 15 towns of a thousand people, where everyone has only a 5 per cent chance of moving to another town to reproduce. It took about 20 generations for everyone to be descended from a specific person in the first generation. I ran the same simulation with 15,000 people living in one town, and the spread took about 18 generations. So the 15-town structure slowed the spread, but only slightly.

What does this mean for Ralph and me? There is a very good chance we are related, whether through Rowletts or another route. And if you have recent ancestors from England, there is a good chance you are too.

For more such insights, log into www.international-maths-challenge.com.

*Credit for article given to Peter Rowlett*

An artificial intelligence that can turn mathematical concepts written in English into a formal proving language for computers could make problems easier for other AIs to solve.

Maths can be difficult for a computer to understand

An artificial intelligence can translate maths problems written in plain English to formal code, making them easier for computers to solve in a crucial step towards building a machine capable of discovering new maths.

Computers have been used to verify mathematical proofs for some time, but they can only do it if the problems have been prepared in a specifically designed proving language, rather than for the mix of mathematical notation and written text used by mathematicians. This process, known as formalisation, can take years of work for just a single proof, so only a small fraction of mathematical knowledge has been formalised and then proved by a machine.

Yuhuai Wu at Google and his colleagues used a neural network called Codex created by AI research company OpenAI. It has been trained on large amounts of text and programming data from the web and can be used by programmers to generate workable code.

Proving languages share similarities with programming languages, so the team decided to see if Codex could formalise a bank of 12,500 secondary school maths competition problems. It was able to translate a quarter of all problems into a format that was compatible with a formal proof solver program called Isabelle. Many of the unsuccessful translations were the result of the system not understanding certain mathematical concepts, says Wu. “If you show the model with an example that explains that concept, the model can then quickly pick it up.”

To test the effectiveness of this auto-formalisation process, the team then applied Codex to a set of problems that had already been formalised by humans. Codex generated its own formal versions of these problems, and the team used another AI called MiniF2F to solve both versions.

The auto-formalised problems improved MiniF2F’s success rate from 29 per cent to 35 per cent, suggesting that Codex was better at formalising these problems than the humans were.

It is a modest improvement, but Wu says the team’s work is only a proof of concept. “If the goal is to train a machine that is capable of doing the same level of mathematics as the best humans, then auto-formalisation seems to be a very crucial path towards it,” says Wu.

Improving the success rate further would allow AIs to compete with human mathematicians, says team member Albert Jiang at the University of Cambridge. “If we get to 100 per cent, we will definitely be creating an artificial intelligence agent that’s able to win an International Maths Olympiad gold medal,” he says, referring to the top prize in a leading maths competition.

While the immediate goal is to improve the auto-formalisation models, and automated proving machines, there could be larger implications. Eventually, says Wu, the models could uncover areas of mathematics currently unknown to humans.

The capacity for reasoning in such a machine could also make it well-suited for verification tasks in a wide range of fields. “You can verify whether a piece of software is doing exactly what you asked it to do, or you can verify hardware chips, so it has applications in financial trading algorithms and hardware design,” says Jiang.

It is an exciting development for using machines to find new mathematics, says Yang-Hui He at the London Institute for Mathematical Sciences, but the real challenge will be in using the model on mathematical research, much of which is written in LaTeX, a typesetting system. “We only use LaTeX because it types nicely, but it’s a natural language in some sense, it has its own rules,” says He.

Users can define their own functions and symbols in LaTeX that might only be used in a single mathematical paper, which could be tricky for a neural network to tackle that has only been trained on the plain text, says He.

For more such insights, log into www.international-maths-challenge.com.

*Credit for article given to Alex Wilkins*