Mazur's Conjecture 3: Finite connected components of rational points

### What is the conjecture

For any algebraic variety defined over the rationals $\mathbb{Q}$, consider the set of its rational points equipped with the subspace topology from the real locus.

The topological closure of the set of rational points has at most a finite number of connected components:

$\text{Count of connected components of } \overline{X(\mathbb{Q})} \text{ in } X(\mathbb{R}) \text{ isfinite}$

where $X$ is a variety over $\mathbb{Q}$, $X(\mathbb{Q})$ denotes the rational points, and the closure is taken in the real points $X(\mathbb{R})$.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://projecteuclid.org/euclid.em/1048709114

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-02-06)

Building blocks (2; from search results):
- Topological closure and connected components (Mathlib: TopologicalSpace.closure, ConnectedComponents)

Missing pieces (2; unclear/absent from search results):
- Formal definition connecting rational points to the real locus topology
- Finiteness of connected component counting for varieties

Rating justification (2 sentences): The basic topological and algebraic objects are available in Mathlib (varieties, closure, connected components), but formalizing the specific statement requires careful definition of how rational points embed into the real points and a minor lemma about component counting. This is a minor infrastructure gap rather than a fundamental one.

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

* ams-14
* ams-11
* ams-54

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

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

Start by reviewing Mathlib's TopologicalSpace.closure and ConnectedComponents definitions, then inspect the available variety and rational-point infrastructure. The work is complete when the conjecture's rational-point embedding, real-locus topology, and finite connected-component statement are expressed and checked in Lean.

Written by the indexing model from the issue text.