Would mathlib accept Sylvester–Schur (Sylvester’s theorem)?

Stream: mathlib4

[Coder-Osman]

Hello mathlib community,

I’m preparing a contribution formalizing the Sylvester–Schur theorem (often called Sylvester’s theorem). In the formulation I have fully formalized in Lean:

theorem exists_prime_gt_and_dvd_ascFactorial
    {n k : ℕ} (hk : 0 < k) (hkn : k < n) :
    ∃ p : ℕ, p.Prime ∧ k < p ∧ p ∣ n.ascFactorial k

Informally: for 0 < k < n, the rising factorial n.ascFactorial k = n * (n+1) * ... * (n+k-1) has a prime divisor strictly larger than k.

Before opening a PR, I’d like to ask some questions:

Is this theorem a good fit for mathlib?

The proof follows the classical Erdős-style argument (bounding a related binomial coefficient via prime-factor envelopes / primorial-style products / central binomial coefficient chains, then deriving a contradiction under a “no prime > k divides” hypothesis).

• I’m trying to keep dependencies reasonable and reuse existing lemmas where possible, but the development does introduce some supporting infrastructure (product decompositions and inequalities tailored to the argument).

Any red flags you anticipate (e.g. proof too long/fragile, too much bespoke inequality machinery, or missing connections to existing results like Mathlib/NumberTheory/Bertrand.lean)?

For reference, Wikipedia’s discussion of “Sylvester’s theorem” in the Bertrand page is here:
https://en.wikipedia.org/wiki/Bertrand%27s_postulate#Sylvester%27s_theorem

Also: the formalization was drafted with AI assistance and then reviewed/edited by me

Thanks a lot for any guidance on whether this is “in scope” for mathlib and what acceptance criteria I should keep in mind.

[Eric Wieser]

If you've already done the work, you may as well upload a draft PR and link back to this discussion in the description; probably the most relevant factor is the size of the contribution, since usually for first contributions we recommend contributors start small.

[Bhavik Mehta]

The statement is something I believe mathlib should have. The size and quality of code are the potential red flags, especially with AI-assisted proofs.

[Coder-Osman]

Thanks Eric and Bhavik — this is very helpful.
I agree that the main question is really the size/maintainability. I’ve already completed a full formalization of the core statement and I’m currently doing some cleanup work, in particular removing remaining native_decide usage.
I’ll post the draft PR link shortly after the native_decide removal and cleanup are complete.

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

Oooh, do I have a lot to say about this.

The short version is that the Erdos proof leaves lots of small cases to the reader, and does not prove the general version involving irreducible arithmetic progressions. Nor does his work extend easily to modern improvements of the Sylvester-Schur Theorem.

The long version is that I am also formalizing that theorem, but in parallel with some generalizations of it. (I omit details which are mathematically interesting but may not be appropriate for this thread.) If you (or anyone else) is interested in what I have learned so far, I encourage you to DM (direct message) me. I have a spotty connection, but I will respond eventually.

I will be very interested in hearing about the challenges you encounter in the formalization of the proof, especially in how you restate the Erdos bound of lcm(1..n) which he uses. I am also willing to compare notes and receive assistance on my path toward formalization.

[Coder-Osman]

I’ve uploaded a draft PR here: https://github.com/Coder-Osman/mathlib4/blob/master/Mathlib/NumberTheory/SylvesterSchur.lean

One remaining blocker is removing the native_decide-based finite check. I’ve been working on replacing it with a decide-only approach, but in practice it’s still extremely slow—even with an algorithmic improvement (roughly linear-time in the range being checked), the kernel checking time can be on the order of tens of minutes. I’ll need a few more days to engineer a Lean-friendly certificate/verification strategy and then I’ll update the PR.

[Snir Broshi]

Coder-Osman said:

I’ve uploaded a draft PR here: https://github.com/Coder-Osman/mathlib4/blob/master/Mathlib/NumberTheory/SylvesterSchur.lean

This is not a draft PR, you currently have no PRs to Mathlib.
See Git Guide for Mathlib4 Contributors for help.

[Snir Broshi]

(though it does let others see your code, so maybe a draft PR is redundant)

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

Besides the finite check, do you see any other aspect that would discourage the draft from being accepted into Mathlib?

[Coder-Osman]

J. J. Issai (project started by GRP) said:

Besides the finite check, do you see any other aspect that would discourage the draft from being accepted into Mathlib?

Besides the native_decide, I don’t see any other aspect that would discourage acceptance into mathlib.

[Coder-Osman]

Quick update: I’ve removed native_decide from the finite check. It now uses only decide, and compiles in about ~2 minutes on my machine. Is that within the usual acceptable range for mathlib?

[Coder-Osman]

Now I optimized it to ~1.5 minutes on my machine

[Violeta Hernández]

2 minutes is way too much for an individual file. Mathlib consists of 8,000 different files and takes only about an hour to build in full.

[Violeta Hernández]

...though your file is also 3k lines long, whereas Mathlib has a 1.5k line restriction per file, and most files are well under 1k.

[Violeta Hernández]

How are you verifying the cases below 2304? I know that for Bertrand's postulate you also get a similarly large lower bound, but then it turns out you only have to check that about 20 numbers are prime. Does something similar happen here?

[Violeta Hernández]

Assuming there isn't some decide call that's taking most of the compile time, and assuming you can clean up your code to Mathlib standards, then I think it should belong in there.

[Coder-Osman]

I’ve now removed native_decide, and I managed to get the FiniteCheck part to compile in ~10s on my machine (it’s decide-only).

The remaining issue is size: after the refactor the development is ~6000 lines. Would you prefer that I move the finite-check machinery into a separate file (e.g. SylvesterSchur/FiniteCheck.lean) so the main theorem file stays within the usual line/maintenance expectations?

[Michael Rothgang]

As a rule of thumb, no file in mathlib should be larger than 1500 files (and usually, we prefer shorter than 1000 lines). The code should definitely be split sensibly.

[Coder-Osman]

Violeta Hernández said:

How are you verifying the cases below 2304? I know that for Bertrand's postulate you also get a similarly large lower bound, but then it turns out you only have to check that about 20 numbers are prime. Does something similar happen here?

For Sylvester–Schur I don’t think there’s a Bertrand-style reduction to “check a tiny fixed list of primes”: the obstruction is that we need a witness prime depending on both n and k.

Instead, I verify the finite range n ≤ 2304 via an explicit algorithmic certificate:

• For each n I construct a small list of primes (in practice ≤ 3 primes suffice) such that their associated validity intervals cover all k ∈ {1,…,⌊n/2⌋}.
• Given a prime p, its interval is computed from r = n % p as k ∈ [r+1, min(p-1, ⌊n/2⌋)] .
• Then the checker just verifies coverage of 1..⌊n/2⌋ by these intervals, plus primality of the chosen p’s.

This makes the verification essentially linear in n overall, rather than enumerating all (n,k) pairs.

[Michael Rothgang]

That said, the big open questions are the size and quality of your code: I don't think any experienced mathlib contributor has looked at that yet. Bare AI output is far from good enough.

[Kevin Buzzard]

Looking through the code, I think the answer to "would mathlib accept this multi-thousand line file" (which is my interpretation of the title of this thread) is "not without a large amount of further work". Some of the code is good, some is terrible (e.g. have _ := hn0), and as usual with LLM-generated code there are far too many definitions almost none of which have any API, and some of the proofs are far too long.

[Kevin Buzzard]

Screenshot 2026-02-27 at 15.09.58.png

Another typical issue with LLM-generated code is the "wall of have phenomenon". (this is in the middle of a 100-line proof).

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

Violeta Hernández said:

How are you verifying the cases below 2304? I know that for Bertrand's postulate you also get a similarly large lower bound, but then it turns out you only have to check that about 20 numbers are prime. Does something similar happen here?

Sylvester's original proof showed (using instead the form (m+1)(m+2)...(m+n) ) that the result held for m>n^2 and then for 13<n<3000 by a largish table of prime gaps. Erdos provides no such argument for small cases, and I suspect that is not happening in the repo being submitted/refactored. I imagine that a hand-coded version could work for the check along the lines of Sylvester's argument, but a lot of lines of code would be spent on k<= 13 because of the formalization challenges.

[Coder-Osman]

Thanks, this is very helpful feedback.
I agree with your assessment: in its current form, this draft is not ready for mathlib. Some parts are in decent shape, but there is clearly a lot of cleanup and restructuring still needed. In particular, I need to break the file into smaller units, remove many ad hoc definitions in favor of a better API, shorten some of the longer proofs, and clean up the proof style throughout.
I’ll take this as a guide for the next round of refactoring.

[Violeta Hernández]

Mathlib could accept this result, polished up, to answer your original query.

[Kevin Buzzard]

I agree. I am also not at all convinced that a human with no experience of writing mathlib-standard code and armed with an LLM, however expensive, could pull this off. The LLMs aren't yet good enough and if a concerted effort is made by the human to use it to make mathlib-standard PRs it won't be long before human reviewers become exasperated with the slop and just stop reviewing. That's the unfortunate state of affairs right now.

In general the community is perfectly well aware that an arbitrary mathematical result at Masters level can currently be formalised into code that compiles by a sufficiently expensive machine, and they are also well aware that this is nowhere near enough to get it into mathlib. On the other hand there is a whole crowd of people out there who are not part of this community and who are not aware of this and each of them seems to need to be told individually.

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

How about this statement (after fixing syntax errors)?

theorem exists_prime_gt_k_and_dvd_irred_arithprog_k
    {n k d : ℕ} (hk : 0 < k) (hkn : k <= n) (hnd: 1=gcd n d) :
    ∃ p : ℕ, p.Prime ∧ k < p ∧ p ∣ \prod i in Icc 1  k , (n + i*d)

Would that be accepted as well (and would it displace the first theorem, which is the case d=1)? Or would both have a place in Mathlib?

[Coder-Osman]

Thanks — this is a fair point, and I understand the distinction you’re making between “code that compiles” and “code that is actually suitable for mathlib.”

I’ll continue restructuring the proof and cleaning up the code with mathlib standards in mind. I’m not expecting reviewers to help polish an LLM-generated draft into an acceptable PR; that part is my responsibility. My goal is to reduce the amount of ad hoc material, improve the API and proof structure, and only ask for review once the development is in much better shape.