From fb5824518da9a6102aebf80d3312c2688fbaff79 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 7 Nov 2025 22:20:41 +0000
Subject: [PATCH 1/3] Initial plan


From 892fe7fa0835f4315d1f44d83448ff767f650ae7 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 7 Nov 2025 22:28:56 +0000
Subject: [PATCH 2/3] Add binomial support to LEAN formula generation using
 Nat.choose

Co-authored-by: ckrause <840744+ckrause@users.noreply.github.com>
---
 src/form/lean.cpp      | 23 +++++++++++++++++++++++
 tests/formula/lean.txt |  2 ++
 2 files changed, 25 insertions(+)

diff --git a/src/form/lean.cpp b/src/form/lean.cpp
index 442a1fde..eb84220a 100644
--- a/src/form/lean.cpp
+++ b/src/form/lean.cpp
@@ -97,6 +97,29 @@ bool LeanFormula::convertToLean(Expression& expr, int64_t offset,
         expr.name = "Int.gcd";
         break;
       }
+      // Convert binomial function to LEAN Nat.choose
+      if (expr.name == "binomial") {
+        // binomial requires exactly 2 arguments
+        if (expr.children.size() != 2) {
+          return false;
+        }
+        auto n = expr.children[0];
+        auto k = expr.children[1];
+        // Check if arguments can be negative
+        if (ExpressionUtil::canBeNegative(n, offset) ||
+            ExpressionUtil::canBeNegative(k, offset)) {
+          return false;
+        }
+        // Convert to Nat.choose(Int.toNat(n), Int.toNat(k))
+        Expression toNatN(Expression::Type::FUNCTION, "Int.toNat", {n});
+        Expression toNatK(Expression::Type::FUNCTION, "Int.toNat", {k});
+        Expression choose(Expression::Type::FUNCTION, "Nat.choose",
+                          {toNatN, toNatK});
+        Expression result(Expression::Type::FUNCTION, "Int.ofNat", {choose});
+        expr = result;
+        imports.insert("Mathlib.Data.Nat.Choose.Basic");
+        break;
+      }
       // Convert floor and truncate functions to LEAN equivalents
       if (expr.name == "floor" || expr.name == "truncate") {
         // These functions should have a single FRACTION argument
diff --git a/tests/formula/lean.txt b/tests/formula/lean.txt
index eac09fb8..20fca306 100644
--- a/tests/formula/lean.txt
+++ b/tests/formula/lean.txt
@@ -72,3 +72,5 @@ A080457: def a (n : Int) : Int := (Int.lor (3*n-6) 3)+4
 A106249: def a (n : Int) : Int := Int.tdiv ((Int.lor (n+1) 2)-1) 2
 A109008: def a (n : Int) : Int := Int.gcd n 4
 A129760: def a (n : Int) : Int := Int.land n (n-1)
+A000096: def a (n : Int) : Int := (Int.ofNat (Nat.choose (Int.toNat (n+2)) (Int.toNat 2)))-1
+A000108: def a (n : Int) : Int := Int.fdiv (Int.ofNat (Nat.choose (Int.toNat (2*n)) (Int.toNat n))) (n+1)

From 3a571e0113029280cece8429af0faa8c4c73ff5d Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 7 Nov 2025 22:30:17 +0000
Subject: [PATCH 3/3] Update CHANGELOG for binomial support in LEAN

Co-authored-by: ckrause <840744+ckrause@users.noreply.github.com>
---
 CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d4c47cfc..338a7025 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,7 @@
 
 ### Enhancements
 
+* Support `bin` (binomial coefficient) in LEAN formula generation
 * Support `fac` in LEAN formula generation
 * Improve LEAN formula generation for `pow`