Telescope Conjecture (Ravenel)

### What is the conjecture

The **Telescope Conjecture** is a central statement in chromatic homotopy theory, part of Ravenel's conjectures. It concerns the behavior of chromatic localization under telescoping constructions.

For a finite $p$-local spectrum $X$ of chromatic type $n$, suppose $v: \Sigma^d X \to X$ is a $v_n$-self map (a self-map such that the induced map $K(n)_*(v): K(n)_*(X) \to K(n)_*(X)$ is an isomorphism). The homotopy cofiber of the telescoping sequence constructed from $v$ is denoted $T_v$. The conjecture asserts:

$\pi_*(T_v) \cong \pi_*(L_n X)$

where $L_n$ denotes the chromatic localization functor at height $n$ and $\pi_*$ denotes the stable homotopy groups.

**Note on status:** The conjecture was **disproved in 2023** by Burklund, Hahn, Levy, and Schlank. However, it remains a fundamental research statement in the field, and formalizing the disproof or the original conjecture statement would be a significant contribution to the formalization of homotopy theory.

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

**Sources:**
- https://en.wikipedia.org/wiki/Ravenel%27s_conjectures, https://sanathdevalapurkar.github.io/files/iap-2018.pdf, https://ncatlab.org/nlab/show/chromatic+homotopy+theory, https://math.mit.edu/events/talbot/2013/ChromConjII.pdf

### Prerequisites needed

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

Building blocks (from Mathlib):
- Basic category theory and categorical limits (Mathlib.CategoryTheory.Limits)
- Homological algebra foundations (Mathlib.Algebra.Homology)

Missing pieces (not in current Mathlib):
- Stable homotopy theory and spectra: Mathlib lacks a formalized theory of spectra as generalized objects in homotopy theory. The current spectrum definition is limited to commutative algebra (algebraic geometry). Defining homotopy-theoretic spectra requires significant foundational work on infinity-categories or model categories.
- Chromatic homotopy theory: Chromatic localization, Morava K-theories $K(n)$, and the chromatic filtration are not present in Mathlib. These require the theory of spectra and formal group theory applied to homotopy theory.

Rating justification: Even stating the Telescope Conjecture requires fully formalizing the theory of spectra in homotopy theory and chromatic localization. This represents one of the major missing areas in Mathlib's algebraic topology infrastructure, making this a level-5 formalizability challenge.

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

* ams-55
* ams-18

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