Leetcode exercises in Lean4

Run all the exercises

lake exe leetcode

Run a single exercise

lake exe <name>

where name is given in the following table:

Exercise	Implementation	Test name	Bench name
twoSum	TwoSum.lean	twosum-test	twosum-bench
reverse	Reverse.lean	reverse-test

Credits

This code was written with @awalterschulze on his twitch channel. The recording of us tackling the initial problems can be found on youtube.