GitHub - plby/HopfProblem: A formalization of the resolution of the Hopf problem: the six-sphere admits a complex manifold structure compatible with its standar

Source: https://github.com/plby/HopfProblem

Skip to content

Navigation Menu

[](https://github.com/)

Sign in

Appearance settings

* Platform

* AI CODE CREATION

- GitHub Copilot Write better code with AI

- GitHub Copilot app Direct agents from issue to merge

- MCP Registry Integrate external tools

* DEVELOPER WORKFLOWS

- Actions Automate any workflow

- Codespaces Instant dev environments

- Issues Plan and track work

- Code Review Manage code changes

- Code Quality Enforce quality at merge

* APPLICATION SECURITY

- GitHub Advanced Security Find and fix vulnerabilities

- Code security Secure your code as you build

- Secret protection Stop leaks before they start

* EXPLORE

- Why GitHub

- Documentation

- Blog

- Changelog

- Marketplace

View all features

* Solutions

* BY COMPANY SIZE

- Enterprises

- Small and medium teams

- Startups

- Nonprofits

* BY USE CASE

- App Modernization

- DevSecOps

- DevOps

- CI/CD

- View all use cases

* BY INDUSTRY

- Healthcare

- Financial services

- Manufacturing

- Government

- View all industries

View all solutions

* Resources

* EXPLORE BY TOPIC

- AI

- Software Development

- DevOps

- Security

- View all topics

* EXPLORE BY TYPE

- Customer stories

- Events & webinars

- Ebooks & reports

- Business insights

- GitHub Skills

* SUPPORT & SERVICES

- Documentation

- Customer support

- Community forum

- Trust center

- Partners

View all resources

* Open Source

* COMMUNITY

- GitHub Sponsors Fund open source developers

* PROGRAMS

- Security Lab

- Maintainer Community

- GitHub Stars

- Archive Program

* REPOSITORIES

- Topics

- Trending

- Collections

* Enterprise

* ENTERPRISE SOLUTIONS

- Enterprise platform AI-powered developer platform

* AVAILABLE ADD-ONS

- GitHub Advanced Security Enterprise-grade security features

- Copilot for Business Enterprise-grade AI features

- Premium Support Enterprise-grade 24/7 support

- Pricing

Search/

Sign in

Sign up

Appearance settings

You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert

{{ message }}

plby/**HopfProblem**Public

- NotificationsYou must be signed in to change notification settings

- Fork 3

- Star 61

- Code

- Issues 1

- Pull requests 1

- Actions

- Projects

- Security and quality 0

- Insights

Additional navigation options

- Code

- Issues

- Pull requests

- Actions

- Projects

- Security and quality

- Insights

[](https://github.com/plby/HopfProblem)

master

**2**Branches**0**Tags

[](https://github.com/plby/HopfProblem/branches)[](https://github.com/plby/HopfProblem/tags)

Go to file

Code

Open more actions menu

Latest commit

plby

.

Aug 27, 2026

9ac8a45·Aug 27, 2026

History

2 Commits

Open commit details

[](https://github.com/plby/HopfProblem/commits/master/)2 Commits

Folders and files

| Name | Name | Last commit message | Last commit date | | --- | --- | --- | --- |

| [comparator](https://github.com/plby/HopfProblem/tree/master/comparator "comparator") | [comparator](https://github.com/plby/HopfProblem/tree/master/comparator "comparator") | [.](https://github.com/plby/HopfProblem/commit/cc698c96ee9502138139a0a0e2277a46721d3c94 ".") | Aug 27, 2026 |

| [.gitignore](https://github.com/plby/HopfProblem/blob/master/.gitignore ".gitignore") | [.gitignore](https://github.com/plby/HopfProblem/blob/master/.gitignore ".gitignore") | [.](https://github.com/plby/HopfProblem/commit/cc698c96ee9502138139a0a0e2277a46721d3c94 ".") | Aug 27, 2026 |

| [Challenge.lean](https://github.com/plby/HopfProblem/blob/master/Challenge.lean "Challenge.lean") | [Challenge.lean](https://github.com/plby/HopfProblem/blob/master/Challenge.lean "Challenge.lean") | [.](https://github.com/plby/HopfProblem/commit/cc698c96ee9502138139a0a0e2277a46721d3c94 ".") | Aug 27, 2026 |

| [LICENSE](https://github.com/plby/HopfProblem/blob/master/LICENSE "LICENSE") | [LICENSE](https://github.com/plby/HopfProblem/blob/master/LICENSE "LICENSE") | [.](https://github.com/plby/HopfProblem/commit/cc698c96ee9502138139a0a0e2277a46721d3c94 ".") | Aug 27, 2026 |

| [README.md](https://github.com/plby/HopfProblem/blob/master/README.md "README.md") | [README.md](https://github.com/plby/HopfProblem/blob/master/README.md "README.md") | [.](https://github.com/plby/HopfProblem/commit/9ac8a456b526527837d7082ff775213ca8bc9809 ".") | Aug 27, 2026 |

| [Solution.lean](https://github.com/plby/HopfProblem/blob/master/Solution.lean "Solution.lean") | [Solution.lean](https://github.com/plby/HopfProblem/blob/master/Solution.lean "Solution.lean") | [.](https://github.com/plby/HopfProblem/commit/cc698c96ee9502138139a0a0e2277a46721d3c94 ".") | Aug 27, 2026 |

| [lake-manifest.json](https://github.com/plby/HopfProblem/blob/master/lake-manifest.json "lake-manifest.json") | [lake-manifest.json](https://github.com/plby/HopfProblem/blob/master/lake-manifest.json "lake-manifest.json") | [.](https://github.com/plby/HopfProblem/commit/cc698c96ee9502138139a0a0e2277a46721d3c94 ".") | Aug 27, 2026 |

| [lakefile.toml](https://github.com/plby/HopfProblem/blob/master/lakefile.toml "lakefile.toml") | [lakefile.toml](https://github.com/plby/HopfProblem/blob/master/lakefile.toml "lakefile.toml") | [.](https://github.com/plby/HopfProblem/commit/cc698c96ee9502138139a0a0e2277a46721d3c94 ".") | Aug 27, 2026 |

| [lean-toolchain](https://github.com/plby/HopfProblem/blob/master/lean-toolchain "lean-toolchain") | [lean-toolchain](https://github.com/plby/HopfProblem/blob/master/lean-toolchain "lean-toolchain") | [.](https://github.com/plby/HopfProblem/commit/cc698c96ee9502138139a0a0e2277a46721d3c94 ".") | Aug 27, 2026 | | View all files |

Repository files navigation

- README

- License

More items

Formalization of the solution to the Hopf problem

[](https://github.com/plby/HopfProblem#formalization-of-the-solution-to-the-hopf-problem)

The six-sphere admits a complex manifold structure compatible with its standard topology.

Based on _A compact complex threefold fibred by tori over the projective line, and the six-sphere_, originally shared on X by Levent Alpöge.

The repository includes a Comparator setup, with the statement adapted from the Formal Conjectures project.

undefinedshell lake update lake exe cache get lake build lean4export lake exe comparator comparator/config.json undefined

Type-check it online!

About

A formalization of the resolution of the Hopf problem: the six-sphere admits a complex manifold structure compatible with its standard topology

Resources

Readme

License

Activity

Stars

**61** stars

Watchers

**0** watching

Forks

**3** forks

Report repository

Releases

No releases published

Contributors1(1)

- **plby**Boris Alexeev

Languages

- Lean 100%

Footer

[](https://github.com/) © 2026 GitHub,Inc.

Footer navigation

- Terms

- Privacy

- Security

- Status

- Community

- Docs

- Contact

- Manage cookies

- Do not share my personal information

You can’t perform that action at this time.