openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance

Source · Project

Cite & export
Open this versionExport record · JSONRecord detailsReport a correction

Mathlib · wanted Poincaré statements

Mathlib contributors

Project documentation
View project ↗

Overview

Mathlib · wanted Poincaré statements

Source-backed selection; publication and proof assessment are separate.

1 cited passage ↓1 problem ↓Record 9454a4c25a2b923eb55dba3098f2d6ae0484d09b ↓

Passages

The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.

Passage 1 · OpenMath paraphrasePermalink

SimplyConnectedSpace.nonempty_homeomorph_sphere_three and nonempty_sdiffeomorph_sphere_three

This Mathlib revision declares the three-dimensional topological and smooth Poincaré statements with proof_wanted. These are formal statements seeking library proofs, not evidence of a completed proof in Mathlib.

Read at source ↗7 recorded uses ↓
Passage details

Passage ID: poincare-conjecture:entry:wanted-statements:v1

Source item: SimplyConnectedSpace.nonempty_homeomorph_sphere_three and nonempty_sdiffeomorph_sphere_three

Source record: mathlib-poincare-wanted@9454a4c25a2b923eb55dba3098f2d6ae0484d09b

Used in

Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.

Poincaré conjecture →

Problem publication v13

The topological three-dimensional Poincaré theorem →

Formal declaration

Topological statement · Mathlib wanted theorem

Statement v2 →Inspect formal evidence ↓

Scope

The topological three-dimensional Poincaré theorem

Statement v2 →

Statement

Statement v2 →

The smooth three-dimensional theorem →

Formal declaration

Smooth statement · Mathlib wanted theorem

Statement v2 →Inspect formal evidence ↓

Scope

The smooth three-dimensional theorem

Statement v2 →

Statement

Statement v2 →
Problem context · 1 citations

Question

Poincaré conjecture

View in problem →

Files

Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.

Formal declarations

Topological statement · Mathlib wanted theorem ↗

Statement only · proof not supplied in this source

This revision uses proof_wanted for the exact statement. A wanted declaration is not a completed Mathlib proof; the external projects above have separate source and verification evidence.

Statement match: Candidate correspondence · not independently confirmed · checked Oct 12, 2026

Declaration & revision
SimplyConnectedSpace.nonempty_homeomorph_sphere_three

Commit 9454a4c25a2b923eb55dba3098f2d6ae0484d09b

Smooth statement · Mathlib wanted theorem ↗

Statement only · proof not supplied in this source

This revision uses proof_wanted for the exact statement. A wanted declaration is not a completed Mathlib proof; the external projects above have separate source and verification evidence.

Statement match: Candidate correspondence · not independently confirmed · checked Oct 12, 2026

Declaration & revision
SimplyConnectedSpace.nonempty_sdiffeomorph_sphere_three

Commit 9454a4c25a2b923eb55dba3098f2d6ae0484d09b

Credits

Recorded authorship

Mathlib contributors

AI involvement not reported

AI use is not reported in the selected source.

Versions

OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.

  1. 9454a4c25a2b923eb55dba3098f2d6ae0484d09b · selectedObserved Oct 12, 2026 · used in current publications

    Mathlib · wanted Poincaré statements

Record details
Source ID
mathlib-poincare-wanted
Record ID
mathlib-poincare-wanted@9454a4c25a2b923eb55dba3098f2d6ae0484d09b
Recorded title
Mathlib · wanted Poincaré statements
Revision
9454a4c25a2b923eb55dba3098f2d6ae0484d09b
Observed
Oct 12, 2026
Source updated
Not recorded
Content SHA-256
Not recorded
Update method
Manual source review; publish new observations with immutable versions
Identifier policy
Source revision plus exact passage or declaration; no fuzzy identity merge
Check interval
90 days
Rights
metadata-link
License
Metadata, links and original OpenMath paraphrases only

Follow the original source for authoritative statements and reuse terms.

Source terms ↗