Mazur's Conjecture 1: Zariski-density and topological closure of rational points

### What is the conjecture

Let $X$ be a smooth variety over $\mathbb{Q}$ such that $X(\mathbb{Q})$ is Zariski-dense in $X$. Then the topological closure of $X(\mathbb{Q})$ in $X(\mathbb{R})$ consists of a (finite) union of connected components of $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 (1-3; from search results):
- Topological closure and connected components (Mathlib)
- Zariski topology (partially in Mathlib schemes, but limited)

Missing pieces (exactly 2; unclear/absent from search results):
- Formalization of algebraic varieties over $\mathbb{Q}$ with rational and real points, including the notion of Zariski-density on varieties
- Rigorous definition of topological closure of rational points in real points of a variety with proper topology structure

Rating justification (1-2 sentences): Even stating this conjecture requires foundational algebraic geometry infrastructure (definition of smooth varieties, rational/real point sets, Zariski topology) that does not exist in usable form in Mathlib. Substantial new theory development in scheme theory and algebraic geometry would be required.

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

* ams-14
* ams-11

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