A number is called "cyclic" if it has no structural overlap between its size and its internal symmetries (technically, if it shares no common factors with a count of its divisors' properties). A "Sophie Germain cyclic" number is one where both the number itself and twice the number plus one are cyclic in this sense. These numbers are named after the mathematician Sophie Germain, and they arise naturally in number theory and the study of group theory. Researchers have been counting how many such numbers appear in various ranges, and a mathematician named Cohen conjectured in recent work that this counting function behaves in a particularly tidy way: specifically, that the count up to a sum of two numbers never exceeds the sum of the individual counts. Mathematicians call this property "subadditivity," and it is a natural and appealing property for counting functions to have.
Cohen tested his conjecture exhaustively on all pairs of numbers up to one million without finding any violation, which gave reasonable confidence it might be true. The paper under review disproves the conjecture by finding a specific small counterexample: using the numbers 31 and 3928, the count of Sophie Germain cyclic numbers up to their sum (3959) turns out to be 697, while the sum of the separate counts is only 696. This is a clean, concrete refutation of the conjecture, showing that the counting function occasionally "bunches up" in a way that violates the subadditivity property.
What makes this paper noteworthy beyond the result itself is how the authors verified it. Rather than relying only on hand calculation or standard computer checks, they confirmed the argument using Lean 4, a formal proof assistant that checks mathematical reasoning at the level of strict logical rules. This means the counterexample has essentially been certified to be correct with machine-level rigor. The result is a good reminder that even well-tested conjectures, checked across millions of cases, can fail just beyond the tested range, and it demonstrates the growing usefulness of formal verification tools in modern mathematics.