FormalConjectures/Wikipedia/Agrawal.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

2 declarations, 2 contain sorry, 0 declared as axioms

Agrawal's conjecture

Agrawal's conjecture is a stronger version of the theorem that forms the basis of the AKS primality test. If true, it would significantly improve the efficiency of primality testing.

The conjecture states that for coprime $n$ and $r$, if the polynomial congruence $(X-1)^n \equiv X^n-1 \pmod{n, X^r-1}$ holds, then $n$ is either prime or $n^2 \equiv 1 \pmod{r}$.

References:

Imports (1)
  1. theorem AgrawalConjecture.agrawal_conjecture Agrawal's Primality Conjecture sorry line 52 source

    Source documentation

    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.

    depends on sorry what this means

    Statement uses: Iff, True, Nat, GT.gt, OfNat.ofNat, Eq, Nat.gcd, Polynomial, ZMod, Polynomial.X, Ideal, Ideal.span, Singleton.singleton, Set, HSub.hSub, HPow.hPow, HasQuotient.Quotient, RingHom, Ideal.Quotient.mk, Or and 1 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem agrawal_conjecture :
  answer(sorry) ↔
    ∀ (n r : ℕ), n > 1 → r > 0 → n.gcd r = 1 →
      let R := Polynomial (ZMod n)
…
  2. theorem AgrawalConjecture.agrawal_conjecture.variants.popovych Roman B sorry line 70 source

    Source documentation

    Roman B. Popovych Conjecture. A stronger version of Agrawal's conjecture, which also considers the congruence $(X+2)^n \equiv X^n + 2 \pmod{n, X^r-1}$. If both congruences hold, then $n$ is either prime or $n^2 \equiv 1 \pmod{r}$. This variant was proposed by Roman B. Popovych in 2018.

    depends on sorry what this means

    Statement uses: Nat, GT.gt, OfNat.ofNat, Eq, Nat.gcd, Polynomial, ZMod, Polynomial.X, Ideal, Ideal.span, Singleton.singleton, Set, HSub.hSub, HPow.hPow, HasQuotient.Quotient, RingHom, Ideal.Quotient.mk, HAdd.hAdd, Or, Nat.Prime

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem agrawal_conjecture.variants.popovych :
  ∀ (n r : ℕ), n > 1 → r > 0 → n.gcd r = 1 →
    let R := Polynomial (ZMod n)
…