[SkiFire13]

> the "proof" just computes the entire memo table for any n

No, this is what would happen _if you ran the proof_, but proofs are not meant to be ran in the first place! The usual goal is proving their correctness, and for that it's enough for them to _typecheck_.

[almostgotcaught]

it's explicitly stated in the article:

> For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof

if you thought harder about it you'd realize what you're suggesting is impossible

[ImprobableTruth]

This is the fault of sloppy language. In Lean, _proofs_ (equivalent to functions) and _proof objects/certificates_ (values) need to be distinguished. You can't compute proofs, only proof objects. In the above quote, replace "proof" with "certificate" and you'll see that it's a perfectly valid (if trivial - it essentially just applies a lemma) proof.

[almostgotcaught]

a distinction without a difference wrt what i'm pointing out: this proof uses exactly zero mathematics just effectively checks all the values of maxDollars_spec.

[SkiFire13]

> it's explicitly stated in the article: > > > For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof

That's what the intermediate function is doing, but _it doesn't need to be executed_ for the final proof to be valid.

> if you thought harder about it you'd realize what you're suggesting is impossible

No, it is perfectly possible. This is not a program running all cases and `assert`ing that they have the expected result, this is a proof encoded as a program that when executed will surely produce a proof that for the given n the theorem holds. But it surely produces a proof when executes you don't need to execute it to know that a proof exists and thus the theorem holds!

This is exactly what mathematicians do when they prove theorems. Do you think they go on and check for every number n that some theorem holds? That's impossible to do for every possible n, and this is exactly what you're claiming you can do in every other language.

And just to be extra clear, a signature like this:

> theorem maxDollars_spec_correct : ∀ n, maxDollars n = maxDollars_spec n

Does not mean that for every n the function returns a boolean indicating whether `maxDollars n` is equal to `maxDollars_spec n` or not. Instead, it _surely_ returns a proof that they are equal. And with _surely_ I mean it cannot return errors or exceptions or whatever. It is guaranteed that the function will terminate with a proof for that proposition, which I want to reiterate again, it's the same as knowing that the proposition is true.