Yes, of course there are. Now, imagine you're a language model, and given the prompt "I'm going to write code to explain what a finite summation is", try to predict the probability that what follows is "and I'm going to do it in Idris".
"Compiling" down the product to a fold brings you to the same issue. Though of course it's a lot easier to reason about math in functional programming than in imperative programming, you still lose some of the equational properties that later allow you to derive closed formulas.
