Erdős problem 730 · problems.science

Are there infinitely many pairs of integers $n < m$ such that $\binom{2n}{n}$ and $\binom{2m}{m}$ have the same set of prime divisors?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/730.lean

Formal Conjectures

FormalConjectures/ErdosProblems/730.leanErdos730.erdos_7301 lineExact file

1True ↔ Erdos730.S.Infinite

OpenStatement only, no proofformal statement reference

Proof manifests naming this Problem

William Blair Lean proofswilliamjblair:Erdos730.audit_unitBand_complement_iff
William Blair Lean proofswilliamjblair:Erdos730.audit_unitBand_slack_ge_iff
William Blair Lean proofswilliamjblair:Erdos730.audit_unitBandEnvelope_iff
William Blair Lean proofswilliamjblair:Erdos730.ConsecutiveTransition.consecutive_primeFactors_eq_iff_transitionConditions
William Blair Lean proofswilliamjblair:Erdos730.ConsecutiveTransition.exists_obstruction_of_primeFactors_ne
William Blair Lean proofswilliamjblair:Erdos730.cutoff_lt_of_unitBand_maximal
William Blair Lean proofswilliamjblair:Erdos730.densityBudget_final_lt
William Blair Lean proofswilliamjblair:Erdos730.dyadicThresholdBase_strictMono_step
William Blair Lean proofswilliamjblair:Erdos730.eight_mul_sq_le_succ_cube
William Blair Lean proofswilliamjblair:Erdos730.endpoint_payment_identity
William Blair Lean proofswilliamjblair:Erdos730.endpoint_payment_lt_one_percent
William Blair Lean proofswilliamjblair:Erdos730.endpoint_powered_threshold_certificate
William Blair Lean proofswilliamjblair:Erdos730.finite_geometric_prime_power_tail
William Blair Lean proofswilliamjblair:Erdos730.finite_prime_power_pair_count
William Blair Lean proofswilliamjblair:Erdos730.finite_reciprocal_square_tail
William Blair Lean proofswilliamjblair:Erdos730.finite_reciprocal_tail_from_root_envelopes
William Blair Lean proofswilliamjblair:Erdos730.FirstPowerRoutes.first_power_fixed_upper_slope
William Blair Lean proofswilliamjblair:Erdos730.FirstPowerRoutes.improved_higher_power_ceiling_lt_three_tenths
William Blair Lean proofswilliamjblair:Erdos730.FirstPowerRoutes.normalized_block_cover_six_fifths
William Blair Lean proofswilliamjblair:Erdos730.FirstPowerRoutes.q_top_low_digit_large
William Blair Lean proofswilliamjblair:Erdos730.FirstPowerRoutes.q_top_small_cofactor_of_square_lt
William Blair Lean proofswilliamjblair:Erdos730.FirstPowerRoutes.q_top_two_digit_large
William Blair Lean proofswilliamjblair:Erdos730.FirstPowerRoutes.remaining_first_power_budget
William Blair Lean proofswilliamjblair:Erdos730.FirstPowerRoutes.s_top_low_digit_large
William Blair Lean proofswilliamjblair:Erdos730.FirstPowerRoutes.s_top_small_cofactor_of_square_lt
William Blair Lean proofswilliamjblair:Erdos730.FirstPowerRoutes.s_top_two_digit_large
William Blair Lean proofswilliamjblair:Erdos730.FullDensityCore.branches_pairwise_coprime
William Blair Lean proofswilliamjblair:Erdos730.FullDensityCore.product_identity
William Blair Lean proofswilliamjblair:Erdos730.FullDensityCore.switching_allowed_class_count_certificate
William Blair Lean proofswilliamjblair:Erdos730.FullDensityTheorem.pairSet_infinite
William Blair Lean proofswilliamjblair:Erdos730.halfBand_endpoint_payment_lt_one_percent
William Blair Lean proofswilliamjblair:Erdos730.halfBand_endpoint_powered_threshold_certificate
William Blair Lean proofswilliamjblair:Erdos730.halfBandEnvelope_forces_high_exponent
William Blair Lean proofswilliamjblair:Erdos730.halfBandEnvelope_prime_power_clearance
William Blair Lean proofswilliamjblair:Erdos730.halfDigitParity_probabilityError
William Blair Lean proofswilliamjblair:Erdos730.higherPrimePowerPairs_card_le
William Blair Lean proofswilliamjblair:Erdos730.KummerTransition.not_dvd_centralBinom_iff_lowerHalfDigits
William Blair Lean proofswilliamjblair:Erdos730.nearEnvelope_forces_high_exponent
William Blair Lean proofswilliamjblair:Erdos730.nearEnvelope_prime_power_clearance
William Blair Lean proofswilliamjblair:Erdos730.ObstructionMaps.PhiP_root_progression
William Blair Lean proofswilliamjblair:Erdos730.ObstructionMaps.PhiQ_root_progression
William Blair Lean proofswilliamjblair:Erdos730.ObstructionMaps.PhiR_root_progression
William Blair Lean proofswilliamjblair:Erdos730.ObstructionMaps.PhiS_root_progression
William Blair Lean proofswilliamjblair:Erdos730.ObstructionMaps.prime_dvd_residual_support
William Blair Lean proofswilliamjblair:Erdos730.padicBranchAllowedCount_le
William Blair Lean proofswilliamjblair:Erdos730.padicBranchMap_bijective
William Blair Lean proofswilliamjblair:Erdos730.powered_threshold_of_halfBand_maximal
William Blair Lean proofswilliamjblair:Erdos730.powered_threshold_of_near_maximal
William Blair Lean proofswilliamjblair:Erdos730.restrictedDigitBox_card
William Blair Lean proofswilliamjblair:Erdos730.tendsto_higherPrimePowerPairs_card_div
William Blair Lean proofswilliamjblair:Erdos730.tendsto_tsum_higherPower_of_dominated
William Blair Lean proofswilliamjblair:Erdos730.unitBand_endpoint_cuberoot_floor_certificate
William Blair Lean proofswilliamjblair:Erdos730.unitBand_endpoint_payment_identity
William Blair Lean proofswilliamjblair:Erdos730.unitBand_endpoint_payment_lt_one_percent
William Blair Lean proofswilliamjblair:Erdos730.unitBand_endpoint_payment_margin
William Blair Lean proofswilliamjblair:Erdos730.unitBand_endpoint_sqrt_floor_certificate
William Blair Lean proofswilliamjblair:Erdos730.unitBand_endpoint_threshold_certificate
William Blair Lean proofswilliamjblair:Erdos730.unitBandDyadicThresholdBase_strictMono_step
William Blair Lean proofswilliamjblair:Erdos730.unitBandEnvelope_forces_high_exponent
William Blair Lean proofswilliamjblair:Erdos730.unitBandEnvelope_prime_power_clearance
William Blair Lean proofswilliamjblair:Erdos730.UnitRangeBlock.higher_prime_power_payment_ceiling_lt_half
William Blair Lean proofswilliamjblair:Erdos730.UnitRangeBlock.normalized_block_cover_cross_bound
William Blair Lean proofswilliamjblair:Erdos730.UnitRangeBlock.quadratic_block_difference_dvd_sq
William Blair Lean proofswilliamjblair:Erdos730.UnitRangeBlock.quadratic_block_expansion

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

AI standalone
Erdős AI contributions wiki · 24 Jun, 2026
Machine
GPT-5.5 Pro
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science