List view

Baum–Connes conjecture

ams-19: K-theory

ams-46: Functional analysis

ams-47: Operator theory

needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.In order to formalise this conjecture, some major additions on top of mathlib are needed.

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2165 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 4, 2026

Unknotting Problem

ams-57: Manifolds and cell complexes

ams-68: Computer science

needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.In order to formalise this conjecture, some major additions on top of mathlib are needed.

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2166 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 4, 2026

Berge Conjecture (Dehn Surgery and Lens Spaces)

ams-54: General topology

ams-55: Algebraic topology

ams-57: Manifolds and cell complexes

needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.In order to formalise this conjecture, some major additions on top of mathlib are needed.

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2167 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 4, 2026

Zeeman's Conjecture: Collapsibility of Contractible 2-Polyhedron Products

ams-54: General topology

ams-55: Algebraic topology

ams-57: Manifolds and cell complexes

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2168 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 4, 2026

Nearby Lagrangian Conjecture

ams-53: Differential geometry

ams-57: Manifolds and cell complexes

ams-58: Global analysis + analysis on manifolds

needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.In order to formalise this conjecture, some major additions on top of mathlib are needed.

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2174 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 5, 2026

Bing-Borsuk conjecture

ams-54: General topology

ams-57: Manifolds and cell complexes

good first issueGood for newcomersGood for newcomers

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2185 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 6, 2026

Borel conjecture: Homotopy equivalence implies homeomorphism for closed manifolds

ams-54: General topology

ams-55: Algebraic topology

ams-57: Manifolds and cell complexes

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2186 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 6, 2026

Halperin Conjecture

ams-55: Algebraic topology

needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.In order to formalise this conjecture, some major additions on top of mathlib are needed.

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2187 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 6, 2026

Whitehead asphericity conjecture

ams-20 Group theory and generalizations

ams-55: Algebraic topology

ams-57: Manifolds and cell complexes

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2189 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 6, 2026

Quadrisecants of Wild Knots Conjecture

ams-57: Manifolds and cell complexes

needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.In order to formalise this conjecture, some major additions on top of mathlib are needed.

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2191 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 6, 2026

Volume Conjecture

ams-55: Algebraic topology

ams-57: Manifolds and cell complexes

ams-81: Quantum theory

needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.In order to formalise this conjecture, some major additions on top of mathlib are needed.

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2190 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 6, 2026

Telescope Conjecture (Ravenel)

ams-18: Category theory; homological algebra

ams-55: Algebraic topology

needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.In order to formalise this conjecture, some major additions on top of mathlib are needed.

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2192 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 6, 2026

Mazur's Conjecture 1: Zariski-density and topological closure of rational points

ams-11: Number theory

ams-14: Algebraic geometry

needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.In order to formalise this conjecture, some major additions on top of mathlib are needed.

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2193 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 6, 2026

Mazur's Conjecture 2: Topology of rational points on varieties

ams-11: Number theory

ams-14: Algebraic geometry

needs-prerequisitesIn order to formalise this conjecture, some major additions on top of mathlib are needed.In order to formalise this conjecture, some major additions on top of mathlib are needed.

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2194 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 6, 2026

Mazur's Conjecture 3: Finite connected components of rational points

ams-11: Number theory

ams-14: Algebraic geometry

ams-54: General topology

new conjectureIssues about open conjectures/unsolved problems problem. Category `research open`Issues about open conjectures/unsolved problems problem. Category `research open`

wikipedia

Status: Open.

#2195 In google-deepmind/formal-conjectures;

· franzhusch opened on Feb 6, 2026