3 ms·

If there's a bug in the theorem prover and it proves itself, it still has that bug.

• spott 10y ago
  Only if the bug in the prover allows the bug in the prover, which seems unlikely (unless the bug is pretty huge).
  • timjver 10y ago
    "seems unlikely" isn't really cutting it, when we're talking about formal systems.
  • mekaj 10y ago
    Trivial, small example: the bug is the prover accepts all inputs.
• burke 10y ago
  Yep. Imagine a prover that accepts all statements. It would accept a buggy program, and it would accept itself. It would obviously help reduce errors but it wouldn't categorically eliminate them.
• nabla9 10y ago
  It would have to be kind of fixed point of bugs (like finding cryptographic hash that equal to the input value). It wold be incredibly unlikely.