Hacker News Reader

Comment by curryhoward | Hacker News Reader

> The article doesn't say that the original proof was incorrect.

The article very clearly points out an error in the original proof.

The HN community can be so toxic sometimes. Inevitably whenever someone produces a new machine-checked proof, all these commenters come out of the woodwork explaining how assumptions/definitions are not verified and therefore the whole endeavor is somehow worthless.

A researcher being excited about their research is nothing to be ashamed about. I especially appreciate the fact that one of the authors took the time to make an accessible blog post to introduce us to their work.

View on HN

> The article very clearly points out an error in the original proof.

We're using slightly different notions of "proof": I am talking about (1) the proof steps involved in proving a given, fixed statement. You are talking about (2) a wider notion that includes the formulation of the statement to be proved. Both of these are valid meanings for the word "proof". Coq can only check the details of sense 1, not the additional details of sense 2. The error in the original proof (sense 2) is in these additional parts, not in the proof according to sense 1.

> assumptions/definitions are not verified and therefore the whole endeavor is somehow worthless.

This is not at all what I have done.

> A researcher being excited about their research is nothing to be ashamed about.

Right. And the actual work done here is reason enough for excitement.

> I especially appreciate the fact that one of the authors took the time to make an accessible blog post to introduce us to their work.

So do I. But the fact that the target audience keeps discussing the title shows that the title was not appropriate for the target audience.

> I am talking about (1) the proof steps involved in proving a given, fixed statement. You are talking about (2) a wider notion that includes the formulation of the statement to be proved.

No, I am not. The original proof used an implicit assumption, which is a problem with the proof proper, not the formulation of the statement to be proved. Using a proof assistant guarantees that there are no implicit assumptions, which is one reason why this work is notable. It rules out an entire class of errors which were present in previous work.

You wrote:

>>> The article very clearly points out an error in the original proof.

You didn't say what error you meant here, but later you wrote this:

> The original proof used an implicit assumption, which is a problem with the proof proper

This is true, but this is not pointed out in the article at all, let alone "very clearly".

As established elsethread, the article's problem with the assumption is not it being implict or explicit, the authors simply didn't want to have to use the assumption at all.

Reply on news.ycombinator.com