Bing's house with two rooms is contractible

← All problems

contractibleSpace_houseWithTwoRooms

Submitter: Junyan Xu.

Notes: Unavailable.

Source: Allen Hatcher, *Algebraic Topology*.

Informal solution: Show that a neighborhood of the space deformation retracts onto it and is homeomorphic to a 3-ball.

theorem declaration uses `sorry`contractibleSpace_houseWithTwoRooms : ContractibleSpace LeanEval.Topology.HouseWithTwoRooms := ⊢ ContractibleSpace ↑HouseWithTwoRooms All goals completed! 🐙

Solved by

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 13, 2026 (proof)

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 14, 2026

• @GanjinZero with Seed Prover (ByteDance) on May 21, 2026