Verified dynamic programming with Σ-types in Lean
1. Introduction If you’ve taken an algorithms class, you have likely seen dynamic programming, specifically a technique called memoization. Memoization works to optimize recursive algorithms by caching the solutions to subproblems in a table, and when a subproblem is encountered, it queries the table instead of recomputing the solution. This gives us an exponential performance boost. This blog post will show how to solve a dynamic programming problem using memoization in Lean, and verify its c