Catalan generating function via compositional inversion

substInv_X_sub_X_sq_eq_catalan

Submitter: Kim Morrison.

Notes: The compositional inverse of X - X² is the generating function for Catalan numbers. This is a classical application of Lagrange inversion in enumerative combinatorics, connecting formal power series inversion to Dyck paths, binary trees, and triangulations.

Source: E. Catalan, Note sur une équation aux différences finies, 1838; J.-L. Lagrange, Nouvelle méthode pour résoudre les équations littérales, 1770.

Informal solution: The compositional inverse C(x) satisfies C - C² = x, giving C = (1 - √(1-4x))/2. By the binomial series, its coefficients are the Catalan numbers C_n = (2n choose n)/(n+1).

theorem declaration uses `sorry`substInv_X_sub_X_sq_eq_catalan (n : ℕ) :
    haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := byn:ℕ⊢ Invertible ((coeff 1) (X - X ^ 2))
      simp [coeff_X, coeff_X_pow]n:ℕ⊢ Invertible 1; exact invertibleOneAll goals completed! 🐙
    coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) =
      (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := byn:ℕ⊢ (coeff (n + 1)) (X - X ^ 2).substInv = ↑((2 * n).choose n) / (↑n + 1)
  sorryAll goals completed! 🐙

Solved by

• @kim-em with Aristotle (Harmonic) on May 1, 2026 (proof)

• @rkirov with Claude Opus 4.7 (1M context) on May 2, 2026 (proof)

• @sqrt-of-2 with GPT-5.5 on May 7, 2026 (proof)

• @antpavzhi with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 13, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026