Mazur's Conjecture 2: Topology of rational points on varieties

[franzhusch]

What is the conjecture

Consider a variety $V$ defined over $\mathbb{Q}$. The conjecture states: The topological closure of the set of rational points of any variety over $\mathbb{Q}$ in its real locus is homeomorphic to the complement of a finite subcomplex in a finite complex.

(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):

• Mathlib topological spaces: closure, homeomorphism
• Basic algebraic geometry (field extensions)
• Simplicial complexes and finite complexes

Missing pieces (exactly 2; unclear/absent from search results):

• Formal definition of algebraic variety over $\mathbb{Q}$ and its real and rational loci ($V(\mathbb{Q})$, $V(\mathbb{R})$)
• Infrastructure for relating scheme-theoretic or concrete algebraic variety definitions to the topological closure property needed for the statement

Rating justification (1-2 sentences): Significant new definitions are required to formalize varieties, their rational and real points, and the real locus, even though the topological machinery (closure, homeomorphism) exists in Mathlib. This requires substantial domain-specific algebraic geometry setup.

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