diff --git a/lean4-mode/lean4-hole.el b/lean4-mode/lean4-hole.el
index 6a31ce88cf..18457e5103 100644
--- a/lean4-mode/lean4-hole.el
+++ b/lean4-mode/lean4-hole.el
@@ -16,7 +16,7 @@
 ;; helm or company's interface would be a good addition.
 ;;
 ;;; Code:
-(require 'lean4-server)
+;(require 'lean4-server)
 
 (defun lean4-hole-handler-completing-read (alternatives)
   "Pick a hole replacement from ALTERNATIVES with `completing-read'."
diff --git a/lean4-mode/lean4-type.el b/lean4-mode/lean4-type.el
index 7215a3a679..6c57a23223 100644
--- a/lean4-mode/lean4-type.el
+++ b/lean4-mode/lean4-type.el
@@ -10,7 +10,7 @@
 (require 'dash-functional)
 (require 's)
 (require 'lean4-util)
-(require 'lean4-server)
+;(require 'lean4-server)
 (require 'lean4-debug)
 (require 'flymake)