Erdős 196

Stream: Formal conjectures

[Yan Yablonovskiy 🇺🇦]

Hey all, below is my preliminary version of Erdős 196, I am just worried its too simple and doesn't really work :

import FormalConjectures.Util.ProblemImports

/-!
# Erdős Problem 196

*Reference:* [erdosproblems.com/196](https://www.erdosproblems.com/196)
-/
open Function Set Nat

namespace Erdos196

/-- Must every permutation of $\mathbb{N}$, contain a monotone 4-term arithmetic progression. -/
@[category research open, AMS 5 11]
theorem erdos_196' (f : ℕ ≃ ℕ) : ∃S, IsAPOfLengthWith S 4 (sInf S) 1 → IsAPOfLength (f '' S) 4 := by
  sorry

end Erdos196

I think the sequences being monotone might be handled by $f$ being a bijection. But it also concerns me a little that the cited results use positive integers rather than naturals.

Davis, J. A. and Entringer, R. C. and Graham, R. L. and Simmons, G. J., *On permutations containing no long arithmetic progressions*. Acta Arith. (1977/78), 81-90.

I am also unsure how to encode the permutation with the bijection, should i be asking for an arithmetic progression $S$ with $d = 1$, such that the image of $f$ is a four term progression.

[Moritz Firsching]

That looks pretty good already, but I don't quite follow why 4 indexing numbers should form an AP with step 1 themselves, they only have to be monotone (in either direction), right? I think it is a bit confusing the way it is stated on erdosproblems.com, because I think the $1,2,3,4$ in the indexes there is misleading. they should by $i, j, k, l$ such that eitehr $i< j<k<l$ or $i>j>k>l$, if I understand the paper correctly. So I would write this as:

@[category research open, AMS 5 11]
theorem erdos_196 (f : ℕ ≃ ℕ) : ∃ (a : List ℕ),
    ((a.Sorted (· < · )) ∨ (a.Sorted (· > · ))) ∧ IsAPOfLength (f '' a.toFinset) 4 := by
  sorry

and this is formulated as a questions, let's use the answer(sorry) mechanism:

@[category research open, AMS 5 11]
theorem erdos_196 : (∀ (f : ℕ ≃ ℕ), ∃ (a : List ℕ),
    ((a.Sorted (· < · )) ∨ (a.Sorted (· > · ))) ∧ IsAPOfLength (f '' a.toFinset) 4)
    ↔ answer(sorry) := by

Regarding positive integers rather than naturals here: I wouldn't worry about that at all, adding a constant (for instant 1 to every number in the set shouldn't change the questions of arithmetic progressions at all here.)

[Yan Yablonovskiy 🇺🇦]

Thanks heaps! Makes sense , I had tried to use PNat but it complains about AddCommMonoid instances

[Yan Yablonovskiy 🇺🇦]

Moritz Firsching said:

@[category research open, AMS 5 11]
theorem erdos_196 : (∀ (f : ℕ ≃ ℕ), ∃ (a : List ℕ),
    ((a.Sorted (· < · )) ∨ (a.Sorted (· > · ))) ∧ IsAPOfLength (f '' a.toFinset) 4)
    ↔ answer(sorry) := by

In general is the preference for this repo to have hypothesis before or after the colon ( e.g. for mathlib
https://leanprover-community.github.io/contribute/style.html#hypotheses-left-of-colon )

[Moritz Firsching]

in general same as mathlib, but for the ↔ answer(sorry) to make sense, it is sometimes necessary to move them after the colon

[Moritz Firsching]

see also discussion now at the bottom of https://www.erdosproblems.com/forum/thread/196