1 files changed, 23 insertions, 0 deletions
diff --git a/content/zettel/4f.md b/content/zettel/4f.md
new file mode 100644
index 0000000..eae8eb9
--- /dev/null
+++ b/content/zettel/4f.md
@@ -0,0 +1,23 @@
++++
+title = "Informal Mathematics"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["4e"]
+forwardlinks = []
+zettelid = "4f"
++++
+
+Often when I write the mathematics seem to be informal. For example, the
+following is meant to describe a **well-founded** relation:
+
+> some metric stored in the $\sim$ relation is decreasing
+
+Then, in many definitions I also do not seem to define things precisely.
+I think this is mostly because there is so much content in the Coq proof
+that cannot all be translated into words, and needs to be reduced
+instead.
+
+Another example is when describing hashed expressions, I think I can be
+a bit more precise about what these are semantically, instead of
+syntactically in the formalisation.