First Contribution: Robbins' sharp bound for Stirling Seq

Stream: mathlib4

[Ashton J]

This is going to be my first contribution to Mathlib4, so I'd appreciate any guidance on the process and approach.

I've formalized Robbins' sharp bound for successive differences in the logarithm of the Stirling sequence:

$|\log(\text{stirlingSeq}(k+1)) - \log(\text{stirlingSeq}(k))| \leq \frac{1}{12k(k+1)}$

This improves the existing bound of $\frac{1}{4k^2}$.

The Mathlib docs note this sharper bound as "not yet formalised, noted at Stirling.le_factorial_stirling.

Link to code:
https://gist.github.com/FaffyWaffles/e1703b6146d8b743a257ec364a86bde4

I have several questions...

I'm planning to add it to Mathlib/Analysis/SpecialFunctions/Stirling.lean, is that the right location?

I've atomized the proof with many small lemmas. Should I consolidate some of these, or is the preferred approach?

Are there naming conventions I should follow? (I tried to follow what I saw in existing files)

I haven't made a PR yet, as I wanted to get feedback first. Happy to make any changes needed to fit Mathlib standards.

Thanks for your help!

[Kenny Lau]

@Ashton J thank you for your honesty about using LLM. do you have a rough estimate of how much of the code is by LLM, or could you provide a rough outline of what was the process of incorporating LLM?

[Kenny Lau]

also could you instruct the LLM to make the docstrings conform more to mathlib standard? this shouldn't be hard for an LLM since it's a language task

[Kenny Lau]

and what does atomised mean?

[Kenny Lau]

image.png

LLM-generated code tends to have a lot of inefficiencies, such as here where a library lemma was just restated two times

[Kenny Lau]

you should try to understand the code yourself

[Ashton J]

Solid 75%, I am still quite new to Lean. The Method I used was I would create a Outline of exactly what we needed to prove. Then, I would "atomize" it, meaning break up a pretty complex lemma into something bitesized, and easy to prove on its own. Then, I would write roughly what I wanted to prove with each lemma, and had Aristotle try to prove some of the easier lemmas. I also went back and forth with Claude for some of the more complex lemmas.

[Ashton J]

I actually did know about that specific section of code, and am going to refactor it in a bit. This was a byproduct of the "Atomization", where we determine what is and is not already in the library.

[David Loeffler]

This looks very nice! It would be a good, solid first contribution to mathlib.

I'm planning to add it to Mathlib/Analysis/SpecialFunctions/Stirling.lean, is that the right location?

Sure - either there, or in a separate file Mathlib/Analysis/SpecialFunctions/StirlingRobbinsBound.lean if you want to keep it separate. Either is fine. (If you make a new file, you should run lake exe mk_all to add it to the main mathlib index file.)

I've atomized the proof with many small lemmas. Should I consolidate some of these, or is the preferred approach?

Right now it is definitely too atomized. A lot of your lemmas are just re-statements of existing mathlib lemmas, or can be proved in one line with standard tactics like ring or positivity. These lemmas should be dispensed with, and applications of them replaced by applications of the existing library lemma or tactic.

Are there naming conventions I should follow? (I tried to follow what I saw in existing files)

Here are the naming conventions; have a look at the other advice under "contributing" as well. The naming conventions take a bit of getting used to, but this is something that will be addressed during the PR review process.