A machine checked proof of the following: "In a finite group of people, some of whom are friends with some of the others there must be at least two people who have the same number of friends."
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.
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.
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.
> 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"
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.
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.
> 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.
Similar reasoning solves one of my favorite brain teasers:
“My wife and I greet 4 other couples. After the handshakes, I ask everyone how many people they shook hands with and get no duplicate replies; no one shook hands with their partner or themselves. How many people did my wife shake hands with?”
This puzzle stumps everyone I know that hasn’t been exposed to combinatorics.
Fun! Let's see; there are 10 people, and 5 couples. Since nobody shook hands with themselves or their partner, everyone (except the question asker, critically) maps to a unique shake number in the set 0 .. 8 (cardinality 9). The question asker also shook one of 0 .. 8 hands, same as one of the other people (otherwise there would be no solution per pigeon-hole principle).
We can easily see the 8-hand-shaker must have a 0-hand-shaker as their partner (since everyone else shook at least one hand, the all-shaker's). We can also see, when constructing possible graphs for smaller total numbers of couples (1, 2, 3, 4, etc.) that if the shake graph of N couples satisfies the uniqueness constraint then we can always add another couple in a way which preserves uniqueness: the new couple is an (2N-2, 0) shaker pair, where everyone else has their shake count incremented by one. Thus we see the question-asker's wife's shake-count is equal to the number of other couples, in this case 4.
I would still need to prove that any shake-graph satisfying the uniqueness constraint must be unique (under isomorphism swapping shake numbers within couples); we saw with the iterative construction that the answer is equal to the number of other couples, but it isn't yet clear that this is the only possible answer. Of course, we can infer from the question itself that there is a unique solution, and so any found solution must therefore be unique :P
After the "8 must be paired with 0" step, my next step was to say, "Now, there is someone who shook hands with 7 people. We know he didn't shake hands with Mr. 0, so he must have shaken hands with everyone else except his wife. Meanwhile, there's also someone who shook hands with 1 person, and we already know he shook with Mrs. 8, so he must have not shaken hands with anyone else. Therefore, 7 and 1 must be a couple."
Then, accounting for the shakings with 7 and 8 and the non-shakings with 0 and 1, we similarly see that 2 can't have shaken hands with anyone else, but 6 must have shaken hands with everyone else except his partner, so 2 and 6 must be paired as well. The 5-3 pairing follows too, after which we're left with 4 and the question-asker, who are a couple by process of elimination.
Incidentally, we conclude that the question-asker also shook hands with 4 people: Mrs. 8, 7, 6, and 5.
