Erdős problem 196

Disproved

There is a permutation of the natural numbers containing no four-term arithmetic progression in increasing or decreasing order. This disproves the conjecture that every permutation must contain one.

Read Lean proof Download Lean source Read explanation (PDF)Verification report Review decision

Submitted by JenW1N

Lean verification:: Passed
Conjectures review:: Approved
Reward:: Paid

The PDF is a working mathematical exposition. Lean verification applies to the formal source, not the prose.

Original question

Must every permutation of

\mathbb{N}

, contain a monotone 4-term arithmetic progression?

Formal statement

Proof target

import Mathlib
import FormalConjectures.ErdosProblems.«196»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos196.erdos_196" := by
  sorry

end Bounty

Open this target’s Challenge.lean Task bundle on GitHub

Original conjecture (Lean type)

True ↔ ∀ (f : ℕ ≃ ℕ), HasMonotoneAP (⇑f) 4

Original conjecture source: FormalConjectures/ErdosProblems/196.lean

Source type SHA-256: sha256:1969cd67b2bc2d369d8a90a88c2aec507b2944165032da740c678331c519e620
Task id: fc-v2-erdos196-erdos-196-3bbe9ed98063619d7bcec9d7-formalized
Task commitment: sha256:f08ef1b1c675c82f71b0ef971637a2257db93023dea0f3599bf93d40404e0b94

References

erdosproblems.com/196

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord

Contribution history

1 piece · 20 lemmas

Individual lemmas, special cases and supporting work, shown in their original scope.

2 Sept 2026
- Erdős 196: monotone 4-AP API for permutations, decidable AP tests, growth obstruction
  5FqLp5…FfZZiK · 20 lemmas

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

versions/fc-v2-erdos196-erdos-196-3bbe9ed98063619d7bcec9d7-formalized →

conjectures-contribution

Every published piece for this problem, with its Lean source and its signed record.

contributions/erdos-196 →