During my time as an eager undergraduate mathematician, I鈥檇 often wonder what it would feel like to prove a truly new result and have my name immortalised in the mathematical history books. I thought that dream had died when I gave up maths to become a science writer, but Aron鈥檚 theorem is now a reality 鈥� and I鈥檝e got the certificate to prove it.
While most mathematical theorems result from weeks of hard work and possibly a few broken pencils, mine comes courtesy of , a company selling personalised theorems as novelty gifts for 拢15 a pop.
Advertisement
Its automated theorem-proving software can churn out a theoretically infinite number of theorems for customers wishing to join the ranks of Pythagoras and Fermat. 鈥淲e generate new theorems and let people name them after themselves, a friend, a loved one, or whoever they want to name it after,鈥� explains Flaminia Cavallo, managing director of TheoryMine, based in Edinburgh, UK.
You may think this is an elaborate scam, or that you鈥檒l just end up with an obscure equation copied from some long-forgotten textbook, but TheoryMine claims to have far more validity than superficially similar companies selling star names.
Isabelle knows
鈥淲e鈥檙e inventing totally novel theorems, and the tradition is you have the right to name these theorems,鈥� explains , professor of automated reasoning at the University of Edinburgh and another member of the TheoryMine team. 鈥淭here are 10 star companies out there, and none of them have any affiliation to the International Astronomical Union.鈥�
He鈥檚 got a point. Automated theorem proving is a well-respected mathematical field, used by manufacturers to guarantee that the algorithms in computer processors will work correctly. Bundy and his colleagues have worked in this area for a number of years, and Cavallo came up with the idea for TheoryMine during her final year of an undergraduate degree in artificial intelligence and mathematics at the University of Edinburgh, where she wrote a program to generate novel theorems for her dissertation.
From its library of mathematical knowledge, the program generates a set of mathematical axioms, then combines them in different ways to produce a series of conjectures. It then uses the library to discard a portion of these on the basis that there are already counter-examples, showing they can鈥檛 be true. Overly complex conjectures are also ignored. Then it applies a technique known as 鈥渞ippling鈥�, in which it tries out various sequences of logical statements until one of these sequences turns out to be a proof of the theorem.
Quantum implications
鈥淚t鈥檚 a clever idea,鈥� says , a computational logician at the University of Cambridge and the creator of Isabelle, a theorem prover that Cavallo鈥檚 program uses. He is more interested in the theory behind the new program though, adding that 鈥渟ome of the technology here is quite impressive, and I would hope that it finds other applications apart from selling certificates鈥�.
It may well do. , another TheoryMiner, is investigating the possibility of using the same techniques to elucidate the rules of algebra in quantum computing systems, which follow different mathematical rules to classical systems.
Don鈥檛 prepare your acceptance speech just yet though, as TheoryMine鈥檚 theorems are unlikely to break drastically new ground. 鈥淲e can鈥檛 say that we鈥檒l never do that, but having looked at the things that come out, they鈥檙e not typically things that are going to change the world,鈥� says Dixon.
If not revolutionary, your theorem will at least be unique, since the TheoryMine software ignores trivial variants of already proved theorems. And in case you鈥檙e wondering, Aron鈥檚 theorem, delivered as a pdf by email yesterday, says something about the order in which you can add a new variety of numbers.
The TheoryMine team explained the logic behind the theorem to me, but I鈥檓 not quite sure I fully understand it 鈥� a common criticism of machine-aided proofs.
Turning over proving responsibilities to a computer also means I haven鈥檛 really captured that exciting feeling of discovering something new. Mathematical proof is about more than just racing to the end result: it鈥檚 a creative process in its own right. Sorry, undergraduate-me. I don鈥檛 think we鈥檒l be joining the history books any time soon.
