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

[franzhusch]

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

• ams-14
• ams-11

Choose either option

• I plan on adding this conjecture to the repository
• 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

Feedback on mistakes/hallucinations: link