Proving FLT with norm_num

Stream: general

[Eric Wieser]

import Mathlib

variable (ignore_me_please : ∀ a b c n : ℕ, a ^ n + b ^ n ≠ c ^ n)

example (n) (hn : n > 2) (a b c : ℕ) : a ^ n + b ^ n ≠ c ^ n := by
  clear ignore_me_please -- I promise not to use this, it would be cheating
  norm_num [*]

[Eric Wieser]

(ok, I got the statement wrong, but obviously the interesting thing here is the footgun, not the fact I pointed it at the foot I thought was FLT)

[Kevin Buzzard]

great, I can retire early! So clear isn't doing what I think it's doing?

[Eric Wieser]

norm_num is matching * against the context before clear ran

[Damiano Testa]

And people still complain that there is the need for better automation.

[Eric Wieser]

My initial takeaway here is that * is just really dangerous in the presence of variables (without the clear the proof does what you'd expect but not what you'd want), and secondarily there is obviously a bug above.

[Floris van Doorn]

I think we still need to overhaul the behavior of variable in Lean 4, as was voted 22 to 0 in this poll: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/automatic.20inclusion.20of.20variables.20in.20mathlib.204/near/386620103

[Kim Morrison]

An update on lean#2452: It is on the agenda, but not immediately. @Sebastian Ullrich wants to address this in his upcoming work on intra-file parallelism, where there will have to be substantial changes to the variable mechanism anyway. Obviously this is a big project and won't happen overnight, but I think after incrementality is merged, the path is at least open.

[Patrick Massot]

Are there news that I missed about incrementality?

[Kim Morrison]

It won't make v4.8.0-rc1, but v4.9.0-rc1 seems plausible. lean4#3636 if you'd like to follow the play-by-play!