Support binomial coefficients in LEAN formula generation

[Copilot]

The LEAN formula exporter rejected programs containing binomial coefficient operations, while the base formula generator already converted bin operations to binomial functions.

Changes

• src/form/lean.cpp: Convert binomial(n, k) to Int.ofNat(Nat.choose(Int.toNat(n), Int.toNat(k))) when both arguments are provably non-negative. Reject conversion otherwise. Add import for Mathlib.Data.Nat.Choose.Basic.

• tests/formula/lean.txt: Add test cases for A000096 (triangular numbers) and A000108 (Catalan numbers).

Example

LODA program for Catalan numbers (A000108):

mov $1,$0
mul $0,2
bin $0,$1
mov $2,$1
add $2,1
div $0,$2

Now exports to LEAN as:

def a (n : Int) : Int := Int.fdiv (Int.ofNat (Nat.choose (Int.toNat (2*n)) (Int.toNat n))) (n+1)

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Support binomial in LEAN formula generation</issue_title> <issue_description>The generic FormulaGenerator converts bin operations to binomial functions. Extend the LEAN formula generator to support this as well. We'll need to find out if LEAN natively supports binomila coeeficients, or if there are modules for it, or if we need to add ad-hoc (recursive) functions for it.</issue_description>

Comments on the Issue (you are @copilot in this section)

@ckrause For non-negative arguments (`Nat`), we could use [Nat.choose](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Choose/Basic.html#Nat.choose). But then we would need to integrate a range check to find out if it is non-negative.

• Fixes loda-lang/loda-cpp#550

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.