Each solutions involve:
- formalizing the statement
- writing the solution and
- proving its correctness.
Would you accept PRs that accept a subset of the above? More people could easily join the collaboration if 1) is done for every problem. Some people might be very good at providing smart solutions just 2), but get stuck at 3).
For example, for HumanEval0 we can have just 1) like
def has_close_elements_iff (solution : Array Float → Float → Bool) : Prop :=
(numbers : Array Float) → (threshold : Float) →
solution numbers threshold ↔ ∃ (i j : Fin numbers.size), i < j ∧ (numbers[i] - numbers[j]).abs < thresholdThen a solution could look like this:
def has_close_elements_sort (numbers : Array Float) (threshold : Float) : Bool :=
-- fast solution that sorts the array first
sorry
theorem has_close_elements_sort_correct : has_close_elements_iff has_close_elements_sort := by
-- proof that the solution is correct
sorryOne advantage of this approach, is that we can have multiple solutions to the same problem, with different algorithms and tradeoffs.
Each solutions involve:
Would you accept PRs that accept a subset of the above? More people could easily join the collaboration if 1) is done for every problem. Some people might be very good at providing smart solutions just 2), but get stuck at 3).
For example, for HumanEval0 we can have just 1) like
Then a solution could look like this:
One advantage of this approach, is that we can have multiple solutions to the same problem, with different algorithms and tradeoffs.