feat: add Catalan number substInv eval problem

FormalMathEval/Combinatorics/CatalanSubstInv.lean

@@ -0,0 +1,34 @@
+import Mathlib.RingTheory.PowerSeries.Substitution
+import Mathlib.Data.Nat.Choose.Central
+import EvalTools.Markers
+
+namespace FormalMathEval
+namespace Combinatorics
+
+open PowerSeries
+
+/-!
+The Catalan generating function via compositional inversion.
+
+The Catalan numbers `C_n = (2n choose n) / (n + 1)` arise as the coefficients of the
+compositional inverse of the power series `X - X²`. This is one of the most classical
+applications of Lagrange inversion in enumerative combinatorics: the generating function
+`C(x) = ∑ C_n x^{n+1}` satisfies `C(x) - C(x)² = x`, so `C` is the compositional inverse
+of the polynomial `P(x) = x - x²`.
+
+Equivalently, `C(x) = (1 - √(1 - 4x)) / 2`.
+
+This identity connects formal power series inversion (`substInv`) to the enumeration of
+Dyck paths, binary trees, triangulations of polygons, and many other combinatorial structures.
+-/
+
+@[eval_problem]
+theorem substInv_X_sub_X_sq_eq_catalan (n : ℕ) :
+    haveI : Invertible (coeff 1 ((X : ℚ⟦X⟧) - X ^ 2)) := by
+      simp [coeff_X, coeff_X_pow]; exact invertibleOne
+    coeff (n + 1) (substInv ((X : ℚ⟦X⟧) - X ^ 2)) =
+      (Nat.choose (2 * n) n : ℚ) / (↑n + 1) := by
+  sorry
+
+end Combinatorics
+end FormalMathEval

manifests/problems.toml

@@ -186,3 +186,14 @@ submitter = "Kim Morrison"
 notes = "A concrete stable-family homotopy-group computation."
 source = "Classical theorem in unstable homotopy theory."
 informal_solution = "Use suspension and the stable range to show the first stable stem is Z/2."
+
+[[problem]]
+id = "substInv_X_sub_X_sq_eq_catalan"
+title = "Catalan generating function via compositional inversion"
+test = false
+module = "FormalMathEval.Combinatorics.CatalanSubstInv"
+theorem = "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)."