Guralnick-Thompson conjecture on monodromy groups

### What is the conjecture

The Guralnick-Thompson conjecture concerns the structure of monodromy groups of algebraic coverings. Let $X \to Y$ be a branched cover of the Riemann sphere, and let $G$ be the monodromy group associated with this cover. The conjecture states that under certain conditions related to the genus and branch points of the cover, the monodromy group $G$ is either the full symmetric group $S_n$ or the alternating group $A_n$ (where $n$ is the degree of the cover). More specifically, the alternating group occurs precisely when the cover has genus $g > 3$ and degree $n > 2g$. This conjecture relates Galois-theoretic properties of coverings to the structure of primitive permutation groups.

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

**Sources:**
- https://www.degruyterbrill.com/document/doi/10.1515/9783110893106.43/html?lang=en, https://www.sciencedirect.com/science/article/pii/002186939090292V, https://authors.library.caltech.edu/80053/, https://arxiv.org/html/2407.20355, https://link.springer.com/book/10.1007/b101762

### Prerequisites needed

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

Building blocks (1-3; from Mathlib):
- `FiniteGroup` and group actions via `MulAction` are available
- `Equiv.Perm` for permutation groups and symmetric/alternating group types exist
- Basic Galois theory framework with field extensions and automorphism groups

Missing pieces (exactly 2; unclear/absent from search results):
- Comprehensive formalization of primitive permutation group theory (classification, transitivity properties)
- Complete monodromy group framework connecting branched covers of Riemann sphere to permutation groups via Galois correspondence

Rating justification: While basic group theory and permutation groups are in Mathlib, the statement requires significant theory development around primitive permutation groups, transitivity properties of group actions, and the algebraic geometry machinery connecting branched covers to monodromy groups. The definitions exist but substantial connecting theory is needed.

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

* ams-20
* ams-12
* ams-14

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