Formalised definitions of Kuranishi structures, polyfolds, d-manifolds and/or implicit atlas might be useful, along with the associated construction of virtual fundamental class or chain. These are all structures that exist on various moduli spaces of pseudoholomorphic curves in symplectic geometry, and allow us to extract invariants.

I would guess that a proof that these structures actually exist on moduli spaces is probably too hard for most current theorem assistants, but already a formal definition might help to clarify various things: the definitions are extremely subtle, and the experts often exchange lengthy papers which illuminate or query different aspects of the definitions.

You should probably do manifolds first, though, if you haven't already...