aboutsummaryrefslogtreecommitdiff
path: root/README.md
diff options
context:
space:
mode:
Diffstat (limited to 'README.md')
-rw-r--r--README.md9
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