3 ms·
> 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
by curryhoward 6y ago
> 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.
- tom_mellior 6y agoYou 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.