From 7e04dcc8dbabdab61caf2758a69978fcf9ae3969 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 9 Jun 2025 13:59:07 +0200 Subject: [PATCH] readme updates --- README.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 0682679..3a418ae 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ # Verified hand-written Lean solutions to HumanEval [HumanEval] is a collection of small programming tasks originally intended as a benchmark for LLMs. -In this repo, we collect hand-written *formally verified* [Lean 4] solutions to these problems. +In this repo, we collect hand-written _formally verified_ [Lean 4] solutions to these problems. The idea is to build a small set of simple examples for verified software development using Lean. It is inspired by [human-eval-verus], which does a similar thing for the Verus Rust verification @@ -24,10 +24,18 @@ as the resulting code can still be considered idiomatic. We use the [Lean 4 standard library style guide and naming convention](https://github.com/leanprover/lean4/tree/master/doc/std), but we won't be very strict about enforcing it. +### Missing lemmas + One of the goals of the goals of this project is to assess the out-of-the-box experience of Lean 4 as a software verification tool, so this project will not take on dependencies such as Batteries. +Solutions to most tasks will encounter lemmas missing from Lean core. Some of the missing +lemmas might be available in a place like Batteries and mathlib. The procedure in this case is +to put the missing lemmas in the file where they are needed, with a note if they are available +somewhere else. In this way, the files in this repository clearly document what was missing +from Lean core. + [HumanEval]: https://github.com/openai/human-eval [Lean 4]: https://lean-lang.org/ [human-eval-verus]: https://github.com/secure-foundations/human-eval-verus