Verified algorithms in Lean, implemented and proved by AIs

1 Open Issue Need Help Last updated: Jul 29, 2025

Open Issues Need Help

View All on GitHub
Algorithm Development Formal Verification

AI Summary: Implement a memoized version of the knapsack algorithm in Lean, along with a proof of equivalence to the existing recursive version. The solution should leverage existing Lean code and potentially strategies from a provided `Memoization.lean` file. Documentation of the implementation process is required.

Complexity: 4/5
good first issue

Verified algorithms in Lean, implemented and proved by AIs

Lean