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.
