Comment on Verified dynamic programming with Σ-types in LeanparentComments−hansvm1yThat can't possibly be the case. The thing concluded was that for every n the statement holds. To do that exhaustively for _every_ n requires infinite time. Either their conclusion is incorrect, or your description of the proof is incorrect.
Comments
That can't possibly be the case. The thing concluded was that for every n the statement holds. To do that exhaustively for _every_ n requires infinite time. Either their conclusion is incorrect, or your description of the proof is incorrect.