Fix LEAN evaluation error for formulas with non-self-recursive mutual recursion (#623)

Author: Copilot

CHANGELOG.md

@@ -9,6 +9,7 @@
 ### Bugfixes
 
 * Fix PARI evaluation error for formulas with constant identity functions (e.g., A026765)
+* Fix LEAN evaluation error for formulas with mutually recursive functions that are not self-recursive (e.g., A001636)
 
 ## v25.11.29
 

src/form/formula_util.cpp

@@ -111,6 +111,59 @@ bool FormulaUtil::isRecursive(const Formula& formula,
   return false;
 }
 
+// Helper function to check if a function depends on another
+static bool dependsOn(const std::multimap<std::string, std::string>& deps,
+                      const std::string& from, const std::string& to) {
+  auto range = deps.equal_range(from);
+  for (auto it = range.first; it != range.second; ++it) {
+    if (it->second == to) {
+      return true;
+    }
+  }
+  return false;
+}
+
+bool FormulaUtil::hasMutualRecursion(const Formula& formula,
+                                     Expression::Type type) {
+  // Get transitive dependencies between functions
+  auto deps = getDependencies(formula, type, true, false);
+
+  // Build a set of all function names
+  std::set<std::string> funcNames;
+  for (const auto& e : formula.entries) {
+    if (e.first.type == type && !e.first.name.empty()) {
+      funcNames.insert(e.first.name);
+    }
+  }
+
+  // Check for mutual recursion: A depends on B and B depends on A (where A !=
+  // B), and neither A nor B is self-recursive.
+  // If at least one function in the cycle is self-recursive, the LEAN code
+  // generator will use Nat domain with pattern offsets, which can prove
+  // termination.
+  for (auto itA = funcNames.begin(); itA != funcNames.end(); ++itA) {
+    for (auto itB = std::next(itA); itB != funcNames.end(); ++itB) {
+      const auto& funcA = *itA;
+      const auto& funcB = *itB;
+
+      // Check for mutual dependency (A->B and B->A)
+      if (dependsOn(deps, funcA, funcB) && dependsOn(deps, funcB, funcA)) {
+        // Check if either A or B is self-recursive
+        // Use non-transitive check for self-recursion
+        bool aIsSelfRecursive = isRecursive(formula, funcA, type);
+        bool bIsSelfRecursive = isRecursive(formula, funcB, type);
+
+        // If neither is self-recursive, LEAN can't prove termination
+        // because the domain will be Int instead of Nat
+        if (!aIsSelfRecursive && !bIsSelfRecursive) {
+          return true;
+        }
+      }
+    }
+  }
+  return false;
+}
+
 Number FormulaUtil::getMinimumBaseCase(const Formula& formula,
                                        const std::string& funcName) {
   Number minBaseCase = Number::INF;

src/form/formula_util.hpp

@@ -17,6 +17,12 @@ class FormulaUtil {
   static bool isRecursive(const Formula& formula, const std::string& funcName,
                           Expression::Type type = Expression::Type::FUNCTION);
 
+  // Check if the formula contains mutually recursive functions (cycles of
+  // length > 1 in the dependency graph, e.g., A calls B, B calls A)
+  static bool hasMutualRecursion(
+      const Formula& formula,
+      Expression::Type type = Expression::Type::FUNCTION);
+
   static Number getMinimumBaseCase(const Formula& formula,
                                    const std::string& funcName);
 

src/form/lean.cpp

@@ -172,6 +172,13 @@ bool LeanFormula::convert(const Formula& formula, int64_t offset,
   if (as_vector) {
     return false;
   }
+
+  // Check for mutual recursion - LEAN can't prove termination automatically
+  // for mutually recursive functions without explicit termination proofs
+  if (FormulaUtil::hasMutualRecursion(formula)) {
+    return false;
+  }
+
   lean_formula = {};
   lean_formula.domain = "Int";
   lean_formula.funcNames =