Uniform Boundedness Conjecture for rational points

### What is the conjecture

For a given number field $K$ and positive integer $g \geq 2$, there exists $N(K, g)$ depending only on $K$ and $g$ such that for any algebraic curve $C$ defined over $K$ of genus $g$, the number of $K$-rational points is at most $N(K, g)$: $$|C(K)| \leq N(K, g).$$

**Sources:**
- https://en.wikipedia.org/wiki/Uniform_boundedness_conjecture_for_rational_points, https://math.mit.edu/~poonen/slides/uniformboundedness.pdf

### Prerequisites needed

**Formalizability Rating:** 4/5 (as of 2026-01-20)

Mathlib has basic algebraic geometry foundations but lacks comprehensive formalization of algebraic curves, genus, Jacobian varieties, and the Mordell-Weil rank. The conjecture also relies on Faltings' theorem (Mordell's conjecture), which is currently not formalized in Mathlib. Significant theory development would be needed to formalize the concept of K-rational points on curves and establish the connection to height theory and abelian varieties.

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

* ams-11
* ams-14
* ams-12

### 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.

Start by reviewing the repository's existing algebraic-geometry formalizations and conventions for conjecture statements. Check whether number fields, algebraic curves, genus, and rational points are available; done means adding a checked formal statement of the conjecture without relying on unformalized results.

Written by the indexing model from the issue text.