bibkey: ordowski2018a133907 authors: Thomas Ordowski year: 2018 title: “OEIS A133907, least prime p with binomial(n+p,p) ≡ 1 (mod p), with the power-sum least-prime conjecture” doi: null url: https://oeis.org/A133907 claim: “%N Least prime number p such that binomial(n+p, p) mod p = 1. %C Conjecture: a(n) is the smallest prime p such that Sum_{k=1..n} k^(p-1) == n (mod p). Thus a(n) >= A317358(n). - Thomas Ordowski, Jul 29 2018” strata_touched:

• D5/S3/Arith/Congruence/OrdowskiBinomialPowerSumLeastPrime license: citation-only triage: anchor

OEIS A133907

Thomas Ordowski’s 2018 conjecture identifies the least prime in the binomial definition with the least prime satisfying the power-sum congruence. The entry author is Hieronymus Fischer, whose AUTHOR line is dated October 20, 2007. The year and authors field identify the conjecture, rather than the entry’s initial publication.

For every natural n > 0, the Lean definition is a n = sInf {p : Nat | p.Prime ∧ (n+p).choose p ≡ 1 [MOD p]}. The theorem states that this value is the least prime p satisfying (∑ k ∈ Finset.Icc 1 n, k^(p-1)) ≡ n [MOD p]. Both predicates, for prime p, are equivalent to p ∣ n / p, where division is natural-number floor division. Lucas supplies the binomial residue; Fermat and the number of multiples of p supply the power-sum residue.

Only the sentence beginning “Conjecture:” is settled. The quoted “Thus a(n) >= A317358(n)” clause is a consequence, not claimed separately. The unsigned floor-division comment is related context and is not a separate public theorem or resolution claim.

Verified locator

• URL: https://oeis.org/A133907

Locator reading dated 2026-09-15:

%N Least prime number p such that binomial(n+p, p) mod p = 1.
%O 1,1
%A _Hieronymus Fischer_, Oct 20 2007
%C Conjecture: a(n) is the smallest prime p such that Sum_{k=1..n} k^(p-1) == n (mod p). Thus a(n) >= A317358(n). - _Thomas Ordowski_, Jul 29 2018
%C Also the least prime number p such that p divides floor(n/p) or p > n.

No literature proof was found in the searched surfaces recorded in the A133907 problem dossier; this is a scoped search result, not an exhaustive historical-priority claim.