Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

No nontrivial Syracuse cycle contains a value below 99781

Proved
syracuse_no_cycle_below_99781

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≤99780z \le 99780z≤99780 and Ta(z)=zT^a(z) = zTa(z)=z for some a≥1a \ge 1a≥1, then z=1z = 1z=1.

The return time aaa is arbitrary — no minimality is assumed — so the statement says that the only Syracuse cycle meeting the interval [1,99780][1, 99780][1,99780] is the trivial cycle {1}\{1\}{1}.

It follows from the finite verification that every odd number below 997819978199781 reaches 111, together with the observation that a periodic point of TTT whose orbit reaches 111 must itself be 111, since T(1)=1T(1) = 1T(1)=1 is absorbing. This raises the small-value threshold from the previously established bound of 271132711327113, and is the input that lets the margin criterion exclude every cycle of period at most 970970970.

Preamble
import Mathlib
import Definitions.Def_syracuseStep
Formal statement
theorem syracuse_no_cycle_below_99781 (z a : ℕ) (hz : 0 < z) (ha : 0 < a) (hle : z ≤ 99780)
    (hcyc : syracuseStep^[a] z = z) : z = 1 := by sorry
Source
Collatz mission https://prove2.me/missions/2f34a49f-2016-4de2-9662-fcd1cc96cc67; extension of syracuse_no_cycle_below_27114 (f56b97a4-527b-4005-8f1a-4f6e2f3250eb), via syracuse_reaches_one_below_99781 and syracuse_periodic_reaches_one (a46524f0-afd4-4232-b74a-8a95d7ab31a5).

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