Hi, running through the benchmark I might have found some entries with mismatching specs / implementations: **sample_examples** - [problem_0.lean](https://github.com/trishullab/clever/blob/main/src/lean4/sample_examples/problem_0.lean) **human_eval** - [problem_1.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_1.lean) - [problem_6.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_6.lean) - [problem_9.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_9.lean) - [problem_13.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_13.lean) - [problem_18.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_18.lean) - [problem_19.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_19.lean) - [problem_20.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_20.lean) - [problem_25.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_25.lean) - [problem_31.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_31.lean) - [problem_32.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_32.lean) - [problem_36.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_36.lean) - [problem_73.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_73.lean) - [problem_78.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_78.lean) - [problem_82.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_82.lean) - [problem_101.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_101.lean) - [problem_108.lean](https://github.com/trishullab/clever/blob/main/src/lean4/human_eval/problem_108.lean) I will try to provide counterexamples or explanations to each in this thread, but that might not be immediate 😅