$\exists K \geq 2 \forall k \geq K, g (k) < L_{k} = lcm (1, \dots, k)$

Quoted from the source · Significance editor · 2026-10-01 §Theorem 1.1 (thm:main) · View source

Component dates

Preprint: 2026-09-26
Exposition: Not recorded
Formalization: 2026-10-01

Component dates (preprint / exposition / formalization). Formalization date from the artifact reported by the source. “Not recorded” means no dated source is recorded for that component. Preprint dates refer to the pinned manuscript version.

Reader summary

Claimed: Ethan Yang's paper and Lean repository claim the eventual strict bound g(k) < lcm(1,...,k). This is one sub-conjecture of Erdős #1095; the sharp growth and successive-ratio questions remain outside its scope.

Reader summary · Significance · 2026-10-01

What has been checked?

Significance inspected the public claim, pinned the repository and PDF, computed the manuscript hash, and checked the upstream CI status. Ethan approved the reading map's presentation.

Reader summary · Significance · 2026-10-01

Independent reruns: 0
Math assessments: 0
Written reviews: 0

Where is help needed?

No fresh independent Lean build, specialist mathematical review, complete source-chain audit, or paper-to-Lean correspondence audit is recorded. The upstream CI result and author approval do not supply those checks.

Reader summary · Significance · 2026-10-01

See 3 open checks →

Problem link

ErdősProblems.com #1095 · open the original problem page

Quoted from the source · Significance editor · 2026-10-01 · View source

Author involvement

Ethan Yang approved the reading map's presentation in a reply supplied to the maintainer. This public record carries that map's scope and review questions into the normal Significance record format. Approval concerns the description and publication of the map; no mathematical review or proof-correctness attestation is inferred. The timestamp records the approval entry, not the exact time of the reply. Private message text is withheld.

Record note · ethan yang · 2026-10-01

Start here · for reviewers

Main deduction

Modify L_k by adding small-prime factors and removing the top prime band, producing a modulus M with room for multipliers t. Lucas's criterion becomes forbidden residue conditions in three prime ranges. PNT bounds their density; truncated inclusion–exclusion with explicit CRT discrepancy produces a surviving t. Set n = Mt - 1 and use the least-witness definition to conclude the strict eventual lcm bound.

Paper §§2–5; Erdos1095/Main.lean · Check both witness inequalities and a single threshold for all sufficiently large k. · Significance’s interpretation · Significance editor · 2026-10-01

Risk points

The finite interval count must control the sum of CRT discrepancies over truncated intersections and the Bonferroni/factorial tail. Check that the chosen constants make the surviving main term exceed the error.
Paper §4 finite sieve lemma and §5 surviving multiplier · Significance’s interpretation · Significance editor · 2026-10-01
Check Lucas's digit conditions, the middle-prime lift from p to p², the top-band residue count, and every PNT estimate at the fixed proportional endpoints used in the construction.
Paper §§2–3; Arithmetic/ and Analytic/PNT.lean · Significance’s interpretation · Significance editor · 2026-10-01
The README reports two upstream Wiener sorry warnings outside the used dependency closure. An independent replay must inspect the actual final-theorem axiom report and confirm that dependency boundary.
verify.sh; AxiomAudit.lean; pinned PrimeNumberTheoremAnd dependency · Significance’s interpretation · Significance editor · 2026-10-01

Useful background

Elementary number theory, Lucas's theorem, the prime number theorem at fixed rescalings, inclusion–exclusion, the Chinese remainder theorem, and Lean dependency/axiom auditing for the formal checks.
Significance’s interpretation · Significance editor · 2026-10-01

Needs checking

Compare the paper's Theorem 1.1 and the exact Lean SourceTarget, explicit-witness target, and least-element definition. Record strict inequalities, all primes p <= k, and the common eventual threshold.
STATEMENT-CORRESPONDENCE.md; StatementAudit.lean; Erdos1095/Statement.lean · Significance’s interpretation · Significance editor · 2026-10-01
Suggest another focused check

Formalization handoff

A compact map for someone who wants to formalize this claim. It records preparation and open work, not a mathematical verdict.

Target: Erdos1095.erdos1095_main : Erdos1095.SourceTarget, preceded by the explicit-witness theorem erdos1095_target. Quoted from the source · Significance editor · 2026-10-01 · View source
System: Lean 4.27.0 and Mathlib 4.27.0 with pinned PrimeNumberTheoremAnd dependency. Quoted from the source · Significance editor · 2026-10-01 · View source
Work state: Artifact reported
Code: formalization repository · commit e06b3e658c48… · Lean/Mathlib 4.27.0

Paper/code correspondence: The repository documents a statement audit; an independent comparison of the paper theorem and Lean target remains open. Significance’s interpretation · Significance editor · 2026-10-01

Significance’s interpretation · Significance editor · 2026-10-01

Copy for sharing

Copy and paste this summary.

Ethan Yang's paper and Lean repository claim the eventual strict bound g(k)
< lcm(1,...,k). This is one sub-conjecture of Erdős #1095; the sharp growth
and successive-ratio questions remain outside its scope.

Checked: Significance inspected the public claim, pinned the repository and
PDF, computed the manuscript hash, and checked the upstream CI status. Ethan
approved the reading map's presentation.

Not checked: No fresh independent Lean build, specialist mathematical
review, complete source-chain audit, or paper-to-Lean correspondence audit
is recorded. The upstream CI result and author approval do not supply those
checks.

As of 2026-10-01T13:17:58Z (freshness: current)
Full record: https://hjyuh.github.io/significance/2026-ethanyang-erdos-1095/
Significance records evidence. It does not judge the mathematics.

Scope: Partial relative to Erdős #1095: the eventual strict lcm bound only. The sharp growth estimate for log g(k), successive-ratio conjectures, and a numerical eventual threshold are outside the submitted scope. Significance’s interpretation · Significance editor · 2026-10-01 §Scope · View source
Source: A least-common-multiple bound for the Erdős–Selfridge function (pinned PDF) · github-ethn-y-erdos-1095-e06b3e658c486b4aa16d0dcf738370fcd84fcd5c · retrieved 2026-10-01T13:17:58Z
sha256 7621e3c47277…

Evidence: 3 entries

Source inspection
ev-source-inspection

Public-source and version check only. This is not a mathematical review.

The public proof-claim thread, repository README, manuscript source, pinned PDF, and upstream Actions status were inspected. The PDF SHA-256 identifies the exact retrieved bytes. This is source inspection, not a specialist review of the proof.

Significance’s interpretation · Significance editor · 2026-10-01 · View source
Formal code published by the source
ev-lean-reported

Published by the source. Any independent rerun appears as a separate entry.

Upstream GitHub Actions reports a successful Verify Lean proof run for this commit. The README describes Lean/Mathlib 4.27.0, the pinned PNT dependency, and an expected axiom surface of propext, Classical.choice, and Quot.sound. No fresh independent replay is recorded here.

Open link @ e06b3e658c48… · Quoted from the source · Significance editor · 2026-10-01 · View source
Source inspection
ev-paper-ci-reported

Public-source and version check only. This is not a mathematical review.

Upstream GitHub Actions reports a successful Build paper run for the pinned commit. This concerns manuscript compilation and packaging.

Quoted from the source · Significance editor · 2026-10-01 · View source

Plain-language explanation

Seek a binomial coefficient with no prime factor at most k. The paper creates room below the lcm by changing its prime factors, then sieves a finite interval of multipliers to find a candidate. This record keeps the partial scope visible and gives separate paper, correspondence, and build checks. Its editorial map was prepared with GPT-6.1 Sol assistance.

Explanation · Significance

Limits of this record

This record does not issue a whole-paper correctness judgement.
Open invitations identify work not yet represented by a completed evidence entry.
No independent reproduction or mathematical assessment is represented unless an evidence entry above says otherwise.

Source inspection

Formal code published by the source

Source inspection