diff --git a/emacs/.config/emacs/Emacs.org b/emacs/.config/emacs/Emacs.org
index 9fea1d1..ed5250d 100644
--- a/emacs/.config/emacs/Emacs.org
+++ b/emacs/.config/emacs/Emacs.org
@@ -111,6 +111,28 @@
     (fontaine-set-preset 'regular))
 #+end_src
 
+** Ligatures
+#+begin_src emacs-lisp
+  (use-package ligature
+    :config
+    (ligature-set-ligatures 't '("www"))
+    (ligature-set-ligatures 'eww-mode '("ff" "fi" "ffi"))
+    (ligature-set-ligatures 'prog-mode '("|||>" "<|||" "<==>" "<!--" "####" "~~>" "***" "||=" "||>"
+                                         ":::" "::=" "=:=" "===" "==>" "=!=" "=>>" "=<<" "=/=" "!=="
+                                         "!!." ">=>" ">>=" ">>>" ">>-" ">->" "->>" "-->" "---" "-<<"
+                                         "<~~" "<~>" "<*>" "<||" "<|>" "<$>" "<==" "<=>" "<=<" "<->"
+                                         "<--" "<-<" "<<=" "<<-" "<<<" "<+>" "</>" "###" "#_(" "..<"
+                                         "..." "+++" "/==" "///" "_|_" "www" "&&" "^=" "~~" "~@" "~="
+                                         "~>" "~-" "**" "*>" "*/" "||" "|}" "|]" "|=" "|>" "|-" "{|"
+                                         "[|" "]#" "::" ":=" ":>" ":<" "$>" "==" "=>" "!=" "!!" ">:"
+                                         ">=" ">>" ">-" "-~" "-|" "->" "--" "-<" "<~" "<*" "<|" "<:"
+                                         "<$" "<=" "<>" "<-" "<<" "<+" "</" "#{" "#[" "#:" "#=" "#!"
+                                         "##" "#(" "#?" "#_" "%%" ".=" ".-" ".." ".?" "+>" "++" "?:"
+                                         "?=" "?." "??" ";;" "/*" "/=" "/>" "//" "__" "~~" "(*" "*)"
+                                         "\\\\" "://"))
+    (global-ligature-mode t))
+#+end_src
+
 ** Which key
 #+begin_src emacs-lisp
   (use-package which-key
@@ -122,12 +144,26 @@
 #+end_src
 
 ** Theme
+*** Catppuccin
 #+begin_src emacs-lisp
   (use-package catppuccin-theme
     :config
     (load-theme 'catppuccin :no-confirm))
 #+end_src
-
+*** Modus Themes
+#+begin_src emacs-lisp
+  ;; (use-package emacs
+  ;;   :config
+  ;;   (require-theme 'modus-themes)
+  ;;   (setq modus-themes-italic-constructs t
+  ;; 	modus-themes-bold-constructs t
+  ;; 	modus-themes-links '(no-underline background faint)
+  ;; 	modus-themes-prompts '(bold intense)
+  ;; 	modus-themes-mode-line '(borderless accented moody)
+  ;; 	modus-themes-org-blocks 'gray-background
+  ;; 	modus-themes-region '(bg-only no-extend))
+  ;;   (modus-themes-load-operandi))
+#+end_src
 * Completion
 
 ** Vertico
@@ -287,11 +323,18 @@
   )
 #+end_src
 
+* Lsp
+I'm not a fan of =lsp-mode=, but =lean4-mode= requires it as a dependency, so I might as well actually install it.
+#+begin_src emacs-lisp
+  (use-package lsp-ui)
+  (use-package lsp-mode)
+#+end_src
+
 * Languages
 ** Agda
 #+begin_src emacs-lisp
-;  (load-file (let ((coding-system-for-read 'utf-8))
-;                  (shell-command-to-string "agda-mode locate")))
+ (load-file (let ((coding-system-for-read 'utf-8))
+                 (shell-command-to-string "agda-mode locate")))
 #+end_src
 
 ** Idris
@@ -305,7 +348,18 @@
 #+begin_src emacs-lisp
   (use-package haskell-mode)
 #+end_src
-
+** PG
+#+begin_src emacs-lisp
+  (use-package proof-general)
+#+end_src
+** Lean
+#+begin_src emacs-lisp
+  (use-package lean4-mode
+    :commands lean4-mode
+    :straight (lean4-mode :type git :host github
+                          :repo "leanprover-community/lean4-mode"
+                          :files ("*.el" "data")))
+#+end_src
 * Latex
 
 ** Auctex