Mathematicians have thought that five long-standing conjectures in graph theory might be true but they have not been able to prove them:

Wagner programmed a neural network to create random examples and use these measures to assess their suitability as a counterexample. The AI discarded the worst scoring ones and then replaced them with more random examples before starting again. In dozens of cases the AI was unable to find an example that disproved the theory, but in five cases it landed on a solution which showed that the conjecture must be false.

Matthew Sparkes, “An AI has disproved five mathematical conjectures with no human help” at New Scientist (May 20, 2021 A subscription is required to read the whole article.)

On Adam Zsolt Wagner’s five-year-old laptop, it took between a couple of hours and a couple of days. Here’s the catch:

While the AI has succeeded in disproving conjectures, proving them is much harder. To disprove an idea requires creating and testing a vast amount of potential solutions to see if any contradict the conjecture, a mechanistic task that can be automated, but a proof is a creative work that requires insightful leaps and involves stringing together many logical steps.

Matthew Sparkes, “An AI has disproved five mathematical conjectures with no human help” at New Scientist (May 20, 2021 A subscription is required to read the article but the paper on which it is based is open access.)

That makes sense if we consider that a single counterexample disproves a theory in mathematics; the theory, as stated, must be applicable to all numbers of a specified type. Coming up with a proof from nothing requires creativity, which isn’t what computers do.

Eric Holloway took the opportunity to tell us, by way of illustration, about a pig who solved math problems:

I once had a marvelous pig. I called him Marvin the Marvelous. He could solve advanced mathematical problems all by himself. First, I would pose the question on a large board so the pig could read it. Then I would label 8 bins with a set of possible answers, only one of which was right. In the bin with the right answer, I’d fill it full of the tastiest pig slop on earth.

Without fail, every single time, Marvin the Marvelous would choose the correct answer, no matter how difficult the problem that was posed. Marvin’s amazing ability won great fame for both him and myself — because I’d raised the clever pig. But, I was always sure to let everyone know that it was really all Marvin’s work; I was merely along for the ride.

Mathematicians have discovered their own Marvin the Marvelous in a new AI algorithm that can disprove mathematical conjectures all by itself. All the mathematician needs to do is reward the AI’s guesses based on how close the guess is to a disproof and then leave the little guy to its own devices. I think we will be seeing more of this ingenious little algorithm, mark my word.

You may also wish to read: Could Chaitin’s Number prove Goldbach’s Conjecture at last? Chaitin notes that the problem grows exponentially and the calculations get quite horrendous. Gregory Chaitin acknowledges that the Omega number doesn’t solve all problems but the Omega prime or Omega double prime might help.