arXiv subjects

Mohammed Abouzaid

Publications and source records attributed to Mohammed Abouzaid.

At least 19 recordsLinked to original sources

arXiv2026

Pseudo-Formalization for Automatic Proof Verification

Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to verify because they are unambiguous and modular. Most proofs, particularly those written by AI systems, have neither property, and translating them into formal languages remains challenging in many frontier math settings. We propose Pseudo-Formalization (PF), a proof format that captures the modularity and precision of formal proofs while retaining the flexibility of natural language. A Pseudo-Formal proof is decomposed into self-contained modules, each stating its premises, conclusion, and proof in natural language. To verify the correctness of a regular natural language proof, an LLM translates it to Pseudo-Formal and then verifies each module independently, an algorithm we call Block Verification (BV). We evaluate PF+BV on two benchmarks spanning olympiad and research-level mathematics, where it pareto-dominates LLM-as-judge baselines on error-finding precision and recall. To support future work, we release our research-level proof verification benchmark ArxivMathGradingBench.

cs.LO↗

arXiv2026

First Proof Second Batch

To assess the ability of current AI systems to correctly solve research-level mathematics problems, we tested several AI systems on a set of ten problems in a broad range of mathematical fields; these problems arose naturally in the research process of the contributors. This document includes the problems, our methodology, and the results of our testing. We provide links to supplementary documents including the human solutions, the AI-generated solutions, and the referee reports and logs for the AI-generated solutions. The ten problems were contributed by the following mathematicians: (1) Dariusz Kalociński and Theodore A. Slaman, (2) Richard Schwartz, (3) Aleksa Milojevic and Benny Sudakov, (4) Larry Guth, (5) Oleg Butkovsky, Jonathan Mattingly, and Lorenzo Zambotti, (6) Joshua Evan Greene and Duncan McCoy, (7) Sucharit Sarkar, (8) Sam Payne and Jidong (Jayden) Wang, (9) Sylvie Corteel and John Lentfer, (10) Srivatsav Kunnawalkam Elayavalli.

cs.AI↗

arXiv2026

First Proof

To assess the ability of current AI systems to correctly answer research-level mathematics questions, we share a set of ten math questions which have arisen naturally in the research process of the authors. The questions had not been shared publicly until now; the answers are known to the authors of the questions but will remain encrypted for a short time.

cs.AI↗

arXiv2025

Normal invariant of nearby Lagrangians via twisted derivative

Let $L$ and $M$ be closed, connected, smooth manifolds and let $L \hookrightarrow T^*M$ be an exact Lagrangian embedding. The induced map $L \to M$ is known by earlier work to be a homotopy equivalence. We show that the associated normal invariant $M \to G/O$ factors through a map $B(\mathcal{T},\mathcal{Q}) \to G/O$ which is a twisted version of the Waldhausen derivative $\mathcal{T} \to G$ on the space $\mathcal{T}$ of tubes. Further, we show that this twisted derivative map itself factors though a map $B(G/O) \to G/O$ which is a twisted version of the $S$-duality map $BG \to G$. In particular we deduce that the normal invariant of the homotopy equivalence $L \to M$ is 2-torsion.

math.SG↗

arXiv2025

Canonical orientations in Heegaard Floer theory

We set up Heegaard Floer theory over the integers, using canonical orientations coming from coupled Spin structures on the Lagrangian tori. We prove naturality of Heegaard Floer homology, sutured Floer homology, and link Floer homology over $\mathbb{Z}$. We give a new proof of the surgery exact triangle in this context, as well as a definition of involutive Heegaard Floer homology over $\mathbb{Z}$.

math.GT↗

arXiv2025

Nearby Special Lagrangians

Let $X$ be a Calabi--Yau manifold and $Q\subset X$ a closed connected embedded special Lagrangian; closed Lagrangians mean compact Lagrangian submanifolds without boundary. We prove that if the fundamental group $π_1Q$ is abelian then there exists a Weinstein neighbourhood of $Q\subset X$ in which every closed irreducibly immersed special Lagrangian with unobstructed Floer cohomology is $C^1$ close to $Q.$ We prove also that if $π_1Q$ is virtually solvable then for every positive integer $R$ there exists a Weinstein neighbourhood of $Q\subset X$ in which every closed irreducibly immersed special Lagrangian of degree $\le R$ and with unobstructed Floer cohomology is unbranched; that is, the projection $L\to Q$ is a covering map. We prove a stronger statement when $π_1Q$ is finite and a weaker statement when $π_1Q$ has no non-abelian free subgroups. The $π_1Q$ conditions, the Floer cohomology condition and the special Lagrangian condition are all essential as we show by counterexamples.

math.SG↗

arXiv2025

Bordism and resolution of singularities

We adapt algorithms for resolving the singularities of complex algebraic varieties to prove that the natural map of homology theories from complex bordism to the bordism theory of complex derived orbifolds splits. In equivariant stable homotopy theory, our techniques yield a splitting of homology theories for the map from bordism to the equivariant bordism theory of a finite group $Γ$, given by assigning to a manifold its product with $Γ$. In symplectic topology, and using recent work of Abouzaid-McLean-Smith and Hirschi-Swaminathan, we conclude that one can define complex cobordism-valued Gromov-Witten invariant for arbitrary (closed) symplectic manifolds. We apply our results to constrain the topology of the space of Hamiltonian fibrations over $S^2$. The methods we develop apply to normally complex orbifolds, and will hence lead to applications in symplectic topology that rely on moduli spaces of holomorphic curves with Lagrangian boundary conditions.

math.AT↗

arXiv2024

The focus-focus addition graph is immersed

For a symplectic 4-manifold $M$ equipped with a singular Lagrangian fibration with a section, the natural fiberwise addition given by the local Hamiltonian flow is well-defined on the regular points. We prove, in the case that the singularities are of focus-focus type, that the closure of the corresponding addition graph is the image of a Lagrangian immersion in $(M \times M)^- \times M$, and we study its geometry. Our main motivation for this result is the construction of a symmetric monoidal structure on the Fukaya category of such a manifold.

math.SG↗

arXiv2024

Foundation of Floer homotopy theory I: Flow categories

We construct a stable infinity category with objects flow categories and morphisms flow bimodules; our construction has many flavors, related to a choice of bordism theory, and we discuss in particular framed bordism and the bordism theory of complex oriented derived orbifolds. In this setup, the construction of homotopy types associated to Floer-theoretic data is immediate: the moduli spaces of solutions to Floer's equation assemble into a flow category with respect to the appropriate bordism theory, and the associated Floer homotopy types arise as suitable mapping spectra in this category. The definition of these mapping spectra is sufficiently explicit to allow a direct interpretation of the Floer homotopy groups as Floer bordism groups. In the setting of framed bordism, we show that the category we construct is a model for the category of spectra. We implement the construction of Floer homotopy types in this new formalism for the case of Hamiltonian Floer theory.

math.SG↗

arXiv2024

Twisted generating functions and the nearby Lagrangian conjecture

We prove that, for closed exact embedded Lagrangian submanifolds of cotangent bundles, the homomorphism of homotopy groups induced by the stable Lagrangian Gauss map vanishes. In particular, we prove that this map is null-homotopic for all spheres. The key tool that we introduce in order to prove this is the notion of twisted generating function and we show that every closed exact Lagrangian can be described using such an object, by extending a doubling argument developed in the setting of sheaf theory. Floer theory and sheaf theory constrain the type of twisted generating functions that can appear to a class which is closely related to Waldhausen's tube space, and our main result follows by a theorem of Bökstedt which computes the rational homotopy type of the tube space.

math.SG↗

arXiv2024

Gromov-Witten invariants in complex and Morava-local $K$-theories

Given a closed symplectic manifold $X$, we construct Gromov-Witten-type invariants valued both in (complex) $K$-theory and in any complex-oriented cohomology theory $\mathbb{K}$ which is $K_p(n)$-local for some Morava $K$-theory $K_p(n)$. We show that these invariants satisfy a version of the Kontsevich-Manin axioms, extending Givental and Lee's work for the quantum $K$-theory of complex projective algebraic varieties. In particular, we prove a Gromov-Witten type splitting axiom, and hence define quantum $K$-theory and quantum $\mathbb{K}$-theory as commutative deformations of the corresponding (generalised) cohomology rings of $X$; the definition of the quantum product involves the formal group of the underlying cohomology theory. The key geometric input to these results is a construction of global Kuranishi charts for moduli spaces of stable maps of arbitrary genus to $X$. On the algebraic side, in order to establish a common framework covering both ordinary $K$-theory and $K_p(n)$-local theories, we introduce a formalism of `counting theories' for enumerative invariants on a category of global Kuranishi charts.

math.SG↗

arXiv2024

Framed $E_2$ structures in Floer theory

We resolve the long-standing problem of constructing the action of the operad of framed (stable) genus-$0$ curves on Hamiltonian Floer theory; this operad is equivalent to the framed $E_2$ operad. We formulate the construction in the following general context: we associate to each compact subset of a closed symplectic manifold a new chain-level model for symplectic cohomology with support, which we show carries an action of a model for the chains on the moduli space of framed genus $0$ curves. This construction turns out to be strictly functorial with respect to inclusions of subsets, and the action of the symplectomorphism group. In the general context, we appeal to virtual fundamental chain methods to construct the operations over fields of characteristic $0$, and we give a separate account, over arbitrary rings, in the special settings where Floer's classical transversality approach can be applied. We perform all constructions over the Novikov ring, so that the algebraic structures we produce are compatible with the quantitative information that is contained in Floer theory. Over fields of characteristic $0$, our construction can be combined with results in the theory of operads to produce explicit operations encoding the structure of a homotopy $BV$ algebra. In an appendix, we explain how to extend the results of the paper from the class of closed symplectic manifolds to geometrically bounded ones.

math.SG↗

arXiv2023

Monotone Lagrangians in cotangent bundles of spheres

We study the compact monotone Fukaya category of $T^*S^n$, for $n\geq 2$, and show that it is split-generated by two classes of objects: the zero-section $S^n$ (equipped with suitable bounding cochains) and a 1-parameter family of monotone Lagrangian tori $(S^1\times S^{n-1})_τ$, with monotonicity constants $τ>0$ (equipped with rank 1 unitary local systems). As a consequence, any closed orientable spin monotone Lagrangian (possibly equipped with auxiliary data) with non-trivial Floer cohomology is non-displaceable from either $S^n$ or one of the $(S^1\times S^{n-1})_τ$. In the case of $T^*S^3$, the monotone Lagrangians $(S^1\times S^2)_τ$ can be replaced by a family of monotone tori $T^3_τ$.

math.SG↗

arXiv2023

Homological mirror symmetry for hypersurfaces in $(\mathbb{C}^*)^n$

We prove a homological mirror symmetry result for maximally degenerating families of hypersurfaces in $(\mathbb{C}^*)^n$ (B-model) and their mirror toric Landau-Ginzburg A-models. The main technical ingredient of our construction is a "fiberwise wrapped" version of the Fukaya category of a toric Landau-Ginzburg model. With the definition in hand, we construct a fibered admissible Lagrangian submanifold whose fiberwise wrapped Floer cohomology is isomorphic to the ring of regular functions of the hypersurface. It follows that the derived category of coherent sheaves of the hypersurface quasi-embeds into the fiberwise wrapped Fukaya category of the mirror. We also discuss an extension to complete intersections.

math.SG↗

arXiv2022

An axiomatic approach to virtual chains

We introduce a category of Kuranishi presentations, whose objects are a variant of the Kuranishi structures introduced by Fukaya and Ono, and which can be seen as a refinement of the version studied by Pardon. We then formulate the notion of virtual chains categorically as a natural transformation between two functors from this category to the category of chain complexes; we call such a datum 'a theory of virtual counts'. To show that this definition carries non-trivial content, we then construct a multicategory whose objects are Kuranishi flow categories, and show that a theory of virtual counts determines a multifunctor to the multicategory of chain complexes. We then implement this construction in the setting of Hamiltonian Floer theory, borrowing from some joint work with Groman and Varolgunes, yielding a construction of Hamiltonian Floer groups (and operations on them) as an output of this machine. We plan to provide a similar account for Lagrangian Floer theory in subsequent joint work.

math.SG↗

arXiv2022

Functoriality in categorical symplectic geometry

Categorical symplectic geometry is the study of a rich collection of invariants of symplectic manifolds, including the Fukaya $A_\infty$-category, Floer cohomology, and symplectic cohomology. Beginning with work of Wehrheim and Woodward in the late 2000s, several authors have developed techniques for functorial manipulation of these invariants. We survey these functorial structures, including Wehrheim-Woodward's quilted Floer cohomology and functors associated to Lagrangian correspondences, Fukaya's alternate approach to defining functors between Fukaya $A_\infty$-categories, and the second author's ongoing construction of the symplectic $(A_\infty,2)$-category. In the last section, we describe a number of direct and indirect applications of this circle of ideas, and propose a conjectural version of the Barr-Beck Monadicity Criterion in the context of the Fukaya $A_\infty$-category.

math.SG↗

arXiv2022

The Gamma and Strominger-Yau-Zaslow conjectures: a tropical approach to periods

We propose a new method to compute asymptotics of periods using tropical geometry, in which the Riemann zeta values appear naturally as error terms in tropicalization. Our method suggests how the Gamma class should arise from the Strominger-Yau-Zaslow conjecture. We use it to give a new proof of (a version of) the Gamma Conjecture for Batyrev pairs of mirror Calabi-Yau hypersurfaces.

math.AG↗

arXiv2021

Complex cobordism, Hamiltonian loops and global Kuranishi charts

Let $(X,ω)$ be a closed symplectic manifold. A loop $ϕ: S^1 \to \mathrm{Diff}(X)$ of diffeomorphisms of $X$ defines a fibration $π: P_ϕ \to S^2$. By applying Gromov-Witten theory to moduli spaces of holomorphic sections of $π$, Lalonde, McDuff and Polterovich proved that if $ϕ$ lifts to the Hamiltonian group $\mathrm{Ham}(X,ω)$, then the rational cohomology of $P_ϕ$ splits additively. We prove, with the same assumptions, that the $\mathbb{E}$-generalised cohomology of $P_ϕ$ splits additively for any complex-oriented cohomology theory $\mathbb{E}$, in particular the integral cohomology splits. This class of examples includes all complex projective varieties equipped with a smooth morphism to $\mathbb{CP}^1$, in which case the analogous rational result was proved by Deligne using Hodge theory. The argument employs virtual fundamental cycles of moduli spaces of sections of $π$ in Morava $K$-theory and results from chromatic homotopy theory. Our proof involves a construction of independent interest: we build global Kuranishi charts for moduli spaces of pseudo-holomorphic spheres in $X$ in a class $β\in H_2(X;\mathbb{Z})$, depending on a choice of integral symplectic form $Ω$ on $X$ and ample Hermitian line bundle over the moduli space of one-pointed degree $d = \langle Ω,β\rangle$ stable genus zero curves in $\mathbb{CP}^d$.

math.SG↗