JD-Jones-ASESFsFormal1.0.0

Palomar-ready Lean formalization of an improved Furstenberg-Sarkozy lower bound
#mathematics #additive-combinatorics #palomar
Sort by
  1. Registry dependency.
    Found on Reservoir.

    mathlibv4.33.0

    The math library of Lean 4