Zulip Chat Archive

Stream: new members

Topic: graded “sorry”

Alok Singh (S1'17) (Mar 07 2022 at 03:21):

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


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 (Mar 07 2022 at 06:22):

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 (Mar 07 2022 at 09:52):

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 (Mar 07 2022 at 09:59):

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

Martin Dvořák (Mar 07 2022 at 10:00):

However, there is not much of a difference from:

sorry --proof can be found at $URL

Martin Dvořák (Mar 07 2022 at 10:01):

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

Eric Wieser (Mar 07 2022 at 10:17):

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

Martin Dvořák (Mar 07 2022 at 10:25):

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

Eric Wieser (Mar 07 2022 at 10:33):

Which lean 3?

Martin Dvořák (Mar 07 2022 at 10:33):


Kyle Miller (Mar 07 2022 at 11:09):

import tactic.basic
import data.nat.basic

namespace tactic
namespace interactive

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

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 (Mar 07 2022 at 12:02):


Last updated: Dec 20 2023 at 11:08 UTC