leanprover-community / leanprover-community/mathlib4
The Shapley-Folkman lemma
Open
@zhangmai19 is already working on this.
Since Jun 13, 2026.
good first issue
t-analysis
- Dominant language
- Lean
- Stars
- 4.2k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
The Shapley-Folkman lemma is a convex analysis result standard in the economics literature. In contrast, it is basically unheard of in mathematics.
The proof is elementary, and very similar to the proofs of Carathéodory's and Radon's theorems, which should serve as inspiration.
This issue existed in mathlib3 as https://github.com/leanprover-community/mathlib/issues/18135.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.