Formalization blueprint

Algebraic Topology (Hatcher)

A Lean 4 formalization of results from Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002), built on Mathlib.

97%

Formalized

261 of 268 items settled

2

Ready now

unblocked, waiting for an author

6

Chapters

top-level milestones

Next up

Relative chains commute with coproducts of arbitrary pairs

Every prerequisite is stated, so this can be written down.

Dependencies

Project map Select a chapter to open its dependencies

graph LR n0["Appendix<br/><small>5 items · 5 fully proved</small>"]:::scope n1["Cohomology<br/><small>3 items · 3 not ready</small>"]:::scope n2["The fundamental group<br/><small>118 items · 8 in mathlib · 110 fully proved</small>"]:::scope n3["Homology<br/><small>146 items · 10 in mathlib · 128 fully proved · 2 ready to state · 1 not ready · 5 planned</small>"]:::scope n4["Homotopy theory<br/><small>3 items · 3 not ready</small>"]:::scope n5["Algebraic Topology (Hatcher) roadmap<br/><small>1 item · 1 not ready</small>"]:::scope n0 -. 4 .-> n2 n2 -->|3| n3 n2 -. 6 .-> n3 click n0 "dependencies/chapters/appendix.html" "Appendix — 5 items · 5 fully proved" click n1 "dependencies/chapters/cohomology.html" "Cohomology — 3 items · 3 not ready" click n2 "dependencies/chapters/fundamental-group.html" "The fundamental group — 118 items · 8 in mathlib · 110 fully proved" click n3 "dependencies/chapters/homology.html" "Homology — 146 items · 10 in mathlib · 128 fully proved · 2 ready to state · 1 not ready · 5 planned" click n4 "dependencies/chapters/homotopy-theory.html" "Homotopy theory — 3 items · 3 not ready" click n5 "dependencies/chapters/roadmap.html" "Algebraic Topology (Hatcher) roadmap — 1 item · 1 not ready"

in mathlib18Upstreamed into Mathlib.fully proved243Proved, and every prerequisite is fully proved too.ready to state29Prerequisites are stated, so this can be written down.not ready8Needs more blueprint work before it can be attempted.planned5Described in the blueprint only.