Natural and Useful Proofs

Trustworthy and Useful

• We talk a lot about verification and trust
• If it is raining, I should take my umbrella. It is raining. Explain why I should take my umbrella.
  • LLMs answer naturally

    Whenever it is raining I should take my umbrella.
    It is raining, so the current situation falls under that rule.
    Therefore, I should take my umbrella.

  • ATPs answer unnaturally

    Assume that I do not take my umbrella.
    From that assumption we are led to the conclusion that it is not raining.
    But this contradicts the given fact that it is raining.
    Therefore the assumption that I do not take my umbrella must be false.
    So I should take my umbrella.

    WTF?!!?

A Call to Arms

• A refutation is a proof that the conjecture is a theorem (not a proof of the theorem)
• A closed tableau is a magical proof that conjecture is a theorem
• A natural deduction can be a natural proof of the theorem
• A sequent calculus proof cannot be a natural proof of the theorem
• An direct proof is a natural and useful proof ... all inferences are consequences
  • logical consequences
  • mathematical consequences
  • legal consequences
  • chemical consequences
  • physical consequences
  • political consequences
  • etc.

• A "proof that there is a proof" is useful for finding an axiomatic proof