pith. sign in

arxiv: 2604.23211 · v1 · submitted 2026-04-25 · 🧮 math.CO · cs.LO· math.AG

Formalizing A₁⁽¹⁾ Curve Neighborhoods in Lean 4

Yihe Huang , Sizhe Cui , Jiaqi Wang , Jujian Zhang This is my paper

Pith reviewed 2026-05-08 07:51 UTC · model grok-4.3

classification 🧮 math.CO cs.LOmath.AG
keywords Lean 4formalizationcurve neighborhoodsCoxeter systeminfinite dihedral groupaffine flag manifoldsquantum Schubert calculuscombinatorial formulas
0
0 comments X

The pith

Lean 4 formalizes curve neighborhoods for A1^(1) by characterizing them as maximal vertices in reachable sets of the infinite dihedral group.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a complete, axiom-free formalization in Lean 4 of combinatorial curve neighborhoods used in quantum Schubert calculus for affine flag manifolds of type A1^(1). It encodes the neighborhoods directly in the moment graph of the infinite dihedral group D_infty by treating the group as a Coxeter system, which permits explicit computation of length functions and degree maps. Reachable sets are built from edge chains subject to degree bounds, and the neighborhoods are identified with the maximal vertices inside those sets. A reader would care because the work verifies explicit combinatorial formulas for arbitrary elements and produces a computable version by restricting search spaces to finite sets, removing reliance on unverified identities in this foundational setting.

Core claim

By formalizing D_infty directly as a Coxeter system in Lean 4, the paper demonstrates that curve neighborhoods equal the maximal vertices contained in reachable sets constructed from degree-bounded edge chains, thereby confirming the explicit combinatorial formulas for every element and allowing extraction of a fully computable version through finite restriction.

What carries the argument

The Coxeter system realization of the infinite dihedral group D_infty in Lean 4, with curve neighborhoods defined as the maximal vertices inside reachable sets obtained from edge chains bounded by specific degrees.

If this is right

  • Explicit combinatorial formulas for curve neighborhoods of arbitrary elements receive full verification in Lean 4.
  • A computable version of the neighborhoods becomes available by restricting the search space to finite sets.
  • Length functions and degree maps are computed explicitly inside the formal Coxeter system.
  • Verified neighborhoods supply a reliable foundation for setting up quantum Schubert calculus on affine flag manifolds in type A1^(1).

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same pattern of formalizing a Coxeter system and extracting maximal vertices from bounded reachable sets could be applied to other affine types to verify their curve neighborhoods.
  • The finite-set extraction indicates that the neighborhoods can be turned into efficient algorithms outside proof assistants for concrete calculations.
  • Verified neighborhoods open the possibility of automated checks for further combinatorial properties arising in quantum cohomology.

Load-bearing premise

The Lean definitions of reachable sets through bounded edge chains and the maximal vertices inside them coincide exactly with the curve neighborhoods defined mathematically by Mihalcea and Norton.

What would settle it

Select any concrete element of D_infty, compute its curve neighborhood via the formalized maximal vertices, and compare the result against an independent manual calculation or a known tabulated example; mismatch on even one element would disprove the formalization's correctness.

read the original abstract

Combinatorial curve neighborhoods are somewhat foundational when setting up the quantum Schubert calculus for affine flag manifolds. In the specific case of type $A_1^{(1)}$, you can encode these neighborhoods entirely within the moment graph of the infinite dihedral group $D_\infty$. Building on the framework developed by Mihalcea and Norton, this paper presents a complete, axiom-free formalization of these combinatorial curve neighborhoods in Lean 4. Rather than just wrapping mathematical statements, we formalized $D_\infty$ directly as a Coxeter system to explicitly compute length functions and degree maps. Reachable sets are defined through edge chains bounded by specific degrees, and we ultimately characterize the curve neighborhood by the maximal vertices inside these sets. The core effort here lies in formally verifying the explicit combinatorial formulas for curve neighborhoods of arbitrary elements. Interestingly, by restricting our search space to finite sets, we also managed to extract a fully computable version of these neighborhoods.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript presents a complete, axiom-free formalization in Lean 4 of combinatorial curve neighborhoods for the A_1^{(1)} case of affine flag manifolds. Building on Mihalcea and Norton, it directly encodes the infinite dihedral group D_∞ as a Coxeter system to compute length functions and degree maps on the moment graph, defines reachable sets via finite edge chains whose degrees are bounded by a given element, and characterizes the curve neighborhood as the set of maximal vertices inside those reachable sets. The core contribution is the formal verification of explicit combinatorial formulas for arbitrary elements, together with extraction of a fully computable version obtained by restricting search spaces to finite sets.

Significance. If the Lean constructions coincide with the Mihalcea-Norton combinatorial objects, the work supplies a machine-checked, computable foundation for quantum Schubert calculus in this affine type. The direct formalization of D_∞ as a Coxeter system (without ad-hoc axioms) and the extraction of executable code for the neighborhoods are clear strengths that enhance reproducibility and allow direct computation of examples.

major comments (2)
  1. [Abstract / characterization section] Abstract and the section describing the characterization of curve neighborhoods: the manuscript states that reachable sets and maximal vertices 'characterize the curve neighborhood' but contains no explicit theorem or lemma of the form '∀ w, curve_neighborhood w = {v | v maximal in reachable_set(w)}' together with a proof that this Lean predicate coincides with the combinatorial definition given by Mihalcea and Norton. Because D_∞ is infinite, any divergence in the degree bound or maximality condition would produce a different object for sufficiently long elements while all internal Lean proofs remain valid; this equivalence is load-bearing for the central claim of having formalized the same object.
  2. [Reachable sets and curve neighborhood characterization] The formalization of reachable sets (edge chains bounded by specific degrees): the paper defines these sets directly in Lean but does not supply a lemma establishing that the resulting maximal-vertex sets are identical to the curve neighborhoods in the Mihalcea-Norton framework for all elements of D_∞. Without such a statement, the formalization, while internally consistent, does not yet confirm that its output matches the mathematical object studied in the literature.
minor comments (1)
  1. [Abstract] The abstract refers to 'explicit verification of the explicit combinatorial formulas' but the manuscript would benefit from a short table or list in the main text indicating precisely which formulas (e.g., for length, degree, or neighborhood size) were verified and for which classes of elements.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and constructive feedback. We appreciate the acknowledgment of the strengths in our direct formalization of D_∞ as a Coxeter system and the extraction of computable code. We address the major comments point by point below.

read point-by-point responses

  1. Referee: [Abstract / characterization section] Abstract and the section describing the characterization of curve neighborhoods: the manuscript states that reachable sets and maximal vertices 'characterize the curve neighborhood' but contains no explicit theorem or lemma of the form '∀ w, curve_neighborhood w = {v | v maximal in reachable_set(w)}' together with a proof that this Lean predicate coincides with the combinatorial definition given by Mihalcea and Norton. Because D_∞ is infinite, any divergence in the degree bound or maximality condition would produce a different object for sufficiently long elements while all internal Lean proofs remain valid; this equivalence is load-bearing for the central claim of having formalized the same object.

    Authors: We agree that an explicit lemma establishing the equivalence is necessary to make the connection to the Mihalcea-Norton definition fully rigorous, particularly to address potential concerns in the infinite case. While the manuscript characterizes the curve neighborhoods via maximal vertices in the degree-bounded reachable sets and verifies the explicit combinatorial formulas for arbitrary elements, it does not contain a dedicated theorem of the requested form. In the revised manuscript we will add such a lemma in the characterization section, together with a proof that our Lean predicate coincides with the literature definition for all w in D_∞, leveraging the direct encoding of length functions and degree maps. revision: yes

  2. Referee: [Reachable sets and curve neighborhood characterization] The formalization of reachable sets (edge chains bounded by specific degrees): the paper defines these sets directly in Lean but does not supply a lemma establishing that the resulting maximal-vertex sets are identical to the curve neighborhoods in the Mihalcea-Norton framework for all elements of D_∞. Without such a statement, the formalization, while internally consistent, does not yet confirm that its output matches the mathematical object studied in the literature.

    Authors: We acknowledge that the manuscript defines reachable sets via finite edge chains with bounded degrees and extracts maximal vertices, but does not include an explicit lemma proving identity with the Mihalcea-Norton curve neighborhoods for every element. The core contribution of verifying the combinatorial formulas is intended to ensure agreement, and the computable restriction to finite search spaces already allows direct checking. In the revision we will add a theorem stating that the maximal-vertex sets equal the curve neighborhoods in the Mihalcea-Norton framework for all elements of D_∞, supported by the axiom-free Coxeter system formalization. revision: yes

Circularity Check

0 steps flagged

No circularity: Lean formalization implements external combinatorial definitions without reduction to inputs by construction

full rationale

The paper directly encodes the infinite dihedral group D_∞ as a Coxeter system inside Lean, then defines reachable sets via explicit edge-chain predicates bounded by degree and extracts curve neighborhoods as the maximal vertices in those sets. These constructions are presented as the formalization of the Mihalcea-Norton combinatorial formulas rather than as a derived prediction from fitted data or prior self-citations. Because the work is a machine-checked implementation against the standard Lean library and an external cited framework, with no equations shown to equal their own inputs by definition and no load-bearing self-citation chains, the derivation chain remains independent. The absence of an explicit equivalence lemma in the provided abstract does not create circularity under the stated criteria, as the formalization itself constitutes the verification step.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper describes the formalization as axiom-free and relies on standard definitions of Coxeter systems, moment graphs, and poset operations already present in the Lean mathlib library. No free parameters, ad-hoc axioms, or new invented entities are introduced.

pith-pipeline@v0.9.0 · 5471 in / 1346 out tokens · 34184 ms · 2026-05-08T07:51:15.001381+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

5 extracted references · 5 canonical work pages

  1. [1]

    Journal of Differential Geometry99(2), 255–283 (2015) 8 Yihe Huang, Sizhe Cui, Jiaqi Wang, and Jujian Zhang

    Buch, A., Mihalcea, L.C.: Curve neighborhoods of Schubert varieties. Journal of Differential Geometry99(2), 255–283 (2015) 8 Yihe Huang, Sizhe Cui, Jiaqi Wang, and Jujian Zhang

    work page 2015

  2. [2]

    In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (2020)

    mathlib Community, T.: The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (2020). https://doi.org/10.1145/3372885.3373824

    work page doi:10.1145/3372885.3373824 2020

  3. [3]

    arXiv preprint (2014), arXiv preprint (2014)

    Mare, L., Mihalcea, L.C.: An affine quantum cohomology ring for flag manifolds and the periodic toda lattice. arXiv preprint (2014), arXiv preprint (2014)

    work page 2014

  4. [4]

    Involve, a Journal of Mathematics10(2), 317–325 (2017)

    Mihalcea, L.C., Norton, T.: Combinatorial curve neighborhoods for the affine flag manifold of typeA(1) 1 . Involve, a Journal of Mathematics10(2), 317–325 (2017)

    work page 2017

  5. [5]

    In: Fodor, P., Montali, M., Calvanese, D., Roman, D

    de Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Automated Deduction – CADE 28 (2021). https://doi.org/10.1007/978-3-030- 79876-5_37

    work page doi:10.1007/978-3-030- 2021