Granville

These files accompany the paper arXiv:XXXX.XXXXX.

The formal proofs provided in this work were developed and verified using Lean 4.26.0. Compatibility with earlier or later versions is not guaranteed due to the evolving nature of the Lean 4 compiler and its core libraries.

Input files

Section 2

• task.md: description of the task to be completed
• requirement.md: additional requirement of the formalization
• LocalGlobal.nterms6.tex: the informal proof of the main theorem.
• .environment: specifies the Lean version

Sharpening inequality for $n = 3$

• task.md: description of the task to be completed
• .environment: specifies the Lean version

Wronskian

• task.md: description of the task to be completed
• .environment: specifies the Lean version
• LocalGlobal.nterms6.pdf

Output files (Run with Lean 4.26.0)

Section 2

• problem.lean: translation of the problem statement into formal language (Lean)
• solution.lean: solution in formal language (Lean)

Sharpening inequality for $n = 3$

• problem.lean: translation of the problem statement into formal language (Lean)
• solution.lean: solution in formal language (Lean)

Theorem 3.5, Corollary 3.6 and 3.7

• problem.lean: translation of the problem statement into formal language (Lean)
• solution.lean: solution in formal language (Lean)

License

This repository uses the MIT License. See LICENSE for details.

Repository maintainers

• Evan Chen
• Kenny Lau
• Ken Ono
• Jujian Zhang