The Lean program in the article, adds `maxDollars_spec n` as a type on `helper`, with strong induction actually proves for all N possible that the implementation of the dynamic program is correct.

You can go further. Write the iterative form of a dynamic program (which uses array to store values, instead of hash, and uses a for loop instead of recursive memoized call) and prove it is computing the recursive maxDollars_spec.

Similar things were done with Z3 prover for other functions. Bit tricks, you want to go from one subset repr to the next. Subset {1, 3} is encoded as 101. Subset {1, 3, 7} as 1010001. You want to go to the next lexicographically greater subset of size 3. You can do that with efficient bit tricks, or you can write a recursive spec. You can use Z3 prover to prove for bitset of size N, that your algorithm that uses efficient tricks is equivalent to the recursive spec.

If Z3 prover actually had to go through all pairs (x,y) to prove that f(x)=y, you'd never get the proof in time.

Well, all I can say here is that my intuition suggested to me that proofs about the complexity of a set are generally not extensible to much-less-complex subsets.

But OK. If you want an objection stated in terms of Richardson's theorem, where are we invoking the sine function?

> Irrespective of where you're convinced it's 100% true that equality of two functions is undecidable in general.

So what? We're not trying to decide the equality of two functions in general. We're deciding the equality of two functions in specific.

> If Richardson's doesn't convince you there's also https://en.m.wikipedia.org/wiki/Rice%27s_theorem

>> Is P equivalent to a given program Q?

Again, why is this supposed to matter?

Here are two programs in C:

    int main(int argc, char* argv[]) {
      return 0;
    }

    int main(int argc, char* argv[]) {
      return 3 + 1 - 4;
    }

Rice's theorem says there is no algorithm which will take two programs as input and return yes if they're equivalent while returning no if they aren't. But no attempt has been made to supply such an algorithm.