power in natural number

Stream: general

[Fan Zheng]

When I typed
theorem test (n : ℕ) : ¬ (7 ∣ 2^n + 1) := sorry
why does Lean complain that
failed to synthesize type class instance for
n : ℕ
⊢ has_pow ℕ ℕ?
Thanks in advance.

[Alex J. Best]

You need to import some libraries in order for powering on nats to be defined, for example if you are using mathlib you can do import data.nat.basic at the top of the file

[Timothee Lacroix]

Fan Zheng said:

When I typed
theorem test (n : ℕ) : ¬ (7 ∣ 2^n + 1) := sorry
why does Lean complain that
failed to synthesize type class instance for
n : ℕ
⊢ has_pow ℕ ℕ?
Thanks in advance.

this looks like one of the minif2f imo problems, which import this file https://github.com/openai/miniF2F/blob/main/lean/src/minif2f_import.lean and additionally uses these locales :

open_locale big_operators
open_locale nat
open_locale real
open_locale rat

With both imports and locales, you should be good to go for anything defined in minif2f :)

[Fan Zheng]

Right, I am just reproducing the proof given in the metaAI paper. In this regard, is there an easy way to know what to import and open_locale for a proof to work? The chat tool only gives statement, not the environment.

[Timothee Lacroix]

as said previously, if you import everything from minif2f_import and open the right locales it should work. (be aware that our proofs may only be valid for lean_version = "leanprover-community/lean:3.30.0" and mathlib rev = "9a8dcb9be408e7ae8af9f6832c08c021007f40ec" which you can set in your leanpkg.toml)

[Timothee Lacroix]

also, it might be safer to grab statements directly from minif2f : https://github.com/openai/miniF2F/blob/main/lean/src/valid.lean

[Eric Wieser]

https://github.com/openai/miniF2F/blob/main/leanpkg.toml and https://github.com/facebookresearch/miniF2F/blob/main/leanpkg.toml both say lean 3.42.0 and cb2b02fff213ed6f65bebd64446baac64137dcda; is the paper not using the same versions as what you released?

[Timothee Lacroix]

Eric Wieser said:

https://github.com/openai/miniF2F/blob/main/leanpkg.toml and https://github.com/facebookresearch/miniF2F/blob/main/leanpkg.toml both say lean 3.42.0 and cb2b02fff213ed6f65bebd64446baac64137dcda; is the paper not using the same versions as what you released?

The facebookresearch/miniF2F contains updates to miniF2F unrelated to the HTPS paper, but used in https://arxiv.org/abs/2210.12283
We tried to keep the lean /mathlib version fixed for the duration of the HTPS project (we didn't want performances bouncing up and down along with changes in mathlib), only including whatever changes necessary to match miniF2F/v1 with our set-up.

I'm currently in the process of trying to update our API to lean 3.48 but it's a bit difficult (mathlib grew in size and our API keeps the entire parse of mathlib around in RAM ...) . I hope the next update is lean 4 :p

[Eric Wieser]

mathlib grew in size and our API keeps the entire parse of mathlib around in RAM

Sounds similar to the reason that the Lean web editor is stuck on an old version!

[Fan Zheng]

I´ve got another question on the same theorem. I rewrote the proof a little bit. It seems that it also checked, but when I move the cursor to some of the lines, the tactic state seems wrong:

theorem test2 (n : ℕ) : ¬ (7 ∣ 2^n + 1) :=
begin
  rw nat.dvd_iff_mod_eq_zero,
  rw nat.add_mod,
  rw nat.mod_eq_of_lt,
  obviously,
  apply nat.strong_induction_on n,
  induction n,
  {
    intros n IH,
    cases n,
    norm_num,
    cases n,
    norm_num,
    cases n,
    norm_num,
    rw nat.succ_eq_add_one,
    rw pow_succ,
    rw nat.succ_eq_add_one,
    rw pow_succ,
    rw nat.succ_eq_add_one,
    rw pow_succ,
    norm_num [← mul_assoc],
    norm_num [nat.mul_mod],
    contrapose! IH,
    refine ⟨ n, _, IH ⟩,
    apply nat.le_succ_of_le,
    exact nat.le_succ (_),
  },
  exact n_ih,
end

For example, when I put the cursor on the line

intros n IH,

the tactic state is

n: ℕ
⊢ 2 ^ n % 7 + 1 % 7 < 7

but I was expecting

case nat.zero
⊢ ∀ (n : ℕ), (∀ (m : ℕ), m < n → 2 ^ m % 7 + 1 < 7) → 2 ^ n % 7 + 1 < 7

which is the case in the original proof. Also, when I move the cursor to the next line, it seems that only n : ℕ is pushed into the hypothesis. I can´t see IH, but it seems hidden, because later it is used anyway.

[Ruben Van de Velde]

Please, #backticks