pi_1 of the circle is Z

pi1_circle_mulEquiv_int

Submitter: Kim Morrison.

Notes: Computes the fundamental group of the complex unit circle.

Source: Classical theorem in algebraic topology.

Informal solution: Use winding number to identify loops in the circle up to homotopy with the integers.

theorem declaration uses `sorry`pi1_circle_mulEquiv_int :
    Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ) := by⊢ Nonempty (HomotopyGroup.Pi 1 Circle 1 ≃* Multiplicative ℤ)
  sorryAll goals completed! 🐙

Solved by

• @rkirov with Claude Opus 4.7 (1M context) on May 3, 2026 (proof)

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

• @LorenzoLuccioli with Aristotle (Harmonic) on May 8, 2026 (proof)

• @sqrt-of-2 with GPT-5.5 on May 10, 2026 (proof)

• @rishistyping with Stealth Model on May 11, 2026

• @rishistyping with [submission] aegis-of-the-unit-circle-logos on May 12, 2026

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

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