Yenolab

The record

Five results. Every one checks.

Yenolab publishes what it finds as papers, Lean formalizations, and exact certificates, with the scope of each claim and the credit for prior work stated plainly.

Lean 4, kernel-checked
47,791 lines
New theorem
1
New record
1
Second routes to known results
3
Axioms behind every final theorem
propext Classical.choice Quot.sound
  1. 01 New theorem Erdős #1095

    A least-common-multiple bound for the Erdős–Selfridge function

    Let g(k) be the least n > k + 1 such that every prime factor of nk exceeds k. Then

    g(k) < lcm(1, 2, …, k)

    for every sufficiently large k: the eventual form of a 1974 conjecture of Ecklund, Erdős, and Selfridge.

    Scope Proves the eventual strict inequality only. The order of magnitude of g(k) remains open.

    Schematic at k = 120. The proof modifies lcm(1, …, k): one extra factor of each small prime , and the primes just below k removed . Lucas’s digit criterion turns the rest into a finite sieve.
  2. 02 New record HorizonMath

    A thin-triangle Kakeya construction at N = 128

    One thin triangle for each slope 0, 1/128, …, 127/128, each of width 1/128 at its base. Choosing the 128 intercepts well makes them overlap as much as possible. This choice gives a union of exact area

    0.106776325791034…

    which is 0.27% below the best published value.

    Keich’s construction
    0.119207
    Best published (Dualverse)
    0.107067
    This construction
    0.106776

    Scope An upper bound with an exact rational certificate, not a claim of optimality.

    Hover a triangle.
  3. 03 Independent disproof Erdős #996

    A bounded counterexample for lacunary averages with endpoint Fourier decay

    A 0–1 function f on the circle and a sequence with nj+1 ≥ 2nj. The Fourier tails of f decay like 8/√(log log m), and its integral is at most 1/16. Yet for almost every x, its averages along the sequence keep climbing back to 3/4. This refutes the triple-logarithmic condition Erdős asked about, for every exponent.

    Prior work Boon Suan Ho disproved the question first, by a different construction. No priority is claimed.

    1/16its average, at most
    3/4what the sampled averages keep returning to
  4. 04 Second route Erdős #1153

    Lebesgue functions on every interval

    For any n interpolation nodes in [−1, 1], let λ(x) = Σk |ℓk(x)|. On every fixed interval [a, b],

    max λ > (2/π − o(1)) log n

    uniformly in the choice of nodes: a question of Erdős and Turán from 1961.

    Prior work First resolved by Terence Tao in 2026, with a sharper error term. This is a different route. Its key input, the de Boor–Pinkus comparison theorem, is proved in full in the formalization.

    Drag the nodes.
  5. 05 Second route Erdős #825

    Abundant numbers are eventually semiperfect

    There is an absolute constant C such that every n with σ(n) > Cn is a sum of distinct proper divisors of n.

    Prior work First proved by Daniel Larsen. This is a different route. Its key input, the Alon–Freiman subset-sum theorem, is proved in full in the formalization.

    Sums of distinct proper divisors of 70 reach every number from 0 to 74 except 4 and 70 itself. So 70 is abundant, σ(70) = 144, yet not semiperfect. Benkoski and Erdős asked whether enough abundance always rules this out.