erdős #1135 · Collatz conjecture
Define by if is even and if is odd.Given any integer does there exist such that ?
Worked, still open.
number theory · open · prize $500 · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
Your $f$ is exactly the “shortcut” form of the **Collatz $ (3n+1) $ map**:
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 11 37 · open (literature)
theorem erdos_1135 : type_of% CollatzConjecture.collatz_conjectureformal-conjectures/1135.lean ↗
oeis
A006370 — The Collatz or 3x+1 map: a(n) = n/2 if n is even, 3n + 1 if n is odd.0,4,1,10,2,16,3,22,4,28,5,34,6,40,7,46,8,52,9,58,10,64,11,70,12,76,13,82,14,88,15,94,16,100,17,106,18,112,19,118,20,124,A008908 — a(n) = (1 + number of halving and tripling steps to reach 1 in the Collatz (3x+1) problem), or -1 if 1 is never reached.1,2,8,3,6,9,17,4,20,7,15,10,10,18,18,5,13,21,21,8,8,16,16,11,24,11,112,19,19,19,107,6,27,14,14,22,22,22,35,9,110,9,30,17
links
Collatz conjecture · reference
status
open