graded “sorry”

Stream: new members

[Alok Singh (S1'17)]

heard this from david spivak: sorry could be a whole system that essentially allows appeals to authority in a structured way

example:

sorry “proof can be found at $URL”

the grading is where some authority has heigher weight than another.

just thought it was an interesting idea since appeals to authority are so common in day to day practice

[Johan Commelin]

Something like that could certainly be done. But note that mathlib doesn't allow sorry in the first place. So this would be a feature for projects building on top of mathlib.

[Eric Wieser]

Appealing to authority is risky here, because the authority only says "I have a proof for X", and doesn't do anything to reassure you that "X" is what you told lean you were trying to prove

[Martin Dvořák]

To me, the suggested syntax seems more like a convenient way to write TODO, rather than appealing to authority.

[Martin Dvořák]

However, there is not much of a difference from:

sorry --proof can be found at $URL

[Martin Dvořák]

The suggested syntax is probably better — the compiler would then be able to provide a list of all sorrys with respective messages.

[Eric Wieser]

I think in tactic mode sorry "msg" might already be supported

[Martin Dvořák]

It doesn't work on my computer (lean3).

[Eric Wieser]

Which lean 3?

[Martin Dvořák]

leanprover-community/lean:3.38.0

[Kyle Miller]

import tactic.basic
import data.nat.basic

namespace tactic
namespace interactive
setup_tactic_parser

meta def appeal_to (t : parse texpr) : tactic unit :=
do tactic.trace $ format! "Appeal to authority: {t}",
   tactic.admit

end interactive
end tactic

theorem flt {a b c n : ℕ} (ha : 0 < a) (hb : 0 < b) (h : a^n + b^n = c^n) :
  n = 1 ∨ n = 2 :=
by appeal_to "Andrew Wiles"

-- Appeal to authority: "Andrew Wiles"
-- declaration 'flt' uses sorry

[Martin Dvořák]

(deleted)