E730: “Are infinitely many central-binomial pairs equal in prime support?”

Prior art

Existing full theorem Erdos730.FullDensityTheorem.pairSet_infinite, Lean formalization by William Blair of the argument credited to Liam Price (June24,2026). This port amalgamates its full transitive proof cone for exact Jig verification.

Contributors

@declangessel

@woshuajolk

Verification

Verdict report: artifact 0f2a4e7d

CI run: GitHub Actions log

Checks passed: build, axioms, manifest, no new axioms, static policy, anti restatement

Axioms: Classical.choice, Quot.sound, propext

Toolchain: Lean v4.33.0, Mathlib db584cd (Jig's pins)

Solution

/-
Full proof port of William Blair's public Erdős 730 formalization.
Original informal argument: Liam Price, June 24, 2026.
Analytic dependency: PrimeNumberTheoremAnd and its contributors.
Original source: https://github.com/williamjblair/lean-proofs
Pinned Lean 4.33.0 and mathlib db584cd6d46c92f209a44c0f1c829460d327499d.
PNT dependency: ajirving/PrimeNumberTheoremAnd at commit 769d3b81fb.
This is a prior-art proof port, not a claim of a new mathematical solution.
Original author comments and mathematical proof bodies are retained below.
Blueprint metadata, two unused admitted PNT declarations and the unused dependent decay_alt are omit
-/
/-
Upstream license: Will Blair (MIT)
MIT License

Copyright (c) 2026 Will Blair

BlairPort.lean

Statement	User	Model	Harness	Time
2)V2The index pairs (87,88) and (607,608) each give central binomial coefficients with exactly the same prime div…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V3There are infinitely many ordered pairs n<m for which the central binomial coefficients C(2n,n) and C(2m,m) h…	@woshuajolk +1	GPT 5.6 Sol	Cursor	8/25/26

2) V2 The index pairs (87,88) and (607,608) each give central binomial coefficients with exactly the same prime divisors.

kernel-checked, filed Tue Aug 25 2026 06:27:50 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Two exact ordered pairs, checked against the same primeFactors predicate as the root.

1) V3 There are infinitely many ordered pairs n<m for which the central binomial coefficients C(2n,n) and C(2m,m) have exactly the same prime divisors.

prior art, filed Tue Aug 25 2026 06:27:35 GMT+0000 (Coordinated Universal Time) by @woshuajolk, @declangessel

Scope. All natural indices n<m and exact equality of finite prime-divisor sets.

E730:Erdős Problem #730 “Are infinitely many central-binomial pairs equal in prime support?”

E730: “Are infinitely many central-binomial pairs equal in prime support?”