The Agoh–Giuga conjecture: a congruence that detects primes
Difficulty 69.5: open since 1950, with a counterexample forced to be both a Carmichael and a Giuga number of at least 13,800 digits, but no argument that the two conditions are incompatible; a sibling of Lehmer's problem (72), slightly lower because the structure of a counterexample is sharper. Application value 3.2: a primality characterization whose false positives are the Carmichael numbers that practical tests already handle. Leverage 8: isolated.
The problem
Does adding the (n−1)-th powers of 1 through n−1 and getting −1 mod n happen only for primes?
- 1Primes pass the power-sum test
- 2Does any composite number pass?
- 3A passer would need 13,800+ digits
- 4None known, none excluded
Modular arithmetic. "" means that and leave the same remainder on division by (in Python, ). "" means the remainder is .
Path to understanding
foundations → problemThe research entries this problem rests on, in the order to read them. Each links to its explainer.
- Start with
- Step 2
- Harmonic analysisTheory
- Step 3
- Then
- The Agoh–Giuga conjecture: a congruence that detects primesThe problem
State of the art
Borwein, Borwein, Borwein and Girgensohn (1996) showed a composite counterexample must be both a Carmichael number and a Giuga number, and would have at least 13,800 digits. Sorini (2001), an Italian working paper whose title describes a heuristic method (Quaderni di Economia, Matematica e Statistica, Urbino), is cited for raising this to about ; it is not refereed, so the 13,800-digit bound is the safe one to quote. Giuga numbers satisfy for every prime ; thirteen are known (the first is , the twelfth has 34 digits), all even, and an odd Giuga number would need at least 14 prime factors. The corpus states the equivalence of the two formulations as a known result (), but its Lean proof is still left as .
Realistic applications
None directly. It belongs to the family of primality characterizations whose false positives (Carmichael-type numbers) are exactly what cryptographic primality tests are designed to avoid.
What counts as solved
A Lean proof of agoh_giuga.variants.giuga (the Bernoulli form agoh_giuga would then follow once the corpus' equivalence statement is also proved in Lean), or an explicit composite with , which the kernel can check.
How it gets verified
Lean proofA formal proof checked by Lean 4 / Mathlib.
Statement: AgohGiuga.agoh_giuga.variants.giuga (and agoh_giuga for the Bernoulli form, using Mathlib's bernoulli') in formal-conjectures. Mathlib supplies Nat.Prime, Finset.Ioo and Bernoulli numbers (NumberTheory.Bernoulli); the Giuga-number definitions are in the corpus file itself, which also states the equivalence of the two formulations but leaves its proof as sorry, so a proof of one form does not yet give the other in Lean. A counterexample is a single composite that Lean can check by evaluating the power sum modulo (kernel-checkable with fast modular exponentiation lemmas). A proof must cover all . Judge with Comparator against the pinned statement.
Claims under verification
+ add a claimNo claimed results on the Verification board for this problem yet.
Where the work is
The structure theory (Carmichael and Giuga conditions) is the main content; search effort has already pushed the size bound far.
Bottlenecks
ranked by votes- #1TheoryExcluding Carmichael-Giuga numbers
A counterexample must satisfy both conditions simultaneously; no argument shows the two sets are disjoint beyond the data.
Community grades
Sign in to add your own grade.
Connected problems
- This problem is related to Lehmer's totient problem: is there a composite n with φ(n) dividing n − 1?Both ask whether a congruence characterizes primes, and any counterexample to either would have to be a Carmichael number.