Source labels openChecked July 26, 2026

Agrawal's conjecture

Agrawal's Primality Conjecture.*

Mathematical statement

Agrawal's Primality Conjecture.*

Does the congruence $(X-1)^n \equiv X^n - 1 \pmod{n, X^r-1}$ imply $n$ is prime (with a specific exception for $n^2 \equiv 1 \pmod{r}$ )?

While the "if" direction is a known theorem, the "only if" direction remains a conjecture.

Statement source: Wikipedia statement material

Statement terms: CC-BY-SA-4.0

Attributed source material. Reuse must follow the linked attribution and share-alike terms.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

agrawal_conjecture

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem agrawal_conjecture :  answer(sorry) ↔    ∀ (n r : ℕ), n > 1 → r > 0 → n.gcd r = 1 →      let R := Polynomial (ZMod n)      let X : R := Polynomial.X      let I : Ideal R := Ideal.span ({X^r - 1} : Set R)      Ideal.Quotient.mk I ((X - 1)^n) = Ideal.Quotient.mk I (X^n - 1) →      (n.Prime ∨ (n^2 : ZMod r) = 1) := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization Wikipediabackground AIM Mathbackground Paperbackground