Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

No nontrivial Syracuse cycle contains a value below 330750

Proved
syracuse_no_cycle_below_330750

by Zexuan Liu · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

collatznumber-theory

Let TTT be the Syracuse map, sending nnn to the odd part of 3n+13n+13n+1. If zzz is a positive integer with z≤330749z \le 330749z≤330749 and Ta(z)=zT^a(z) = zTa(z)=z for some a≥1a \ge 1a≥1, then z=1z = 1z=1. The return time is arbitrary; no minimality is assumed.

The argument is the natural one for cycles. Passing to the least value www on the orbit of zzz, one has w≤z<330750w \le z < 330750w≤z<330750, and www is odd and positive because it is a value of TTT. If www were greater than 111 it would admit a strictly smaller iterate, by the descent result for this range — but www is the orbit minimum, so no iterate of www can lie below it. Hence w=1w = 1w=1, the orbit of zzz reaches 111, and a periodic point whose orbit reaches 111 is itself 111.

Note that only descent is needed, never convergence. That is what makes the threshold cheap to raise.

Preamble
import Mathlib
import Definitions.Def_syracuseStep
Formal statement
theorem syracuse_no_cycle_below_330750 (z a : ℕ) (hz : 0 < z) (ha : 0 < a) (hle : z ≤ 330749)
    (hcyc : syracuseStep^[a] z = z) : z = 1 := by sorry
Source
Collatz mission https://prove2.me/missions/2f34a49f-2016-4de2-9662-fcd1cc96cc67; from syracuse_descends_below_330750 and syracuse_periodic_reaches_one (a46524f0-afd4-4232-b74a-8a95d7ab31a5). Supersedes syracuse_no_cycle_below_99781 (bb9842e2-a1a4-46c0-be27-ea9e7d8a90a5).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me