imo problems that are challenging to formalize

Stream: new members

[Horst Staley]

Hello everyone :wave:

I am interested in getting my hands dirty with Lean4 by formalizing some IMO problems (hopefully can also make some useful contributions to mathlib on the way) ...

can someone point me to some IMO problems that are known to be difficult to formalize ... I can tell the geometry ones are challenging, but are there other ones as well?

Thanks in advance!

[Scott Morrison]

I'm not sure you'll find someone with a ready answer for you. One simple answer is anything that hasn't yet been formalized!

[Scott Morrison]

The geometry problems are difficult because they need a lot of Mathlib development to build good API --- but that is not what a beginner wants to tackle!

[Horst Staley]

Thanks @Scott Morrison that was definitely my plan B ... if nobody pointed out particularly interesting or challenging ones, I will just take a random one :)

[Scott Morrison]

The basic problem is that "difficult to formalize" doesn't correlate at all well with "difficult as an exam question". Any generally "difficult to formalize" means "you have to design new API in Mathlib", which is not what you're looking for initially.

[Scott Morrison]

If you're just looking for "difficult as an exam question", start with Q6s. :-)

[Horst Staley]

nono, definitely not ... I'm just looking for difficult to formalize (and I was thinking of starting with just the problem statements)

[Horst Staley]

if I just wanted to solve hard math problems, I have my chalkboard, no need for lean :D

[Scott Morrison]

Much better exercise to do the proofs. :-)

[Joseph Myers]

It's hard to be sure your formal statement is correct if you don't formalize a proof (consider the case of an AI that claimed a solution to a hard problem that had been wrongly formalized using ℕ subtraction).

Having a detailed written informal solution is important before starting formalizing (see e.g. The IMO Compendium (for 1959-2009) or shortlist booklets (2006-2022) (but watch out for the version of a problem in the shortlist differing significantly from the version on the final exam) or the AoPS wiki).

See also archive/imo/README.md (in mathlib3, one of the miscellaneous .md files not yet ported to mathlib4) for more discussion of IMO formalizations.

[David Renshaw]

FYI, I've been doing a bunch of olympiad formalization here and contributions are welcome.

[Joseph Myers]

I think all 386 past IMO problems would be appropriate for the mathlib archive (we currently have 32 of them, for an average of half a problem per IMO), as would problems from other (e.g. national / regional) olympiads (or proof-based mathematics competitions in general) such as you have in that repository, if brought up to mathlib standards (including in particular factoring out any results of more general use and putting those in mathlib proper). Of course getting something up to mathlib standards may be a lot of work - I don't expect to convert my British MO formalizations to Lean 4 or to attempt to get them up to mathlib standards.

[Eric Wieser]

Joseph Myers said:

See also archive/imo/README.md (in mathlib3, one of the miscellaneous .md files not yet ported to mathlib4) for more discussion of IMO formalizations.

#6031

[Yury G. Kudryashov]

Do we have a list of files/webpages that we should migrate? The style guide still talks about Lean 3.

[Yury G. Kudryashov]

I left some comments on #6031

[Joseph Myers]

I think there are some additional .md files to migrate (CITATION.md for example), though of course not all the placeholder files that say that some documentation was moved to the website. And the whole website needs updating to Lean 4 where not already done.

[Horst Staley]

Thanks @Joseph Myers

[Horst Staley]

Hello everyone, I have decided to start with IMO 1961 Q3

def ProblemEquation (n : ℕ) (x : ℝ) : Prop :=
  (cos x)^n - (sin x)^n = 1

def evenSet : Set ℝ :=
  {x : ℝ | ∃ k : ℤ, x = ↑k * π}

def oddSet : Set ℝ :=
  {x : ℝ | ∃ k : ℤ,
  x = ((4 * ↑k - 1) * (π / 2)) ∨
  x = ((4 * ↑k) * (π / 2))}

theorem imo1961_q3 {n : ℕ} {x : ℝ} : (Even n ∧ ProblemEquation n x ↔
  (x ∈ evenSet)) ∧ (Odd n ∧ ProblemEquation n x ↔ x ∈ oddSet) := by
  constructor

Before I started cranking on the proof, I just wanted to doublecheck that I've set it up in the best possible way ... I appreciate any feedback! :pray:

[David Renshaw]

In this problem, part of the answer is actually coming up with the solution set, and your setup does not really surface that.

[David Renshaw]

I would do something more like

def solutionSet (n : ℕ) : Set ℝ :=
  if Even n
  then { x : ℝ | ∃ k : ℤ, x = ↑k * π}
  else { x : ℝ | ∃ k : ℤ,
         x = ((4 * ↑k - 1) * (π / 2)) ∨
         x = ((4 * ↑k) * (π / 2))}

theorem imo1961_q3 {n : ℕ} {x : ℝ} :
    (cos x)^n - (sin x)^n = 1 ↔ x ∈ solutionSet n := by
  sorry

[David Renshaw]

And I think we're eventually going to want some kind of annotation that we can put on that solutionSet def, to make it clear that supplying that term is supposed to be part of the problem.

[David Renshaw]

Lately I've been adding a -- @[solution_data] commented-out (fake) annotation for such defs, as here: https://github.com/dwrensha/math-puzzles-in-lean4/blob/ea6cedd064e12e7853c8e8fed89e3d585ac3ce54/MathPuzzles/Usa1998Q4.lean#L53-L54

[Horst Staley]

thank you, much more elegant

[Horst Staley]

@David Renshaw or others, is there an example of how to construct the solutionSet somehow within a Lean environment?

Seems like most of the answers here figure it out via pen and paper ...

[David Renshaw]

You want to automatically fill in the term for solutionSet? That's really difficult, but it's ultimately something we'll need to do as part of the IMO Grand Challenge.

[David Renshaw]

Hm... I suppose a tricky aspect is that if you are filling in the term in tactic mode, you don't have easy access to the later definition imo1961_q3 where the def is used.

[Horst Staley]

eventually yes, but at first I was thinking just demonstrating that it could be done manually in the Lean environment would be a good step

[David Renshaw]

what do you mean by "in the Lean environment"?

[Horst Staley]

I mean, a sequence of steps/tactics that would begin with just (cos x)^n - (sin x)^n = 1, and end up with the contents of solutionSet ...

[Horst Staley]

maybe the best analogue would be to scratch work?

[Horst Staley]

hopefully what I am saying makes sense, I am new to Lean

[Eric Wieser]

In Lean 3 it was possible to write:

def the_problem (ans : nat) : Prop := 1 + 2 = ans

-- this should be a theorem, but if you make it a def then the `_` can be filled in later
def obvious : the_problem _ := rfl

#check obvious -- the_problem (1 + 2)

[David Renshaw]

I like the word "proplem", but I don't understand what Eric is saying

[David Renshaw]

In our case we could do

theorem imo1961_q3 {n : ℕ} (solutionSet: Set ℝ) {x : ℝ} :
    (cos x)^n - (sin x)^n = 1 ↔ x ∈ solutionSet := by sorry

and then ... ?

[Eric Wieser]

The point is that in Lean 3 you could use a def where you would normally use a theorem, and it leaves a metavariable to solve mid-proof

[David Renshaw]

interesting

[Horst Staley]

is there a way to do this in Lean4?

[Horst Staley]

is there a better channel to get feedback on my lean code? or should I just keep posting it here

[Kevin Buzzard]

Posting here is fine

[Horst Staley]

(deleted)

[Kevin Buzzard]

Uploading code by attaching it is quite inconvenient, eg I can't see it on mobile. Just paste the code in between triple backticks unless it's well over 100 lines in which case link to a gist

[Horst Staley]

Sorry I’m also on mobile :)

[Horst Staley]

import Mathlib.Data.Real.Basic
import Mathlib.Data.Nat.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
import Mathlib.Tactic.Linarith

open Real
open Nat

lemma sin_even_nonneg (x : ℝ) (n : ℕ)
(even_n : Even n) : 0 ≤ sin x ^ n :=
by
  rcases even_n with ⟨r, hr⟩
  rw [hr]
  rw [← two_mul]
  rw [rpow_nat_cast]
  rw [pow_mul]
  apply pow_nonneg
  apply sq_nonneg

lemma cos_pow_ge_one (x : ℝ) (n : ℕ)
(even_n : Even n)
(f : cos x ^ ↑n = 1 + sin x ^ ↑n) : cos x ^ ↑n ≥ 1 := by
  rw [f]
  apply le_add_of_nonneg_right
  exact sin_even_nonneg x n even_n

lemma abs_cos_pow_le_one (x : ℝ) (n : ℕ) : abs (cos x) ^ n ≤ 1 := by
  apply rpow_le_one
  apply abs_nonneg
  apply abs_cos_le_one
  apply cast_nonneg

lemma cos_pow_le_one (x : ℝ) (n : ℕ) : (cos x) ^ n ≤ 1 := by
  have f := le_abs_self ((cos x) ^ n)
  have g := abs_cos_pow_le_one x n
  have h := abs_rpow_le_abs_rpow (cos x) ↑n
  have j := le_trans f h
  have k := le_trans j g
  exact k

lemma sin_eq_zero_if_n_even_and_f (x : ℝ) (n : ℕ) (even_n : Even n) :
(cos x)^n - (sin x)^n = 1 → sin x = 0 := by
  rw [sub_eq_iff_eq_add]
  intro f
  have g := cos_pow_ge_one x n even_n f
  have h := cos_pow_le_one x n
  have k := le_antisymm h g
  have l := congr_arg abs k
  rw [abs_one] at l
  rw [rpow_nat_cast] at l
  rw [abs_pow_eq_one] at l
  have m := eq_or_eq_neg_of_abs_eq l
  rw [← @sin_eq_zero_iff_cos_eq x] at m
  exact m
  apply Nat.pos_of_ne_zero
  rw [k] at f
  contrapose f
  rw [← neZero_iff] at f
  rw [not_neZero] at f
  intro f_1
  rw [f] at f_1
  rw [rpow_nat_cast] at f_1
  rw [_root_.pow_zero] at f_1
  norm_num at f_1

lemma f_holds_if_n_nonzero_even_and_x_integer_multiple_of_pi (x : ℝ) (n : ℕ) (k : ℤ)
(n_zero : n ≠ 0) (even_n : Even n) : x = ↑k * π →
cos x ^ ↑n - sin x ^ ↑n = 1 := by
  intro f
  have h : ∃ k : ℤ, ↑k * π = x
  use k
  exact symm f
  rw [← sin_eq_zero_iff] at h
  rw [h]
  rw [sin_eq_zero_iff_cos_eq] at h
  rcases h with h1 | h2
  rw [h1]
  norm_num
  exact Nat.pos_of_ne_zero n_zero
  rw [h2, rpow_nat_cast, rpow_nat_cast, zero_pow, sub_zero,
  neg_one_pow_eq_one_iff_even]
  exact even_n
  norm_num
  exact Nat.pos_of_ne_zero n_zero

-- @[solution_data]
def solutionSet (n : ℕ) : Set ℝ :=
  if n = 0
  then ∅
  else if Even n
  then { x : ℝ | ∃ k : ℤ, x = ↑k * π}
  else { x : ℝ | ∃ k : ℤ,
         x = ((4 * ↑k - 1) * (π / 2)) ∨
         x = ((4 * ↑k) * (π / 2))}

theorem imo1961_q3 {x : ℝ} {n : ℕ} :
  (cos x)^n - (sin x)^n = 1 ↔ x ∈ solutionSet n := by
  rw [solutionSet]
  split_ifs with n_zero n_even
  constructor

  -- case n=0
  intro f
  rw [rpow_nat_cast, rpow_nat_cast, sub_eq_iff_eq_add, n_zero, _root_.pow_zero,
  _root_.pow_zero, one_add_one_eq_two] at f
  norm_num at f
  exfalso

  -- case n even, forward direction
  constructor
  intro f
  have g := sin_eq_zero_if_n_even_and_f x n n_even f
  rw [sin_eq_zero_iff] at g
  rcases g with ⟨k, g1⟩
  constructor
  exact symm g1

  -- case n even, reverse direction
  intro f
  rcases f with ⟨a, b⟩
  exact f_holds_if_n_nonzero_even_and_x_integer_multiple_of_pi x n a n_zero n_even b

  --case n odd
  sorry

[Kevin Buzzard]

Edit the post to use ``` at top and bottom (you've used the wrong ticks)

[Kevin Buzzard]

sin_even_nonneg shouldn't exist in that form -- any real raised to an even power is nonnegative. Make the result more general and change the name?

[Kevin Buzzard]

cos_pow_le_one has a much more elegant proof as a three line calc block

[Kevin Buzzard]

sin_eq_zero_if_n_even : lemma names shouldn't have if or an and in -- take a look at the #naming convention. We use of for both. and would only be in the name of a lemma which explicitly mentioned the logical $\land$ symbol

[Kevin Buzzard]

The layout of the sin_eq_zero_if_n_even proof is poor -- you should never have two open goals in your context; when this happens you need to indent. If you don't do this it makes proofs very hard to read away from lean

[Kevin Buzzard]

Nice job though -- you're half way there!

[Horst Staley]

2/3 :) if you consider the n=0 case

[Horst Staley]

Thanks!

[Horst Staley]

OK, I just had the time to do another pass, would you mind critiquing again?

import Mathlib.Data.Real.Basic
import Mathlib.Data.Nat.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
import Mathlib.Tactic.Linarith

open Real
open Nat

lemma rpow_even_nonneg {x : ℝ} {n : ℕ}
(even_n : Even n) : 0 ≤ x ^ n := by
  rcases even_n with ⟨r, hr⟩
  rw [hr, ←two_mul, rpow_nat_cast, mul_comm, pow_mul]
  have g:= sq_nonneg (x^r)
  rw [rpow_nat_cast] at g
  exact g

lemma cos_pow_ge_one {x : ℝ} {n : ℕ}
(even_n : Even n) (f : cos x ^ ↑n = 1 + sin x ^ ↑n) : cos x ^ ↑n ≥ 1 := by
  rw [f]
  apply le_add_of_nonneg_right
  exact rpow_even_nonneg even_n

lemma abs_cos_pow_le_one {x : ℝ} {n : ℕ} : abs (cos x) ^ n ≤ 1 := by
  apply rpow_le_one
  apply abs_nonneg
  apply abs_cos_le_one
  apply cast_nonneg

lemma cos_pow_le_one {x : ℝ} {n : ℕ} : (cos x) ^ n ≤ 1 :=
  calc
    (cos x) ^ n ≤ abs ((cos x) ^ n) := le_abs_self ((cos x)^n)
    _           ≤ abs (cos x) ^ n   := abs_rpow_le_abs_rpow (cos x) ↑n
    _           ≤ 1                 := abs_cos_pow_le_one

lemma sin_eq_zero_of_even_f {x : ℝ} {n : ℕ} (even_n : Even n) :
(cos x)^n - (sin x)^n = 1 → sin x = 0 := by
  rw [sub_eq_iff_eq_add]
  intro f
  if hn : n = 0 then
    rw [rpow_nat_cast, rpow_nat_cast] at f
    rw [hn] at f
    norm_num at f
  else
    have g :=
    congr_arg abs (le_antisymm (@cos_pow_le_one x n) (cos_pow_ge_one even_n f))
    rw [abs_one, rpow_nat_cast, abs_pow_eq_one (cos x) (Nat.pos_of_ne_zero hn)] at g
    have h := eq_or_eq_neg_of_abs_eq g
    rw [← @sin_eq_zero_iff_cos_eq x] at h
    exact h

lemma exists_integer_of_integer {x : ℝ} {k : ℤ} : x = ↑k * π → ∃ k : ℤ, ↑k * π = x := by
  intro f
  use k
  exact symm f

lemma f_holds_of_n_nonzero_even_x_int_multiple_of_pi {x : ℝ} {n : ℕ} {k : ℤ}
(n_zero : n ≠ 0) (even_n : Even n) : x = ↑k * π →
cos x ^ ↑n - sin x ^ ↑n = 1 := by
  intro f
  have g := exists_integer_of_integer f
  have h := Nat.pos_of_ne_zero n_zero
  rw [← sin_eq_zero_iff] at g
  rw [g]
  rw [sin_eq_zero_iff_cos_eq] at g
  apply Or.elim g
  . intro g1
    rw [g1]
    norm_num
    exact Nat.pos_of_ne_zero n_zero
  . intro g2
    rw [g2, rpow_nat_cast, rpow_nat_cast, zero_pow h, sub_zero, neg_one_pow_eq_one_iff_even]
    exact even_n
    norm_num

-- @[solution_data]
def solutionSet (n : ℕ) : Set ℝ :=
  if n = 0
  then ∅
  else if Even n
  then { x : ℝ | ∃ k : ℤ, x = ↑k * π}
  else { x : ℝ | ∃ k : ℤ,
         x = ((4 * ↑k - 1) * (π / 2)) ∨
         x = ((4 * ↑k) * (π / 2))}

theorem imo1961_q3 {x : ℝ} {n : ℕ} :
  (cos x)^n - (sin x)^n = 1 ↔ x ∈ solutionSet n := by
  rw [solutionSet]
  split_ifs with n_zero n_even
  constructor

  -- case n=0
  intro f
  rw [rpow_nat_cast, rpow_nat_cast, sub_eq_iff_eq_add, n_zero, _root_.pow_zero,
  _root_.pow_zero, one_add_one_eq_two] at f
  norm_num at f
  exfalso

  -- case n even, forward direction
  constructor
  intro f
  have g := sin_eq_zero_of_even_f n_even f
  rw [sin_eq_zero_iff] at g
  rcases g with ⟨k, g1⟩
  constructor
  exact symm g1

  -- case n even, reverse direction
  intro f
  rcases f with ⟨a, b⟩
  exact f_holds_of_n_nonzero_even_x_int_multiple_of_pi n_zero n_even b

  --case n odd
  sorry

[Horst Staley]

The exists_integer_of_integer lemma seemed a bit hacky to me, but i couldn’t figure out a simpler way to transform it

[David Renshaw]

Instead of pulling that out as a lemma, you could directly do

  have g : ∃ k : ℤ, ↑k * π = x := ⟨k, f.symm⟩

[Ioannis Konstantoulas]

Joseph Myers said:

It's hard to be sure your formal statement is correct if you don't formalize a proof (consider the case of an AI that claimed a solution to a hard problem that had been wrongly formalized using ℕ subtraction).

Can you link to that story?

[Joseph Myers]

https://arxiv.org/pdf/2205.11491.pdf (last page, proof of an incorrect version of IMO 2001 problem 6).