Working on a project: Sylvester-Schur

Stream: new members

[J. J. Issai (project started by GRP)]

Hi. I'm posting using an account for a specific project: getting an enhanced version of Sylvester-Schur into Lean. This version improves upon the original theorem as follows: there is an arithmetic function f(k) (naturals to naturals) such that for all $k$ and for all $n \ge f(k)$, there is a prime $p > k$ which divides $(n+1)...(n+k)$.
Sylvester and Schur (and Erdos) gave (somewhat partial) proofs of this for the function f(k)==k. I hope to generate a proof in Lean with some f(k) < k, and I am experimenting to see how small and explicit I can make f(k) using elementary methods.

I started using the Google AI assistant Gemini 2.5 to help, and I suspect it is giving me some hallucinations. I am looking for some direction from the community.

Which channel(s) should I join to learn about using Gemini/Lean effectively?

Which channels/resources should I find to determine how much toward Sylvester-Schur has been done already?

I suspect that nothing has been done in this direction beyond the (module, proof, document?) Bertrand in MathLib, but Gemini leads me to believe that Sylvester-Schur and a necessary precursor (the Law of Ademption, details provided upon request) have already been implemented in MathLib. My initial searches turn up nothing.

I welcome other advice. For this project, I will sign using initials rather than something longer. I am Gerhard Paseman.

GRP 2025.06.17.

[Scott Carnahan]

If you want f(k) < k, then you should revise the claim to assume 2 ≤ k.

[Johan Commelin]

Dear GRP, welcome to Zulip!

There is a channel #Machine Learning for Theorem Proving dedicated to all aspects AI in the ITP context.

Searching for results in Mathlib is a bit of a dark art. But one very good fallback is to ask on Zulip, as you just did. For this we have the channel #Is there code for X?.

[Johan Commelin]

And of course you should feel free to ask all sorts of Lean related questions in this current channel!

[J. J. Issai (project started by GRP)]

Johan thank you. I will check on those channels and form a query there. Is there a way to reference this conversation when I create a message there?

[J. J. Issai (project started by GRP)]

Incidentally, $f(k) \ge k'-k$, where $k'$ is the smallest prime number bigger than k. One can give a "useless" proof of this once S-S is established. Thus $f(1) \ge 1$ . My hope is to find some nicely expressible and tight upper bounds on f(k) using elementary methods. These upper bounds will be considered useful (at least, by me).

GRP 2025.06.18.

[Johan Commelin]

@J. J. Issai (project started by GRP) If you write #ne some where in a message, you should get an auto completion menu, that allows you to select #new members, and then further select this particular topic.

Also, concerning typesetting: you can write LaTeX maths if you enclose it in double dollars (yes, not single ones :shrug:). So $$\sqrt{a + b}$$ gives $\sqrt{a + b}$.

[Edward van de Meent]

and for multiline math, you can do the following:

```math
x^2 - y ^2 = (x + y)(x - y)\\
\text{e}^{i\pi} = -1\\
\frac{a}{b} + \frac{c}{d} = \frac{ad + bc}{bd}
```

produces

$$x^2 - y ^2 = (x + y)(x - y)\\ \text{e}^{i\pi} = -1\\ \frac{a}{b} + \frac{c}{d} = \frac{ad + bc}{bd}$$

[J. J. Issai (project started by GRP)]

Edward and Johan, thank you. I will need help with some basics, particularly finding items in Mathlib to use and then examples of how to use them. I am hoping to find the following:

p-adic valuation of factorial : $\nu_p(n!) = \sum_{e>0} \lfloor \frac{n}{p^e} \rfloor$ ;

Sylvester's Law of Ademption: for any prime power $p^e$, $p^e \mid {{n+k} \choose k}$ implies $p^e \le n+k$;

Sylvester's Fundamental Inequality: for $k$-smooth terms

$$(n+1)\cdots(n+k), \\ (n+1)\cdots(n+k - \pi(k)) \le k! .$$

Pointers to these in Mathlib would be appreciated. GRP 2025.06.20.

[J. J. Issai (project started by GRP)]

Thanks to JZ Pan I have these as an entry point for p-adic valuation od factorial. I am still looking for prior are for the Law and Inequality.

[Kenny Lau]

@J. J. Issai (project started by GRP) does Nat.Prime.emultiplicity_choose help?

[Aaron Liu]

I've got the second one here

import Mathlib

example {u n k : Nat} (hn : k ≤ n) (hu : IsPrimePow u) (h : u ∣ n.choose k) : u ≤ n := by
  obtain ⟨p, e, hp, he, rfl⟩ := hu
  have : Fact p.Prime := ⟨Nat.prime_iff.mpr hp⟩
  have h0 : n ≠ 0 := by
    intro h0
    rw [(hn.trans_eq h0).antisymm k.zero_le, Nat.choose_zero_right,
      Nat.dvd_one, Nat.pow_eq_one, or_iff_left he.ne'] at h
    rw [h] at hp
    exact not_prime_one hp
  rw [padicValNat_dvd_iff_le (Nat.choose_pos hn).ne',
    padicValNat_choose hn (Nat.lt_add_one _), Finset.Ico_add_one_right_eq_Icc] at h
  have hb := h.trans (Finset.card_filter_le ..)
  rw [Nat.card_Icc, Nat.add_sub_cancel] at hb
  apply (Nat.pow_le_pow_right (Nat.prime_iff.mpr hp).pos hb).trans
  exact Nat.pow_log_le_self p h0

[J. J. Issai (project started by GRP)]

@Kenny Lau Thanks, JZ Pan recommended it too on another channel. I will check it out.

[J. J. Issai (project started by GRP)]

@Aaron Liu Thanks! I'm still in blueprint mode. I will study this along with other examples soon. I hope you can answer questions about this in a few days.

[J. J. Issai (project started by GRP)]

@Aaron Liu While I'm here, a newbie Zulip question: In a message, I can embed some math with double $. signs. Is there a macro function similar to LaTeX newcommand so that I can define a symbol and then use it? Like in LaTeX \newcommand{\manyalpha}{\alpha\alpha\alpha\alpha}. and then use \manyalpha between double $ signs?

[J. J. Issai (project started by GRP)]

I would expect to redefine the macro across new messages.

[Aaron Liu]

I have no idea, I don't really use LaTeX that much in zulip messages

[Kenny Lau]

$\newcommand{\manyalpha}{\alpha\alpha\alpha\alpha}\manyalpha$

[Kenny Lau]

$$\manyalpha$$

[Kenny Lau]

yep looks like it doesn't transfer across messages

[Aaron Liu]

Wow it works

[J. J. Issai (project started by GRP)]

OK. I will try it. Thanks Kenny and Aaron.