Let $[1,\dots ,n]$ denote the least common multiple of $\{1,\dots ,n\}$. Is it true that, for all $k\ge 1$,$$[1,\dots ,p_{k+1}-1]<p_k[1,\dots ,p_k]?$$

lcm(1..p_{k+1}-1) < p_k*lcm(1..p_k) <=> P(k) := prod of bases q of prime powers q^m (m>=2) in the gap (p_k,p_{k+1}) is < p_k.

Since no prime lies in (p_k,p_{k+1}), primes <= p_{k+1}-1 equal p_1..p_k, so the lcm ratio is exactly prod over prime powers q^m (m>=2) in the gap of q. Conjecture <=> that product < p_k. Tightest case k=4: gap (7,11) has 8=2^3,9=3^2, product 6<7. A violation needs two prime squares q1^2,q2^2 in one gap with q1*q2>=p_k, forcing gap length >= ~2*sqrt(p_k).

depends on (the wall): a fully unconditional proof still needs effective prime-gap-vs-prime-square bounds (BHP p^0.525 exceeds sqrt(p), so does not trivially close it)

docs/erdos-attack/458/verify458.py: 0 counterexamples for all prime gaps to p_k~3.6e8 (re-checked to 5e6); exact integer arithmetic.

#458 superseded finite-range proof attempt: the reduction to prime-power bases is useful, but the claimed BHP-driven unconditional range was overstrong and is replaced by att_1f15d7e468458e15.

The reduction #458 <=> P(k) := product of bases q of prime powers q^m, m>=2, in the gap (p_k,p_{k+1}) is still retained. The attempted finite-range close via BHP and a square-gap crossover was too strong as a frontier claim. The corrected state is narrower: checked two-base exclusions, a source-backed finite Legendre bridge excluding the two-square obstruction for p<=4.97025e27, and a separate mixed-cluster residual. See att_1f15d7e468458e15 and docs/erdos-attack/458/NOTE.md.

depends on (the wall): Bertrand (Mathlib); BHP crossover note is retained only as a heuristic route, not an accepted finite-range proof; residual: mixed clusters or a named external theorem strong enough to exclude them

Superseded by lean/Vela/Erdos458.lean, docs/erdos-attack/458/NOTE.md, and the 2026-06-04 #458 research audit.

#458 superseded cross-model finite-range claim: the shared reduction and bounded searches were useful, but the claimed unconditional p<1.21e24 conclusion is not accepted frontier state.

The cross-model agreement correctly recovered the gap-product reduction, the tight gap (7,11), the five multi-base gaps seen in the bounded audit, and the two-square sufficient obstruction. It overpromoted conditional or heuristic square-gap reasoning into an unconditional finite-range statement. The corrected record is att_1f15d7e468458e15: #458 remains open, the two-square obstruction is source-backed excluded only through the finite Legendre bridge, and mixed clusters with at least three distinct bases remain residual.

depends on (the wall): BHP and Firoozbakht remain candidate routes, not accepted proof inputs; mixed clusters remain a residual unless separately excluded; the live problem remains open

Superseded by the 2026-06-04 Vela audit and checked Lean bridge.

Erdos #458 remains open: Vela now has a named Lean target, checked gap-support lemmas, exact prime-power gap verification through 10^15 with no counterexample, finite square/two-cube obstruction bridges, and narrowed mixed-cluster residues.

The Lean module lean/Vela/Erdos458.lean names Erdos458Statement and the expected equivalent GapProductStatement, and checks finite-prefix lcm divisibility primitives, finite-lcm factorization support, certified MaxPowLE-to-lcmUpto factorization equality, the abstract and lcm-stated single-base exponent-jump/factor identities, the all-bases contribution-pair decomposition into single-base exponent-jump sets, the corresponding gapBaseProduct formula, the Bertrand short-gap consequence for consecutive primes, repeated-base exclusion in actual consecutive-prime gaps, the finite image-product rewrite for distinct contributing bases, the per-contribution base bound q<p, the theorem that GapInequality holds when the distinct contributing-base image has cardinality at most one, the combined theorem that any two contributions not both squares have base product below p for p>=33, the theorem that three higher-power contributions have base product below p for p>=2049 unless all three are cubes, the theorem that one square plus two ordered higher-power contributions has base product below p for p>2^41 outside the low higher-exponent pairs (3,3), (3,4), (3,5), (3,6), and (4,4), the two-square obstruction, the prime-between-squares reformulation of that obstruction, the theorem that a finite LegendreUpTo N verification rules out two-square obstructions for lower primes p<=N^2, and the theorem that a finite CubePrimesUpTo C verification rules out any two distinct cube contributions for lower primes satisfying 2p<=C. Sorenson and Webster's 2025 computation verifies Oppermann's conjecture, hence Legendre's conjecture, for n<=70,500,000,000,000; consumed through the checked Vela bridge, this excludes the two-square obstruction for p<=4,970,250,000,000,000,000,000,000,000. Johnston, Sorenson, Thomas, and Webster's 2026 preprint reports primes between consecutive cubes for n^3<=1.649*10^40; consumed through the checked Vela bridge, this excludes any two-distinct-cube obstruction for p<=8,245,000,000,000,000,000,000,000,000,000,000,000,000. The public Erdős Problems page was checked on 2026-06-04 and still marks #458 open and falsifiable, with the square and small-prime obstructions explicitly named. The public forum check through 10^12 was reproduced and extended locally through prime powers below 10^15: 1962689 prime powers, 1962684 gaps with prime powers, five multi-base gaps, zero repeated-base gaps, zero counterexamples, and worst gap (7,11) with product 6<7. The final all-bases finite product equality lcmUpto (r-1) = lcmUpto p * gapBaseProduct p r is still not machine-checked. The residual mixed clusters are now one square plus exactly two higher powers in the low exponent pairs above, with (3,3) excluded inside the finite cube-check range when cube bases are distinct, one square plus at least three higher powers, at least two cube contributions beyond the finite cube-check range, or at least four higher powers.

depends on (the wall): final all-bases finite product equality lcmUpto (r-1) = lcmUpto p * gapBaseProduct p r remains unproved in Lean; universal proof still needs mixed-cluster exclusion or a named external theorem strong enough to supply it

cd lean && lake build Vela.Erdos458; cd lean && lake env lean --stdin #check factorization_finset_lcm_apply, lcmUpto_factorization_eq_sup, lcmUpto_factorization_eq_maxPowLE, lcmUpto_exponent_jumps_iff_exists_power_between, lcmUpto_singleBaseFactor_eq_prefixPowerRatio, contributionPairs_eq_primeBaseBiUnion_contributingExponents, gapBaseProduct_eq_primeBaseExponentProduct, two_square_contributions_contradict_legendre_up_to_lower_prime_bound, three_higher_power_contributions_product_lt_lower_prime_unless_triple_cubes, square_and_two_higher_contributions_product_lt_lower_prime_outside_low_pairs, and two_cube_contributions_contradict_cubePrimesUpTo_lower_prime_bound_of_ne; python3 docs/erdos-attack/458/verify_prime_power_gaps.py --limit 1000000000000000 --top 50 --out examples/erdos-problems/attack/erdos458-prime-power-gap-run-1e15-2026-06-04.v1.json; python3 -m json.tool on #458 audit artifacts.

#458 superseded obstruction-classification attempt: the sigma=sum 1/a_i filter is useful, but this record overclaimed complete classification and is replaced by att_1f15d7e468458e15.

The exponent-budget filter remains a useful necessary condition: if contributing powers are q_i^a_i, then by Bertrand the base product is < (2p)^sigma with sigma=sum_i 1/a_i, so a counterexample needs sigma > log(p)/log(2p). The previous claim that this yielded a complete verified obstruction map was too strong. Mixed clusters with at least three distinct bases remain a genuine residual unless excluded by a new argument or a named theorem. The corrected accepted state is the research audit att_1f15d7e468458e15, which records the checked two-base exclusions, the two-square obstruction, the finite Legendre bridge, and the local 10^15 audit.

Superseded by lean/Vela/Erdos458.lean and docs/erdos-attack/458/CLASSIFICATION-NOTE.md.