🔢 mathematics

A counterexample to a subadditivity conjecture of Cohen for Sophie Germain cyclic numbers

This paper disproves Cohen's subadditivity conjecture for Sophie Germain cyclic numbers by presenting a specific counterexample at $m=31$ and $n=3928$ , a result that has been formally verified by the Lean 4 kernel.

Original authors: Josué Alexander Ibarra

Published 2026-07-14

📖 3 min read🧠 Deep dive

CC BY 4.0

Original authors: Josué Alexander Ibarra

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you're organizing a massive party where the guest list is made up of special numbers called "cyclic numbers." These are the VIPs of the number world: they have a unique superpower where every group of that size can be arranged in a perfect circle without any chaos. There's an even cooler club called "Sophie Germain cyclic numbers." To get in, a number has to be a VIP itself, and its "plus-one" twin (specifically, $2n + 1$ ) also has to be a VIP.

For years, a mathematician named Cohen had a hunch about how these VIPs spread out. He thought they followed a rule called subadditivity. Think of it like a "no double-dipping" rule for counting guests. The rule says: if you count how many VIPs are in a small group of $m$ people and add that to the count of VIPs in a larger group of $n$ people, the total should always be at least as big as the number of VIPs you'd find if you just looked at a single, combined group of $m + n$ people. In other words, you can't find a denser crowd of VIPs in a random slice of the party than you do in the very first slice starting from the beginning.

Cohen checked this rule for millions of numbers (up to $10^6$ ) and couldn't find a single crack in the armor. He was so confident he wrote it down as Conjecture 66.

But here comes the plot twist: The rule is broken.

A mathematician named Josué Alexander Ibarra found a specific spot where the party gets surprisingly crowded, breaking the "no double-dipping" rule. He looked at two specific numbers: 31 and 3928.

If you count the VIPs in the first 31 numbers, you find exactly 10 of them.
If you count the VIPs in the first 3928 numbers, you get some big number (let's call it $X$ ).
According to the old rule, the total VIPs in the first 3959 numbers (which is $31 + 3928$ ) should be less than or equal to $10 + X$ .

But when Ibarra did the math, he found 697 VIPs in the first 3959 numbers.
When he added the VIPs from the first 31 ($10$) and the first 3928 ( $X$ ), he got 696.

697 is greater than 696.

The rule failed. The VIPs in the middle of the party (specifically in the stretch from 3929 to 3959) were so dense that they packed in 11 new guests, while the very first stretch of the party (1 to 31) only had 10. It's like finding a secret VIP lounge in the middle of the room that's more crowded than the entrance hall.

This isn't just a guess or a simulation; the paper proves it with absolute certainty. The author didn't just run a program and hope for the best; they used a formal proof system called Lean 4, which acts like a super-strict referee that checks every single logical step to ensure no mistakes were made. The referee confirmed that the counterexample is real and that the old rule is definitely false.

Interestingly, Cohen himself later admitted that his earlier search missed this because of a tiny error in his computer code. Now that the code is fixed and the counterexample is verified, we know for sure that the "no double-dipping" rule for these special numbers doesn't hold up. It turns out that sometimes, the middle of the party is just more exciting than the beginning.

Technical Summary: A Counterexample to a Subadditivity Conjecture of Cohen for Sophie Germain Cyclic Numbers

Problem Statement
The paper addresses a conjecture proposed by J. E. Cohen regarding the distribution of "Sophie Germain cyclic" integers. An integer $n \ge 1$ is defined as cyclic if $\gcd(n, \phi(n)) = 1$ (equivalently, if every group of order $n$ is cyclic). An integer is Sophie Germain cyclic if both $n$ and $2n+1$ are cyclic. Let $C_\sigma(N)$ denote the counting function for these integers in the interval $[1, N]$ .

Cohen conjectured that $C_\sigma$ is subadditive, specifically that for all integers $1 \le m \le n$ :
$C_\sigma(m + n) \le C_\sigma(m) + C_\sigma(n)$
This is the cyclic analog of the second Hardy–Littlewood conjecture concerning the prime counting function $\pi$ . While Cohen verified this inequality for $m, n \le 10^6$ without finding a counterexample, he left the general validity open.

Methodology
The author employs a direct computational and logical approach to disprove the conjecture:

Targeted Search: Instead of a broad search, the author identifies a specific window $(m, m+n]$ where the density of Sophie Germain cyclic integers exceeds the density in the initial segment $[1, m]$ .
Explicit Enumeration: The proof relies on the finite enumeration of Sophie Germain cyclic integers within specific ranges. The author calculates the exact count for $m=31$ and identifies a window of length 31 starting at $n=3928$ (i.e., the interval $(3928, 3959]$ ).
Formal Verification: The results are verified using the Lean 4 proof assistant over the mathlib library. The formalization defines cyclic numbers via Nat.Coprime n (Nat.totient n) and verifies the counting function $C_\sigma$ . Crucially, the proof is checked by the Lean kernel itself, relying only on standard axioms (propext, Classical.choice, Quot.sound) and avoiding native decision procedures (native_decide), ensuring the result is a theorem rather than a computational artifact.

Key Results
The paper provides a concrete counterexample to Cohen's Conjecture 66:

Parameters: $m = 31$ and $n = 3928$ .
Counts:
- $C_\sigma(31) = 10$ (The integers are 1, 2, 3, 5, 7, 11, 15, 17, 23, 29).
- The interval $(3928, 3959]$ contains 11 Sophie Germain cyclic integers: 3929, 3931, 3935, 3941, 3943, 3945, 3947, 3949, 3953, 3957, 3959.
- Consequently, $C_\sigma(3959) = C_\sigma(3928) + 11$ .
Inequality Violation:
$C_\sigma(3959) = C_\sigma(3928) + 11 > C_\sigma(3928) + 10 = C_\sigma(3928) + C_\sigma(31)$
Thus, $C_\sigma(31 + 3928) > C_\sigma(31) + C_\sigma(3928)$ , disproving the subadditivity claim.

The author notes that the specific value of $C_\sigma(3928)$ is irrelevant to the proof; the disproof relies solely on the fact that the window $(3928, 3959]$ is denser than $[1, 31]$ .

Significance and Claims
The paper claims the following significance:

Resolution of an Open Problem: It definitively proves that Cohen's Conjecture 66 is false, closing a question left open after a search up to $10^6$ .
Correction of Previous Work: The author notes that Cohen's failure to find a counterexample in his original search was due to an error in his computer code, a fact confirmed by Cohen himself following this paper's findings.
Theoretical Consistency: The falsity of the subadditivity conjecture for Sophie Germain cyclic numbers aligns with the general belief that the analogous conjecture for primes (Hardy–Littlewood) is also false and incompatible with the prime $k$ -tuples conjecture.
Formal Rigor: The result is distinguished by its formal verification in Lean 4, providing a kernel-checked proof that the counterexample lies within the range previously searched ( $m, n \le 10^6$ ).

The paper concludes that counterexamples of this nature are not rare, but this specific instance is notable for its location within the range of Cohen's original (erroneous) search.

Technical Summary: A Counterexample to a Subadditivity Conjecture of Cohen for Sophie Germain Cyclic Numbers

More like this