`simp_all` May Make Goals Unprovable

[yangky11]

Hi Jannis,

I'm playing with LLM-aesop and found an example where it cannot prove a theorem because of the normalization that aesop performs using simp_all.

https://github.com/yangky11/miniF2F-lean4/blob/6dfeeb0788de2bd2e35ae728a108006460f62f8b/MiniF2F/Valid.lean#L330

This theorem can be proved by linarith (which LLMs can correctly generate) but not simp_all ; linarith. After simp_all, the hypothesis x * (1 / 2 + 2 / 3) = 1 becomes x * (2⁻¹ + 2 / 3) = 1, which cannot be solved by linarith.

I'm wondering if there is any workaround. For example, is there an option to disable normalization or use a more conservative strategy for normalization? Thank you!

[JLimperg]

I would count this as a linarith deficiency: it should recognise that 2⁻¹ is in the linear arithmetic fragment. You could open a mathlib issue about this.

As a workaround, you can disable Aesop's builtin simp_all with aesop (simp_options := {enabled := false}). You could also remove the offending simp lemma with an (erase ...) clause.

[yangky11]

That makes sense. I'll open an issue in mathlib. Thx!