diff --git a/ITP/main.bib b/ITP/main.bib
index 2fb4238..0a72c5c 100644
--- a/ITP/main.bib
+++ b/ITP/main.bib
@@ -726,4 +726,21 @@ @article{03overmars_finding_sets_points_empty_convex_6_gons
   timestamp    = {Thu, 12 Mar 2020 17:21:09 +0100},
   biburl       = {https://dblp.org/rec/journals/dcg/Overmars03.bib},
   bibsource    = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{90dobkin_searching_empty_convex_polygons,
+  author       = {David P. Dobkin and
+                  Herbert Edelsbrunner and
+                  Mark H. Overmars},
+  title        = {Searching for Empty Convex Polygons},
+  journal      = {Algorithmica},
+  volume       = {5},
+  number       = {4},
+  pages        = {561--571},
+  year         = {1990},
+  url          = {https://doi.org/10.1007/BF01840404},
+  doi          = {10.1007/BF01840404},
+  timestamp    = {Wed, 17 May 2017 14:25:12 +0200},
+  biburl       = {https://dblp.org/rec/journals/algorithmica/DobkinEO90.bib},
+  bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
\ No newline at end of file
diff --git a/ITP/slides.typ b/ITP/slides.typ
index 7c0f315..2b4a8b3 100644
--- a/ITP/slides.typ
+++ b/ITP/slides.typ
@@ -1,93 +1,111 @@
 #import "@preview/touying:0.5.2": *
 #import "@preview/cetz:0.2.2"
-#import themes.university: *
+#import themes.metropolis: *
 
-// Some slides adapted from https://www.cs.cmu.edu/~mheule/talks/6hole-TACAS.pdf
+// Many slides adapted from https://www.cs.cmu.edu/~mheule/talks/6hole-TACAS.pdf
 
-#show: university-theme.with(
-  config-info(
+#let config = (
+  aspect-ratio: "16-9",
+  // config-common(handout: true),
+  ..config-info(
     title: [Formal Verification of the Empty Hexagon Number],
     author: [
-      Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio,\
-      Cayden Codel, *Mario Carneiro*, Marijn J. H. Heule
+      Bernardo Subercaseaux¹, Wojciech Nawrocki¹, James Gallicchio¹,\
+      Cayden Codel¹, *Mario Carneiro*#h(0em)¹, Marijn J. H. Heule¹
     ],
     date: [
-      Interactive Theorem Proving | September 9th, 2024\
+      _Interactive Theorem Proving_ | September 9th, 2024\
       Tbilisi, Georgia
     ],
-    institution: [Carnegie Mellon University, USA]
+    institution: [¹ Carnegie Mellon University, USA]
+  ),
+  ..config-colors(
+    primary: rgb("#eb811b"),
+    primary-light: rgb("#d6c6b7"),
+    secondary: rgb("#23373b"),
+    neutral-lightest: rgb("#fafafa"),
+    neutral-dark: rgb("#23373b"),
+    neutral-darkest: rgb("#23373b"),
   )
 )
+#show: metropolis-theme.with(config)
+#set text(size: 23pt)
 
 #title-slide()
 
+// WN: I think this should be first slide, not the 9-pt example;
+// it is really confusing to look at a pointset
+// without knowing what kind of structure one is looking for.
+
 == Empty $k$-gons
 
-Fix a set $S$ of points on the plane.
-A *$k$-hole* is a convex $k$-gon with no point of $S$ in its interior.
+Fix a set $S$ of points on the plane, _no three collinear_.
+A *$bold(k)$-hole* is a convex $k$-gon with no point of $S$ in its interior.
 
-#components.side-by-side(
+// PERTURB THE POINTS
+#align(center, components.side-by-side(
   cetz.canvas(length: 33%, {
     import cetz.draw: *
-    set-style(circle: (fill: blue, stroke: none, radius: 0.05))
+    set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05))
     on-layer(1, {
       circle((angle: 0deg, radius: 1), name: "a")
       circle((angle: 72deg, radius: 1), name: "b")
       circle((angle: 144deg, radius: 1), name: "c")
       circle((angle: 216deg, radius: 1), name: "d")
       circle((angle: 290deg, radius: 1), name: "e")
-      circle((angle: 30deg, radius: 1.5), fill: black)
-      circle((angle: 240deg, radius: 1.5), fill: black)
+      circle((angle: 30deg, radius: 1.5))
+      circle((angle: 240deg, radius: 1.5))
     })
-    line("a", "b", "c", "d", "e", "a", fill: green)
+    line("a", "b", "c", "d", "e", "a", fill: config.colors.primary.transparentize(20%))
     content((0, -1.5), "5-hole ✔")
     content((0, -2.0), "convex 5-gon ✔")
   }),
   cetz.canvas(length: 33%, {
     import cetz.draw: *
-    set-style(circle: (fill: blue, stroke: none, radius: 0.05))
+    set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05))
     on-layer(1, {
       circle((angle: 0deg, radius: 1), name: "a")
       circle((angle: 120deg, radius: 1), name: "b")
       circle((angle: 180deg, radius: 0.2), name: "c")
       circle((angle: 240deg, radius: 1), name: "d")
-      circle((angle: 200deg, radius: 1.2), fill: black)
+      circle((angle: 200deg, radius: 1.2))
     })
-    line("a", "b", "c", "d", "a")
+    line("a", "b", "c", "d", "a", fill: config.colors.primary-light.transparentize(20%))
     content((0, -1.5), "4-hole ✘")
     content((0, -2.0), "convex 4-gon ✘")
   }),
   cetz.canvas(length: 33%, {
     import cetz.draw: *
-    set-style(circle: (fill: blue, stroke: none, radius: 0.05))
+    set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05))
     on-layer(1, {
       circle((angle: 0deg, radius: 1), name: "a")
       circle((angle: 120deg, radius: 1), name: "b")
       circle((angle: 240deg, radius: 1), name: "c")
-      circle((angle: 30deg, radius: 0.2), fill: black)
+      circle((angle: 30deg, radius: 0.2))
     })
-    line("a", "b", "c", "a")
+    line("a", "b", "c", "a", fill: config.colors.primary-light.transparentize(20%))
     content((0, -1.5), "3-hole ✘")
     content((0, -2.0), "convex 3-gon ✔")
   }),
-)
+))
+
+// TOOO: speaker note: our points are never collinear
 
-== Empty 4-gons
+== 5 points must contain a 4-hole
 
 #slide(repeat: 10, self => [
   #let (uncover,) = utils.methods(self)
 
   *Theorem* (Klein 1932). // WN: I don't think a citation exists for this
-  Every 5 points in the plane, no three collinear,
-  contain a 4-hole. #pause
+  Every 5 points in the plane contain a 4-hole. #pause
 
-  _Proof._ By cases on the size of the convex hull: 5, 4, or 3 points.
+  _Proof._ By cases on the size of the convex hull.
 
   #components.side-by-side(
-    uncover("3-", context align(center, cetz.canvas(length: 33%, {
+    uncover("3-", align(center, cetz.canvas(length: 33%, {
       import cetz.draw: *
 
-      set-style(circle: (fill: blue, stroke: none, radius: 0.05))
+      set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05))
       on-layer(1, {
         circle((angle: 0deg, radius: 1), name: "a")
         circle((angle: 72deg, radius: 1), name: "b")
@@ -97,13 +115,13 @@ A *$k$-hole* is a convex $k$-gon with no point of $S$ in its interior.
       })
       line("a", "b", "c", "d", "e", "a")
       if 4 <= self.subslide {
-        line("a", "b", "c", "d", "a", fill: green)
+        line("a", "b", "c", "d", "a", fill: config.colors.primary.transparentize(20%))
       }
     }))),
-    uncover("5-", context align(center, cetz.canvas(length: 33%, {
+    uncover("5-", align(center, cetz.canvas(length: 33%, {
       import cetz.draw: *
 
-      set-style(circle: (fill: blue, stroke: none, radius: 0.05))
+      set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05))
       on-layer(1, {
         circle((angle: 0deg, radius: 1), name: "a")
         circle((angle: 90deg, radius: 1), name: "b")
@@ -113,16 +131,16 @@ A *$k$-hole* is a convex $k$-gon with no point of $S$ in its interior.
       })
       line("a", "b", "c", "d", "a")
       if 7 <= self.subslide {
-        line("a", "d", "c", "x", "a", fill: green)
+        line("a", "d", "c", "x", "a", fill: config.colors.primary.transparentize(20%))
       }
       if 6 <= self.subslide {
-        line((angle: 0deg, radius: 1.5), (angle: 180deg, radius: 1.5), stroke: blue)
+        line((angle: 0deg, radius: 1.5), (angle: 180deg, radius: 1.5), stroke: config.colors.primary)
       }
     }))),
-    uncover("8-10", context align(center, cetz.canvas(length: 33%, {
+    uncover("8-10", align(center, cetz.canvas(length: 33%, {
       import cetz.draw: *
 
-      set-style(circle: (fill: blue, stroke: none, radius: 0.05))
+      set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 0.05))
       let xθ = 20deg
       let yθ = xθ + 180deg
       on-layer(1, {
@@ -133,103 +151,188 @@ A *$k$-hole* is a convex $k$-gon with no point of $S$ in its interior.
         circle((angle: yθ, radius: 0.3), name: "y")
       })
       line("a", "b", "c", "a")
-      if 10 <= self.subslide {
-        line("a", "x", "y", "c", "a", fill: green)
-      }
       if 9 <= self.subslide {
-        line((angle: xθ, radius: 1.5), (angle: yθ, radius: 1.5), stroke: blue)
+        line((angle: xθ, radius: 1.5), (angle: yθ, radius: 1.5), stroke: config.colors.primary)
+      }
+      if 10 <= self.subslide {
+        line("a", "x", "y", "c", "a", fill: config.colors.primary.transparentize(20%))
       }
     })))
   )
 ])
 
-== The Happy Ending Problem
+== 9 points with no 5-holes
+
+#slide(
+    // Hide header by making it background-coloured
+    // config: config-colors(secondary: config.colors.neutral-lightest),
+    align: center+horizon,
+    repeat: 4,
+    self => cetz.canvas({
+  import cetz.draw: *
+  set-style(circle: (fill: config.colors.neutral-darkest, stroke: none, radius: 1.2))
+  scale(.1)
+  on-layer(1, {
+    let pts = (
+      (1,  0,  "a"),
+      (100, 0, "b"),
+      (51, 88, "c"),
+
+      (30, 40, "d"),
+      (49, 10, "e"),
+      (70, 40, "f"),
+
+      (45, 26, "g"),
+      (55, 26, "h"),
+      (50, 35, "i"),
+    )
+
+    for (x, y, n) in pts {
+      circle((x, y), name: n)
+    }
+  })
+  if self.subslide > 1 {
+    line("a", "b", "c", "a")
+    line("d", "e", "f", "d")
+    line("g", "h", "i", "g")
+  }
+  if self.subslide == 3 {
+    line("a", "e", "h", "i", "d", "a", fill: config.colors.primary-light.transparentize(20%))
+    content((25, -10), [5-hole ✘])
+    content((25, -20), [convex 5-gon ✔])
+  }
+  if self.subslide == 4 {
+    line("d", "e", "b", "h", "g", "d", fill: config.colors.primary-light.transparentize(20%))
+    content((75, -10), [convex 5-gon ✘])
+  }
+}))
+
+/////////// DONE ABOVE
+/////////// WORK AREA BELOW
 
-*Theorem* @35erdos_combinatorial_problem_geometry.
-For a fixed $k$, every _sufficiently large_ set of points,
-no three collinear, contains a convex $k$-gon.
+== The Happy Ending Problem
 
-What about _$k$-holes_?
+// TODO(WN): make #pause-gray gray out the things that came before
 
-*Theorem* @hortonSetsNoEmpty1983.
-For any $k ≥ 7$, there exist arbitrarily large sets of points,
-no three collinear, containing no $k$-holes.
+$g(k) =$ least $n$ s.t. any set of $n$ points must contain a *convex $bold(k)$-gon*
 
-The $k$-th *hole number* $h(k)$ is the least number
-such that any set of $h(k)$ points,
-no three collinear,
-necessarily contains a $k$-hole.
+$h(k) =$ least $n$ s.t. any set of $n$ points must contain a *$bold(k)$-hole* #pause
 
-Horton ⇒ $h(7) = h(8) = … = ∞$
+We just showed $h(4) ≤ 5$ and $9 < h(5)$. #pause
 
-== The Complete Story
+*Theorem* @35erdos_combinatorial_problem_geometry.
+For a fixed $k$, every _sufficiently large_ set of points contains a convex $k$-gon.
+So $g(k)$ is finite. #pause
 
-- $h(3) ≤ 3$ (trivial) ✔
-- $h(4) ≤ 5$ (Klein 1932) ✔
-- $h(5) ≤ 10$ @Harborth1978 ✔
-- *$bold(h(6) ≤ 30)$ @24heule_happy_ending_empty_hexagon_every_set_30_points* ✔
-- $29 < h(6)$ @03overmars_finding_sets_points_empty_convex_6_gons ✔
+*Theorem* @hortonSetsNoEmpty1983.
+For any $k ≥ 7$, there exist arbitrarily large sets of points containing no $k$-holes.
+So $h(7) = h(8) = … = ∞$.
+
+== The complete story
+
+#table(
+  columns: (auto, auto),
+  inset: 5pt,
+  stroke: none,
+  [$h(3) = 3$ (trivial)],
+  [$g(3) = 3$ (trivial)],
+  [$h(4) = 5$ (Klein 1932)],
+  [$g(4) = 5$ (Klein 1932)],
+  [$h(5) = 10$ @Harborth1978],
+  // TODO: see https://en.wikipedia.org/wiki/Happy_ending_problem#cite_note-4
+  [$g(5) = 9$ (CITATION NEEDED)],
+  [*$bold(h(6) = 30)$ @03overmars_finding_sets_points_empty_convex_6_gons @24heule_happy_ending_empty_hexagon_every_set_30_points*],
+  [$g(6) = 17$ @szekeres_peters_2006],
+) #pause
+
+We formally verified all the above in $L∃∀N$. #pause
+
+Upper bounds by combinatorial reduction to SAT. #pause
+
+#[
+#set par(first-line-indent: 1em, hanging-indent: 1em)
+▸ We focused on $h(6)$.\ #pause
+▸ $g(6)$ previously verified in Isabelle/HOL @10maric_formal_verification_modern_sat_solver_shallow_embedding_isabelle_hol.\ #pause
+▸ Efficient SAT encoding of Heule & Scheucher speeds up $g(6)$ verification. #pause
+]
 
-We formally verified all the above results using $L∃∀N$.
-// TODO(WN): Should we stress more that
-// verifying Heule/Scheucher was the hard part; and
-// the other upper bounds follow from the encoding with not much effort; and
-// then we also verified the pointset checker to establish lower bounds.
+Lower bounds by checking explicit sets of points.
+  // TODO: Is this the first verification of the hole-tester algo?
 
-Upper bounds via reduction to SAT.
+== SAT-solving mathematics
 
-Lower bounds by checking explicit sets of points.
+*Reduction.* Show that a mathematical theorem is true
+if a propositional formula φ is unsatisfiable.
 
-== SAT-Solving Mathematics
+*Solving.* Show that φ is indeed unsatisfiable using a SAT solver. #pause
 
-- *Reduction.* Show that the mathematical theorem of interest is true
-  if a concrete propositional formula φ is unsatisfiable.
-- *Solving.* Show that φ is indeed unsatisfiable using a SAT solver.
+▸ Solving is reliable, reproducible, and trustworthy:
+formal proof systems (DRAT) and verified proof checkers (`cake_lpr`). #pause
 
-*Solving* is reliable, reproducible, and trustworthy:
-formal proof systems (DRAT) and verified proof checkers (`cake_lpr`).
+▸ But reduction is problem-specific, and involves complex transformations:
+_focus of our work_.
 
-*Reduction* is problem-specific, and involves complex transformations:
-focus of our work.
+== Reduction from geometry to SAT
 
-== Reduction from Geometry to SAT
+// TODO: make text shorter
 
+// TODO(WN): pauses for the list
 #set text(size: 23pt)
-1. Any set of points, no three collinear,
-   can be transformed into a _canonical form_
+1. Points can be put in _canonical form_
    without removing $k$-holes.
    ```lean
-  theorem symmetry_breaking {l : List Point} :
-    3 ≤ l.length → Point.ListInGenPos l →
-    ∃ w : CanonicalPoints, l ≼σ w.points
-  ```
-2. $n$ points in canonical form with no $k$-holes
+   theorem symmetry_breaking {l : List Point} :
+     3 ≤ l.length → PointsInGenPos l →
+     ∃ w : CanonicalPoints, l ≼σ w.points
+   ```
+2. $n$ points in canonical form with no $6$-holes
    induce a propositional assignment that satisfies $φ_n$.
-  ```lean
-  theorem satisfies_hexagonEncoding (w : CanonicalPoints) :
-      ¬σHasEmptyKGon 6 w.toFinset →
-      w.toPropAssn ⊨ hexagonEncoding w.rlen
-  ```
-3. $φ_30$ is unsatisfiable.
-  ```lean
-  axiom unsat_6hole_cnf : (Geo.hexagonCNF (rlen := 30-1)).isUnsat
-  ```
+   ```lean
+   theorem satisfies_hexagonEncoding {w : CanonicalPoints} :
+     ¬σHasEmptyKGon 6 w → w.toPropAssn ⊨ Geo.hexagonCNF w.len
+   ```
+3. But $φ_30$ is unsatisfiable.
+   ```lean
+   axiom unsat_6hole_cnf : (Geo.hexagonCNF 30).isUnsat
+   ```
+
+== 1. Symmetry breaking
+
+// TODO: add teh content
+
+The sequence of six steps from Fig. 5
+(transformation into `CanonicalPoints`);
+make it an animation.
+
 
-// TODO: Marijn describes the entire encoding. Should we,
-// or should we focus more on the verification;
-// for example our adjusted symmetry breaking?
+== 2. SAT encoding
 
-== Lower Bounds
+// TODO: add teh content
 
-Checker checker
-// TODO: Say something about pointset checker verification
+- Introduce $σ$ variables
+- Show scary picture of full encoding (?)
+- Talk about cap-cup clauses; copy slide 14/21 from Marijn
 
-== Final Theorem
+== 3. Running the SAT solver
+
+// TODO: add teh content
+
+How many clauses, how long it took, cluster compute amount (from 'Running the CNF')
+
+== Lower bounds
+
+// TODO(MARIO): put someting in this slide, without describing the algorithm
+// TODO(Bernardo): draw pictures of the algorithm
+
+$cal(O)("sth")$ time, $cal(O)("sth")$ space algorithm @90dobkin_searching_empty_convex_polygons
+
+We verified it, and used it to check the lower bounds.
+
+== Final theorem
 
-#rect(height: 100%)[
 #set text(size: 24pt)
 ```lean
-axiom unsat_6hole_cnf : (Geo.hexagonCNF (rlen := 30-1)).isUnsat
+axiom unsat_6hole_cnf : (Geo.hexagonCNF 30).isUnsat
 
 theorem holeNumber_6 : holeNumber 6 = 30 :=
   le_antisymm (hole_6_theorem' unsat_6hole_cnf) (hole_lower_bound [
@@ -241,8 +344,7 @@ theorem holeNumber_6 : holeNumber 6 = 30 :=
     (552, 502), (754, 697), (777, 194), (1259, 320)
   ])
 ```
-]
 
 == Bibliography
 
-#bibliography("main.bib", style: "chicago-author-date")
\ No newline at end of file
+#bibliography("main.bib", style: "chicago-author-date", title: none)
\ No newline at end of file
diff --git a/flake.lock b/flake.lock
index fd85f3d..9b66e4e 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1705309234,
-        "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=",
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
         "type": "github"
       },
       "original": {
@@ -20,11 +20,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1705883077,
-        "narHash": "sha256-ByzHHX3KxpU1+V0erFy8jpujTufimh6KaS/Iv3AciHk=",
+        "lastModified": 1725534445,
+        "narHash": "sha256-Yd0FK9SkWy+ZPuNqUgmVPXokxDgMJoGuNpMEtkfcf84=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "5f5210aa20e343b7e35f40c033000db0ef80d7b9",
+        "rev": "9bb1e7571aadf31ddb4af77fc64b2d59580f9a39",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index cd8760d..d106b60 100644
--- a/flake.nix
+++ b/flake.nix
@@ -16,6 +16,7 @@
           fontconfig
           gcc
           python3
+          typst
         ];
 
         FONTCONFIG_FILE = pkgs.makeFontsConf { fontDirectories = [