A few weeks ago I started the human-eval-lean project, an effort to collect hand-written solutions to the famous HumanEval (AI) programming benchmark, written in the programming language Lean. The twist is that Lean is not just a programming language, but also a proof assistant, and all solutions in human-eval-lean come with machine-checked formal proofs that the code is correct.
