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

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

Start by reading the linked source and reviewing the available Mathlib topology, closure, homeomorphism, and simplicial-complex material. Then determine how varieties over ℚ, their rational and real loci, and the required topological statement could be represented; done means adding a complete Lean formalization of the conjecture.

Written by the indexing model from the issue text.