Hacker News Reader

Comment by chongli | Hacker News Reader

Wow, what a weird coincidence. I just did this proof in graph theory yesterday!

Suppose, for a contradiction, that there are n people, each with a different number of friends. Since a person can't be friends with themselves, the numbers of friends is as follows:

0, 1, ..., n - 1

Then, the person with n - 1 friends has a friendship with everyone else in the group, including the person with 0 friends. But this is a contradiction! Thus there must be at least two people with the same number of friends.

View on HN

Lovely proof!

Proof by contradiction is so much simpler than constructive proofs.

The flip side is that you lost the ability to "program" a solution. And they are not always simpler. Good constructive proofs usually goes by "Look at this object, now back at me, now at this object, I'm on a boat, I do a little computation, I'm on a horse, I do a little reduction, and I end up with the result I want, Qed."

That is, they start by claiming that a given object has the property you want and then proceed to show that it is the case.

I'm not a constructivist by any stretch of the word, but knowing different kinds of proofs of the same object is often giving us insight which we wouldn't have otherwise.

Is that the same proof than the ~120 lines of code of the link?

If yes, proof assistants have to be improved on conciseness, imho

Yes, it's the same proof.

The difference is that in a proof assistant, you cannot gloss over a detail. So many of the lines establishes well-known facts which a mathematician has internalized in their brain.

You could store that in a library (and many proof assistants do!) but then the proof would probably be harder to follow for a first time reader.

The end goal of proof assistance are simpler proofs. Telling the system system something like: "Proof. search by pigeonhole. crush. Qed." and all the details would be established by the assistant itself. This allows for concise proofs, especially in software where many proofs amounts to the invocation of some induction scheme and solving by rote substitution and rewriting.

> The difference is that in a proof assistant, you cannot gloss over a detail. So many of the lines establishes well-known facts which a mathematician has internalized in their brain.

Maybe an intermediate DSL that would allow some "fallacies" or shortcuts would also render the proof more readable to more people. And the weakness in the reasoning could be easily spotable by special keywords.

> You could store that in a library (and many proof assistants do!) but then the proof would probably be harder to follow for a first time reader.

I'm not sure I agree with that. There is a middle ground to find between rewriting a sort function everytime it is needed, and encapsulating everything in a main() function. Creating an API/DSL/Vocabulary is not easy, but def required to attract more developers.

The original proof I posted was organized slightly differently from your argument.

Some of those 120 lines were commentary, blanks and things like "qed". Also, I tried to used small steps in the proof. You can have a more concise proof if you are willing to take larger steps and rely more on automation. The cost is that the justification for the steps might become opaque to humans.

Here is a second attempt at the proof that follows your argument and uses more automation. It is much shorter than the original: https://gist.github.com/jmoy/27bcc72fb5a3f871b72c31e81bccb55...

> The cost is that the justification for the steps might become opaque to humans.

If the machine can tell "this proof is correct". Does the proof really need to be reviewed by humans? As long the human can easily read the problem which is proved, if the machine says the proof is complete, it should be good enough.

It has not been proven that the software is correct.

> If yes, proof assistants have to be improved on conciseness, imho

TBF the proof is written for readability, not concision.

But also, this happens in programming as well:

"A search function looking for `x` in a sorted list that starts in the middle of the list, compares the element to `x`, and then recursively searches the front half or back half of the list"

"A valid HTML document with one button that, when clicked, downloads a text file containing the md5sum of the page"

"A facebook clone"

True, but in other languages, developers try to fill the gap with numerous libraries and languages on top of each others, with abstractions on top of abstractions. Proof assistants feel "stuck" at a low level, with high expertise required to use them.

Reply on news.ycombinator.com