Proof of false using library_search

Stream: mathlib4

[Alex Keizer]

I was having some issues with library_search succeeding, yet giving only

𝔗𝔯𝔶 𝔱𝔥𝔦𝔰: refine ?_

as a suggestion (and repeating it ~200 times).

In the process of coming up with an MWE, however, I stumbled on a proof of false

import Mathlib

theorem falsum : False :=
by library_search

#print axioms falsum   -- 'falsum' depends on axioms: [sorryAx]

I expected that library_search would succeed only if it actually found an applicable proof, but it seems to have snuck in a sorry. Is that intended?

This is using mathlib4 commit ed053df and the lean version used by that mathlib, i.e., leanprover/lean4:nightly-2022-03-27

[Kevin Buzzard]

Ha! I'm not really sure that counts as a proof of false :-) But nice observation!

[Reid Barton]

Presumably the question is why whatever library_search used is in the library

[Mario Carneiro]

Isn't this already fixed? I feel like I have seen this bug report 2 or 3 times now

[Mario Carneiro]

does anyone know why "try this" is in fraktur now?

[Henrik Böving]

It's definitely been like this quite long, I remember lots of occasions where this happened when library_search couldnt find a proof

[Mario Carneiro]

Oh, this is a different issue. Looks like if none of the proofs work it admits the goal

[Mario Carneiro]

I was thinking this was the issue where library_search would explicitly apply sorryAx

[Mario Carneiro]

@Gabriel Ebner Not sure how this is all supposed to work, but this seems suspicious:

      for suggestion in suggestions do
        addTermSuggestion tk (← instantiateMVars mvar)

suggestion is unused

[Mario Carneiro]

I believe the huge number of refine ?_ suggestions are supposed to be suggestions to apply many lemmas from the library but you aren't seeing them because of this bug

[Mario Carneiro]

mathlib4#255

[Scott Morrison]

I think Gabriel wrote "Try this" in fraktur so we would all be so annoyed by it that someone wrote proper editor integration for "Try this" suggestions. :-)