Revision #1111 → #2438 · back to history
modifiedPoincaré conjecture (overview)a824a769c8f8
| Field | From #1111 | To #2438 |
|---|
| note | The 3-sphere characterization is stated as a `proof_wanted` declaration in Mathlib's PoincareConjecture file (statement present, proof not formalized). | The 3-sphere characterization is stated as a `proof_wanted` declaration in Mathlib's PoincareConjecture file (statement present, proof not formalized). (Mathlib declares this as `proof_wanted` — stated, not yet proven.) |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |
modifiedStatement of the Poincaré conjecturef111d3769a84
| Field | From #1111 | To #2438 |
|---|
| note | This exact statement (simply connected compact 3-manifold ≃ₜ 𝕊³) appears as a `proof_wanted` in Mathlib, formalized but unproven. | This exact statement (simply connected compact 3-manifold ≃ₜ 𝕊³) appears as a `proof_wanted` in Mathlib, formalized but unproven. (Mathlib declares this as `proof_wanted` — stated, not yet proven.) |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |
modifiedHomotopy form of the Poincaré conjecture4eec7ee18e59
| Field | From #1111 | To #2438 |
|---|
| note | The homotopy-equivalence form (`M ≃ₕ 𝕊ⁿ → Nonempty (M ≃ₜ 𝕊ⁿ)`) is stated as a `proof_wanted` generalized over all dimensions n, of which n=3 is this case. | The homotopy-equivalence form (`M ≃ₕ 𝕊ⁿ → Nonempty (M ≃ₜ 𝕊ⁿ)`) is stated as a `proof_wanted` generalized over all dimensions n, of which n=3 is this case. (Mathlib declares this as `proof_wanted` — stated, not yet proven.) |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |