Readme updates

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