Weinstein conjecture in dimension three (Taubes 2007)

weinstein_conjecture_dim3 — a formalization challenge from the lean-eval benchmark.

Notes

Every Reeb vector field of a contact form on a closed smooth 3-manifold has a closed periodic orbit. Mathlib lacks contact-geometry API and a manifold exterior derivative, so the encoding fixes dα by the intrinsic coordinate-free identity dα(X, Y) = X(α(Y)) − Y(α(X)) − α([X, Y]) (which uniquely determines dα from α via mathlib's mfderiv + VectorField.mlieBracket), and uses the equivalent dimension-3 contact condition α ≠ 0 ∧ dα nondegenerate on ker α in place of α ∧ dα ≠ 0. [I.Boundaryless] is essential: on the cube [0,1]³ with α = dz + x·dy, every Reeb integral curve has affine z-component with |z'| = 1 and escapes the cube, so closed orbits do not exist without the boundaryless hypothesis. §141 of Knill's Some Fundamental Theorems in Mathematics.

Formal statement

/-- **Weinstein conjecture in dimension three** (Taubes 2007). Every
Reeb vector field of a contact form on a closed smooth 3-manifold has
a closed periodic orbit. -/
theorem weinstein_conjecture_dim_three
    (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E']
    [FiniteDimensional ℝ E']
    (H' : Type*) [TopologicalSpace H']
    (I' : ModelWithCorners ℝ E' H')
    (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M']
    [T2Space M'] [CompactSpace M'] [Nonempty M'] [Fact (Module.finrank ℝ E' = 3)]
    [I'.Boundaryless]
    (α : OneForm I' (M := M')) (dα : TwoForm I' (M := M'))
    (R : ∀ x : M', TangentSpace I' x)
    (_hcontact : IsContactForm3 I' α dα)
    (_hReeb : IsReebVectorField I' α dα R) :
    HasClosedReebOrbit I' R := by
  sorry

Informal solution sketch

Taubes proves the three-dimensional Weinstein conjecture using Seiberg–Witten theory, relating large-parameter solutions of the Seiberg–Witten equations on Y × ℝ associated to a contact form to Reeb dynamics. If a closed contact 3-manifold had no closed Reeb orbit, the large-r analysis of the deformed Seiberg–Witten equations would contradict the nonvanishing input from Seiberg–Witten Floer homology / embedded contact homology in the relevant Spin^c structure. Mathlib has the smooth-manifold infrastructure used to state the problem (smooth manifolds, tangent spaces, mfderiv, Lie brackets) but not the contact-geometry, Reeb-dynamics, Seiberg–Witten, or embedded-contact-homology machinery needed to prove it.

Source

C.H. Taubes, 'The Seiberg–Witten equations and the Weinstein conjecture', Geom. Topol. 11 (2007) 2117–2202; arXiv:math/0611007. Conjecture: A. Weinstein, 'On the hypotheses of Rabinowitz' periodic orbit theorems', J. Differential Equations 33 (1979) 353–358. §141 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: weinstein_conjecture_dim_three
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.