Hilberts 15th Problem

### What is the conjecture

Establish rigorously and with exact determination of the limits of validity the foundations of Schubert's enumerative calculus. Given algebraic varieties with general position constraints, determine the geometric numbers (intersection multiplicities and solution counts) obtained by Schubert's elimination theory, such that the multiplicity of solutions and degree of elimination equations can be foreseen, and these counts are preserved under degenerations of position.

**Sources:**
- https://en.wikipedia.org/wiki/Hilbert%27s_fifteenth_problem, https://en.wikipedia.org/wiki/Schubert_calculus, https://en.wikipedia.org/wiki/Enumerative_geometry, https://ncatlab.org/nlab/show/Schubert+calculus, https://encyclopediaofmath.org/wiki/Schubert_calculus

### Prerequisites needed

**Formalizability Rating:** 5/5 (0 is best) (as of 2026-01-20)

Schubert calculus in Lean/Mathlib requires significant foundational development. Core concepts needed include: (1) Grassmannian varieties and their Chow rings, (2) intersection theory with multiplicities, (3) Littlewood-Richardson rules, (4) characteristic classes, (5) elimination theory for polynomial systems with multiplicity tracking. While algebraic varieties and basic intersection theory have some Mathlib coverage, the specialized machinery of Schubert calculus (Chow rings, Grassmannian geometry, and the rigorous treatment of enumerative counting) would require substantial new theory development to formalize this problem completely.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-14
* ams-13
* ams-18

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Created by AI, reviewed by me.

No files, tests, or entry points are named. Start by reviewing existing formalized conjectures in the repository and the cited material on Schubert calculus; done would mean adding a rigorous Lean statement or formalization with the required foundational machinery.

Written by the indexing model from the issue text.