Hacker News Reader

Your comment inspired an interesting (to me at least) thought. I'm imagining a world where mathematics becomes too advanced for even the brightest human being, but progress is preserved by proof-generating programs running in data centers. The data centers churn out exabytes of mathematical proofs, and humanity employs an army of what are effectively philologists/semioticians to dissect, mine, and excavate these proofs for meaning.

Ted Chiang has a (very) short story exploring this idea, with metahumans replacing data centers here: https://www.nature.com/articles/35014679

Thank you for that link. A very interesting story, with surprising philosophical depth given its brevity.

And when your surpassing creations find the answers you asked for, you can’t understand their analysis and you can’t verify their answers. You have to take their word on faith—Or you use information theory to flatten it for you, to squash the tesseract into two dimensions and the Klein bottle into three, to simplify reality and pray to whatever Gods survived the millennium that your honorable twisting of the truth hasn’t ruptured any of its load-bearing pylons. You hire people like me; the crossbred progeny of profilers and proof assistants and information theorists…

In formal settings you’d call me Synthesist.

—Peter Watts, Blindsight (2006)

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

True, and important. However, I suppose it could be argued that if the only results AlphaProof could obtain were long and unreadable proof(s) with no discernible structure, it might suggest something about the epistemic assumptions we tend to make about Occam's Razor and the (so-called) beauty and parsimony.

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 epistemic assumptions we tend to make about Occam's Razor and the (so-called) beauty and parsimony.

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.

A long unreadable proof would not mean a small proof doesn't exist.

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.

Maybe that'll be time to bring in AlphaProofReductor or AlphaProofCanonizer. I'm finding this worry a bit strange. I'm guessing tools evolve together depending on need, so as long as humans want to know 'why and how' there'll be some effort in reduction?

There probably are not.

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.

If AlphaProof generated a long and unreadable proof with no discernible structure, it would not be such a large contribution to mathematics as if a human figured out "why" and wrote it in a way other humans could understand.

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.

Gödel's incompleteness theorem doesn't fill me with the same confidence as you that "a true theorem should have a useful explanation".

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

Yeah, it certainly isn't true that a true theorem should have a useful explanation. I only have my human intuition to go on, but I bet the Riemann hypothesis would not be like the four-color problem. Graph-type problems just seem to lend themselves to exhaustively checking a zillion cases in a boring way, whereas in fields like number theory or analysis that sort of proof hardly ever seems to exist.

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....

We already have machine-assisted proofs which are structured by people but executed by machines. AlphaProof would be that but structured by machine. As with the machine-assisted proofs, there's value in knowing and building upon the result even if the methods themselves can't be adapted for other use.

> If AlphaProof generated a long and unreadable proof...

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!

We have automated proof checkers like CoQ. A proof machine would be designed to output proofs in a syntax that could be mechanically checked by an existing verifier.