Initial Commit (untested)

1 files changed, 9 insertions, 0 deletions

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..633b106
--- /dev/null
+++ b/README.md
@@ -0,0 +1,9 @@
+# lean-astar
+
+A simple A* implementation in Lean4, made for Advent of Code 2023.
+
+It currently is not formally validated, but might get validated later.
+
+However, the termination of the pathfinding function has been shown, and it uses a formally validated binary heap for its open set, so the first steps towards formal validation have been done already.
+
+Beware that this code is not optimized, and high performance is explicitly not a goal of this repo.
\ No newline at end of file