diff --git a/README.md b/README.md
index 858af6d..eccc869 100644
--- a/README.md
+++ b/README.md
@@ -11,7 +11,7 @@ For more information about Alectryon make sure to take a look at their repositor
 
 # Installation
 
-You can either build LeanInk and install it yourself or use the build script to install a LeanInk release version:
+You can either build LeanInk and install it yourself as shown below, or you can use the build script to install a LeanInk release version:
 
 ```bash
 sh -c "$(curl https://raw.githubusercontent.com/leanprover/LeanInk/main/init.sh -sSf)"
@@ -28,6 +28,11 @@ cd LeanInk
 lake build
 ```
 
+To install this built version to your `$HOME/.elan/bin` folder run:
+```bash
+lake script run install
+```
+
 # Usage
 
 Analyzing a simple lean program `Input.lean` is very straightforward. To do so you simply use the `analyze` command (shorthand `a`) and provide LeanInk the input file.
diff --git a/init.sh b/init.sh
index 39c73fe..c39da19 100644
--- a/init.sh
+++ b/init.sh
@@ -4,6 +4,4 @@ cd leanInk
 git fetch --tags -q
 latestTag=$(git describe --tags `git rev-list --tags --max-count=1`)
 git checkout $latestTag -q
-sh install.sh
-cd ..
-rm -rf ./leanInk
\ No newline at end of file
+lake script run install && cd .. && rm -rf ./leanInk
\ No newline at end of file
diff --git a/install.sh b/install.sh
deleted file mode 100644
index 4ea6b32..0000000
--- a/install.sh
+++ /dev/null
@@ -1,34 +0,0 @@
-#!/bin/bash
-
-error () {
-    echo $1
-}
-
-echo "Compiling LeanInk..."
-# First we have to build leanInk.
-lake build > /dev/null || error "Failed to build leanInk. Make sure your lean install is correct!"
-
-# As we can assume that lean is already installed as expected we can assume
-# that the .elan folder already exists and is correctly linked.
-ELAN_BIN="$HOME/.elan/bin/"
-
-echo "Installing LeanInk..."
-if [[ -f "$ELAN_BIN/leanInk" ]]; then
-    OLD_LEAN_INK=$(eval "$ELAN_BIN/leanInk -v")
-    NEW_LEAN_INK=$(eval "./build/bin/leanInk -v")
-    echo "LeanInk ($OLD_LEAN_INK) already installed. Do you want to overwrite it with LeanInk ($NEW_LEAN_INK) [Y|n]?"
-    read < /dev/stdin
-    SHOULD_OVERWRITE="$(tr '[:upper:]' '[:lower:]' <<< "${REPLY}")"
-    if [[ "${SHOULD_OVERWRITE}" == "y" ]]; then 
-        cp -f ./build/bin/leanInk ~/.elan/bin/ || error "Failed copying LeanInk to .elan/bin!"
-        echo "New LeanInk version successfully installed!"
-    else
-        echo "New LeanInk version not installed!"
-    fi
-else        
-    if cp ./build/bin/leanInk "$ELAN_BIN"; then
-        echo "LeanInk version successfully installed!"
-    else
-        echo "Failed copying LeanInk to .elan/bin!"
-    fi
-fi
diff --git a/lakefile.lean b/lakefile.lean
index cae14af..83d5f8b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,12 +13,16 @@ lean_exe leanInk {
   supportInterpreter := true
 }
 
-/-! Run the leanInk that is built locally to analyze the given test file.
-If there is a lakefile.lean present then pass the additional `--lake` option -/
-def runLeanInk (test : FilePath) : IO UInt32 := do
+def getLeanInkExePath : IO (FilePath × FilePath) := do
   let leanInk : FilePath := "build" / "bin" / "leanInk"
   let leanInkExe := leanInk.withExtension FilePath.exeExtension
   let realPath ← IO.FS.realPath leanInkExe
+  return (leanInkExe, realPath)
+
+/-! Run the leanInk that is built locally to analyze the given test file.
+If there is a lakefile.lean present then pass the additional `--lake` option -/
+def runLeanInk (test : FilePath) : IO UInt32 := do
+  let (leanInkExe, realPath) ← getLeanInkExePath
 
   if ! (← leanInkExe.pathExists) then
     IO.println s!"Could not find leanInk executable at {leanInkExe}"
@@ -50,7 +54,25 @@ def runDiff (actual : FilePath) (expected : FilePath) : IO Bool := do
   return actualStr.trim = expectedStr.trim
 
 def copyFile (src : FilePath) (dst : FilePath) : IO Unit := do
-  IO.FS.writeFile dst (← IO.FS.readFile src)
+  IO.FS.writeBinFile dst (← IO.FS.readBinFile src)
+
+def indexOf? [BEq α] (xs : List α) (s : α) (start := 0): Option Nat :=
+  match xs with
+  | [] => none
+  | a :: tail => if a == s then some start else indexOf? tail s (start+1)
+
+def getTargetLeanInkPath : IO (Option FilePath) := do
+  let (leanInkExe, _) ← getLeanInkExePath
+  let lakePath ← IO.appPath
+  let index := indexOf? lakePath.components ".elan"
+  if let some i := index then
+    if let some fileName := leanInkExe.fileName then
+      let elanPath := lakePath.components.take (i + 1)
+      let sep := pathSeparator.toString
+      let elanPath : FilePath := sep.intercalate elanPath
+      let leanInkPath := elanPath / "bin" / fileName
+      return some leanInkPath
+  return none
 
 /-! Walk the `test` folder looking for every `.lean` file that's not a `lakefile` or part of an
 `lean_package` and run `leanInk` on it. If `capture` is true then update the `.lean.leanInk.expected`
@@ -92,4 +114,23 @@ script tests (args) do
 
 script capture (args) do
   IO.println "Updating .leanInk.expected output files"
-  execute True
\ No newline at end of file
+  execute True
+
+script install (args) do
+  IO.println "Installing leanInk..."
+  IO.println "  Building leanInk..."
+  if let some targetPath ← getTargetLeanInkPath then
+    let (_, realPath) ← getLeanInkExePath
+    let out ← IO.Process.output { cmd := "lake", args := #["build"] }
+      if out.exitCode = 0 then
+        IO.println s!"  Built {realPath}..."
+        IO.println s!"  Installing {targetPath}..."
+        copyFile realPath targetPath
+        IO.println s!"  LeanInk successfully installed!"
+        return 0
+      else
+        IO.println s!"### Failed to build leanInk:\n{out.stdout} {out.stderr}"
+        return out.exitCode
+  else
+    IO.println "### Cannot find .elan target directory"
+    return 1