Halperin Conjecture

### What is the conjecture

In rational homotopy theory, the Halperin conjecture (formulated by Stephen Halperin in 1976) concerns the Serre spectral sequence of fibrations with certain fiber properties.

Let $F \to E \to B$ be a fibration where the fiber $F$ is an elliptic space with evenly graded cohomology (equivalently, with positive Euler characteristic $\chi(F) > 0$). The conjecture states that this fibration is **TNCZ** (totally non-homologous to zero), which means the induced map $H^*(B) \to H^*(F)$ is surjective in rational cohomology. Equivalently, the Serre spectral sequence associated to the fibration degenerates at the $E_2$-page.

An elliptic space is a simply connected space whose rational homotopy algebra (the minimal model) is a finite-dimensional, commutative, differential graded algebra over $\mathbb{Q}$.

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

**Sources:**
- https://en.wikipedia.org/wiki/Halperin_conjecture, https://arxiv.org/abs/2104.04086, https://arxiv.org/abs/math/0010124, https://link.springer.com/article/10.1007/s40062-015-0114-y

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Fibrations and fiber bundles (basic category theory and topology in Mathlib)
- Serre spectral sequences (available in Mathlib's homological algebra)
- Rational cohomology and differential graded algebras (partially in Mathlib)

Missing pieces (exactly 2; unclear/absent from search results):
- Rational homotopy theory infrastructure: formal definitions of elliptic spaces, minimal models, and the correspondence between spaces and commutative differential graded algebras over $\mathbb{Q}$
- Characterization of the TNCZ property in terms of spectral sequence degeneracy and explicit connection to formality and the Euler characteristic condition

Rating justification (1-2 sentences): The foundational concepts (fibrations, spectral sequences) exist in Mathlib, but the theory of rational homotopy, elliptic spaces, and their formal properties requires significant new infrastructure beyond what is currently available. The formalization would require developing a substantial portion of rational homotopy theory, particularly the minimal model machinery and formality conditions.

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

* ams-55

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