Of course, it is possible that clever users could tease useful information out of the black box truth oracle. Perhaps by modifying the statement of the conjecture and checking each modification, they could discover some parts of the structure of the problem, which would help inspire a useful proof. Furthermore, it would be helpful to never again waste time trying to prove a false conjecture.

In formal settings you’d call me Synthesist.

—Peter Watts, Blindsight (2006)

[1]: https://www.rifters.com/real/Blindsight.htm

On that angle, it could be further argued that humans are biased towards 'readable' proofs and that there are many undiscovered 'unreadable' proofs that we simply have no way of obtaining without automation of some kind.

Anyway I assume there are volumes already written on this subject...

The vast majority of ways to write a program are unreadable messes. The shortest way to write a program is sometimes an unreadable mess, mainly when it's been code golfed. The longest ways to write a program are always unreadable. Proofs work the same way - and if Alpha Go selects randomly from all of the ways to write a reasonable-length proof, it is virtually guaranteed to pick an unreadable one.

I feel like a unreadable proof would be useful to simply know something is true while a small proof would be more useful to perhaps gain some sort of insight.

A successful AlphaProof would be trained to favor shorter proofs. It would be fast enough to prove RH myriad different ways, and not be finished until its proof cannot be shortened any more, just as AlphaGo isn't finished until no version of it can beat it.

Whether humans could understand the shortest possible proof is another question. It might take generations of study just to understand its outline, and many more to extract all the lemmas implied.

Or, it might turn out to be a trivial trick, and not reveal anything new and substantial.

Maybe not directly. But if AlphaProof managed to prove the Riemann hypothesis, I bet it wouldn't be long before human mathematicians had managed to decipher the proof and explain it in a way that other mathematicians found useful. It's just a lot easier to re-explain something that other people have already proved, rather than proving it yourself.

In fact, looking at chess engines tells us that sometimes (though not always) brute-force calculation of many possibilities gives us better moves. In the same way some true statements might just be an exhaustive calculation.

Perhaps the four color theorem is the most famous example of a proof that has lacked (still lacks) a lot of useful lemmas in relation to its length: https://en.wikipedia.org/wiki/Four_color_theorem

I hope we do get some famous theorems proved by computers so that we can see whether it's enlightening to humans. I am quite curious whether my intuition is correct and it is a shame to think I might never know....

Then how would anyone be sure it isn't wrong?

It was great that while Goldston and Yıldırım were wrong, their work proved to be useful. A lot of people are glad that Riemann (and Fermat) didn't their problems!

I don't think so, but I think the trick will be how to score a new mathematical relationship as "interesting". Basically, a fitness metric. With Chess, you have the obvious win/loss metric, and also number of turns and possibly time. With math, how do you quantify the level of interestingness between 2+2=4 and p=np?

This isn't a snarky question, by the way. I'm genuinely interested in how this might be done.

For example, an automated theorem prover can easily prove many statements of the form "A or not-A or (any long statement)". Those are all uninteresting tautologies that should be discarded.

It's interesting to theorize about improving these heuristics with AI methods, there is some work along these lines like ENIGMA-NG.

And if you have a prover that can answer that question, you don't need to train a neural network to give you the answer.

Proving maths demands 100% precision and recall, at which point employing ML doesn't make sense - the point of ML is (horribly simplified) stochastic reasoning, not finding truths.

Another problem is that a lot of proofs starts by exploration. For example, certain bounds for functions or convergence rates are proved without knowing what will be the end result.

Of all the problems that ML could be applied to, I find mathematical proofs one of the least promising. One, I don't see enough similarity between proofs that would allow any algorithm to learn useful patterns; and two, I don't think most mathematicians would trust a proof that cannot be understood (even if the output is a set of steps for a formal system, I imagine translating that to human language could be quite difficult).

My argument is that it all happens through the application of operators and abstractions i.e. other numbers going through Gödel's approach.

In the same vein, we "should" in theory produce something similar. In RL, we have agents that learn to 'imagine' goals and then achieve them. Given the correct representation of such 'dreams' the models 'could' in theory learn to achieve such auxiliary theorems.

And even then recall/precision need to be 100%. And even if you could achieve that, you still end up with something that... generates statements that are provably true. Mild yay.

But that's not the problem. We can generate plenty of those. You want to identify the ones that actually advance the state of knowledge usefully.

There is the "prove this conjecture I have" part, which I think will be taken over by machines rather soon (say, within my lifetime). I cannot imagine there is something extra-ordinarily hard that mathematicians do, that is somehow not captured by how a Go player approaches the game.

There is also the "come up with an interesting conjecture" part, which I think is a lot harder. It is extra-ordinarily hard to specify what exactly makes some conjectures more interesting than others. So I reckon this part of math will be much harder to automate in the long run. It will probably require a lot of cross-contamination from AI that manage to write interesting books for example.

It's not "extraordinarily hard" but the issue is that math does not have a well-defined search space. A lot of times, proving statements requires quite a lot of intermediate results, additional tools and definitions... There is more creativity in math proofs that people think, and I don't think ML algorithms will be able to reproduce that. At most I see specific algorithms for limited purposes.

‘Proofs’ in human parlance are those which we believe to be interesting or aesthetic or useful.

I don't know if there was much work done on this idea beyond Gödel's proof, but I think it's a really neat idea that gives a way to manipulate mathematical proofs as objects and create new ones from a very high level view.

you could try something like this for statements in a formal axiomatic system, but know that you're running up against things like the halting problem / entscheidungsproblem / godel incompleteness. so it may be possible to train a neural net to decide the veracity of a statement and do so more quickly than a human might, but you would inevitably be running up against things that are truly undecidable in nature. which is not like go or chess where although they are difficult, they are decidable.

My point is that even though some things have technical similarities, in practice they are very different challenges.

chess is in exp, the class of problems requiring exponential time to solve and exponential time to check. unlike p vs np we do know that exp \neq p.