Potential tactic bug

Stream: mathlib4

[Andreas Gittis]

I've been training a ML model to prove theorems in Lean. The good news is that in a stupendous feat of engineering (and after many epochs of incremental progress) my model's performance rocketed up to a sizzling 99.83% on miniF2F. The bad news is that all the proofs leverage the same bug displayed in the MWE below:

import Mathlib

open BigOperators Real Nat Topology

theorem amc12a_2019_p21 (z : ℂ) (h₀ : z = (1 + Complex.I) / Real.sqrt 2) :
  ((∑ k ∈ Finset.Icc 1 12, z ^ k ^ 2) * (∑ k ∈ Finset.Icc 1 12, 1 / z ^ k ^ 2)) = 36 := by
  exfalso
  apply lt_irrefl (2 : ℝ)
  apply lt_of_lt_of_le
  bound
  positivity

The message in the InfoView at the end says"No Goals" which allowed my model to cheat, but there is a red underline under the theorem name that reads the following error:

"(kernel) application type mismatch
lt_of_lt_of_le (Eq.symm h₀ ▸ Int.lt_floor_add_one 2)
argument has type
(fun z _h => 2 < ↑⌊2⌋ + 1) z ⋯
but function has type
2 < 0 → 0 ≤ 2 → 2 < 2"

Anyway, the message in the InfoView seems like it might be unintended behavior of some sort. Submitted for your consideration.

[Edward van de Meent]

i think this is a bug caused by bound not running isDefEq on the goal, or something like that? If it did, the goal after bound wouldn't contain ?b, and would cause positivity to fail here. (an example of what this would be like is given replacing bound by exact by bound)

[Edward van de Meent]

Since bound is a mathlib tactic, this conversation should probably be moved to #mathlib4

[Michael Rothgang]

I pinged the maintainers - this thread should get moved soon

[Notification Bot]

This topic was moved here from #lean4 > Potential tactic bug by Bryan Gin-ge Chen.

[Edward van de Meent]

alternatively to my previous suggestion (assigning the metavariable) of what would be expected behaviour, maybe the more desirable behaviour for tactics of this sort is throwing an error when run on a goal with unassigned metavariables?

[Kevin Buzzard]

Checking to see that you have proved what you were supposed to have proved is a very subtle question and there have been plenty of discussions about it in the #Machine Learning for Theorem Proving channel.

[Andreas Gittis]

Kevin Buzzard said:

Checking to see that you have proved what you were supposed to have proved is a very subtle question and there have been plenty of discussions about it in the #Machine Learning for Theorem Proving channel.

Hm, what do you mean by that? It's true that there isn't a formal way to verify the problem you've formalized is the problem you want to prove, but in this case the Lean kernel knows that the proof is incorrect but the Lean InfoView doesn't. I don't think there is any ambiguity in the case of rejection by the kernel.

Edward van de Meent said:

alternatively to my previous suggestion (assigning the metavariable) of what would be expected behaviour, maybe the more desirable behaviour for tactics of this sort is throwing an error when run on a goal with unassigned metavariables?

I guess this is considered a tactic bug, but is it intended behavior for Lean not to send information of a failed proof in the kernel back to the InfoView? If that's a design choice, what's the motivation for it?

[Kevin Buzzard]

Andreas Gittis said:

Hm, what do you mean by that? It's true that there isn't a formal way to verify the problem you've formalized is the problem you want to prove, but in this case the Lean kernel knows that the proof is incorrect but the Lean InfoView doesn't. I don't think there is any ambiguity in the case of rejection by the kernel.

I mean that there are entire repos such as https://github.com/GasStationManager/SafeVerify devoted to the problem of checking whether something is a proof of a theorem.

[Edward van de Meent]

Andreas Gittis said:

Is it intended behavior for Lean not to send information of a failed proof in the kernel back to the InfoView? If that's a design choice, what's the motivation for it?

I'm not quite sure what you mean? if you put the cursor on the declaration name, it shows the kernel error in the infoview, no?

[Andreas Gittis]

Edward van de Meent said:

Andreas Gittis said:

Is it intended behavior for Lean not to send information of a failed proof in the kernel back to the InfoView? If that's a design choice, what's the motivation for it?

I'm not quite sure what you mean? if you put the cursor on the declaration name, it shows the kernel error in the infoview, no?

Ah yes you're right it does show next to the theorem name. I've always checked proofs by putting the cursor at the end of the last tactic in the proof and nothing shows up in the InfoView there (except "No Goals").