Nearby Lagrangian Conjecture

### What is the conjecture

Let $M$ be a closed manifold and let $T^*M$ denote its cotangent bundle, which carries a canonical symplectic structure. A Lagrangian submanifold of $T^*M$ is a submanifold $L \subseteq T^*M$ on which the symplectic form vanishes and which is maximal with this property. An exact Lagrangian submanifold is one where the Liouville form restricts to an exact differential form on $L$. The zero section of $T^*M$ (the image of the zero map $M \to T^*M$) is a Lagrangian submanifold.

The **Nearby Lagrangian Conjecture** states that every closed exact Lagrangian submanifold $L$ of $T^*M$ is Hamiltonian isotopic to the zero section of $T^*M$. That is, there exists a Hamiltonian isotopy (a one-parameter family of Hamiltonian diffeomorphisms) that transforms $L$ into the zero section.

**Current Status:** The conjecture is known to hold for $M = S^1$ (the circle) and $M = S^2$ (the sphere). Recent work has shown that any closed connected exact Lagrangian manifold in a cotangent bundle is a homotopy equivalence to the zero section, but the full Hamiltonian isotopy statement remains open for manifolds of dimension $\geq 3$.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Nearby_Lagrangian_conjecture, https://arxiv.org/abs/2011.13178, https://arxiv.org/abs/1107.4674, https://arxiv.org/abs/2211.15802

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-02-05)

Building blocks (1-3; from search results):
- `SmoothManifold`, `CotangentBundle` (foundational structures in Mathlib for differential geometry)
- Manifold and submanifold types with smooth structure

Missing pieces (exactly 2; unclear/absent from search results):
- Symplectic form and symplectic manifold structures (not yet in Mathlib as of recent searches)
- Lagrangian submanifold definition, Hamiltonian isotopy, and exact Lagrangian conditions (symplectic topology not formalized)

Rating justification (1-2 sentences): While Mathlib has strong differential geometry foundations (smooth manifolds, tangent/cotangent bundles), symplectic geometry—including symplectic forms, Lagrangian submanifolds, and Hamiltonian flows—has not been substantially formalized in the library. Stating the conjecture requires developing core symplectic structures and Lagrangian submanifold theory.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-53
* ams-57
* ams-58

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)