undefined | Better HN

0 pointszarzavat10mo ago0 comments

Presumably an AI would formalise the proof in a system such as Lean, then you only need to trust the kernel of that proof system.

Rejecting a proof would be more complicated, because while for confirming a proof you only need to check that the main statement in the formalisation matches that of the conjecture, showing that a proof has been rejected requires knowledge of the proof itself (in general).

0 comments

lblume10mo ago

> requires knowledge of the proof itself (in general)

Why? If a proof is wrong it has to be locally invalid, i.e. draw some inference which is invalid according to rules of logic. Of course the antecedent could have been defined pages earlier, but in and of itself the error must be local, right?

IsTom10mo ago

Human-written proofs are not written in Lean to be checked easily and there'll be potentially many formalizations for written prose and only some of them will be what the author intended. You need to pick the right formalization before you can say that this proof has local errors.

lblume10mo ago

If a human reviewer rejects a proof, what do they consider apart from local errors? Formal proofs have formal local errors (which can be checked mechanically), while informal proofs have informal local errors (which require humans and some degree of hermeneutics to check). Am I missing something?

1 more reply

j / k navigate · click thread line to collapse

0 pointszarzavat10mo ago0 comments

Presumably an AI would formalise the proof in a system such as Lean, then you only need to trust the kernel of that proof system.

0 comments

lblume10mo ago

> requires knowledge of the proof itself (in general)

IsTom10mo ago

lblume10mo ago

1 more reply

j / k navigate · click thread line to collapse