FOM: Poincare conjecture

[JOE SHIPMAN, BLOOMBERG/ SKILLMAN]

Jan Mycielski points out that the Poincare conjecture is equivalent to a pi^0_1
sentence because of recent work by Rubinstein establishing the algorithmic
decidability of the 3-sphere (finitely presented as e.g. a simplicial
complexes).  That is, given a simplicial complex we can effectively recognize
whether its underlying topological space is homeomorphic to the 3-sphere.
A corollary is that 4-manifolds are effectively recognizable (the hard part in
recognizing that a simplicial complex is a 4-manifold is proving that the
boundary of a neighborhood of a vertex is a 3-sphere).  I don't know how strong
a system you need to prove Rubinstein's theorem but we at least know that the
Poincare Conjecture is pi^0_1 over ZF, and that if it is false it can be
finitely refuted (just like the Riemann hypothesis).  -- Joe Shipman