What does this research mean for the field?

The Erdős Square-Free Binomial Coefficient Conjecture, which asserts that the central binomial coefficient C(2n, n) is never square-free for n > 4, is completely and formally verified using the Lean 4 interactive theorem prover. Novelty: ClaimNovelty.CONFIRMATORY. Consensus alignment: ConsensusAlignment.SUPPORTS_CONSENSUS.

What question did this study set out to answer?

Investigate and formally verify the Erdős Square-Free Binomial Coefficient Conjecture, confirming whether the central binomial coefficient C(2n, n) is never square-free for any integer n > 4.

August 29, 2026Open Access

On the Square Factors of Central Binomial Coefficients

View Full Paper

Ask AI

Bookmark

Authors

CNCharles EDOU NZE

Discussion

Member takes

Implication

Theoretical analysis demonstrates non-square-freeness in central binomial coefficients for integers n > 4, verifying the Erdős conjecture through analytic number theory and interactive proofs.

Key Points

Investigate and formally verify the Erdős Square-Free Binomial Coefficient Conjecture, confirming whether the central binomial coefficient C(2n, n) is never square-free for any integer n > 4.
Synthesized Kummer's base-p carry theorem with p-adic valuations and the Granville-Ramaré sieve framework across medium-range primes √(2n) < p ≤ √(8n/3).
Conducted 100% machine-checked formal verification of square-free predicates and explicit prime-square certificates in Lean 4 with 0 axioms, 0 linter warnings, and 0 sorry placeholders.
Determined the complete exception set of square-free central binomial coefficients to be exclusively n ∈ {1, 2, 4}, producing C(2,1)=2, C(4,2)=6, and C(8,4)=70.
Confirmed that for every integer n > 4, prime contributions leave an unbridgeable deficit unless medium-range primes supply square factors p² ∣ C(2n, n), with explicit witnesses such as 3² ∣ C(6,3) and 2² ∣ C(10,5).

Cite This Study

Charles EDOU NZE (2026) studied this question.

synapsesocial.com/papers/6a92be7b8e5d7d1fc0c12385 https://doi.org/10.5281/zenodo.22133077

View Full Paper

Ask AI

Bookmark

Implication

Theoretical analysis demonstrates non-square-freeness in central binomial coefficients for integers n > 4, verifying the Erdős conjecture through analytic number theory and interactive proofs.

On the Square Factors of Central Binomial Coefficients

Discussion

Member takes

Implication

Key Points

Cite This Study

On the Square Factors of Central Binomial Coefficients

Discussion

Member takes

Implication

Key Points

Cite This Study

Also Consider

Also Consider