diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
index 66c9583..ff2fbb6 100644
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -14,5 +14,9 @@
 				"leanprover.lean4"
 			]
 		}
-	}
+	},
+	"postCreateCommand": [
+		"lake update",
+		"lake exe cache get"
+	]
 }
diff --git a/Prova/MathlibExample.lean b/Prova/MathlibExample.lean
new file mode 100644
index 0000000..0849845
--- /dev/null
+++ b/Prova/MathlibExample.lean
@@ -0,0 +1,3 @@
+import Mathlib.Topology.Basic
+
+#check TopologicalSpace
diff --git a/README.md b/README.md
index 4e34d8f..eb76da7 100644
--- a/README.md
+++ b/README.md
@@ -1,20 +1,20 @@
 # Lean Codespace
 
-Questa repo contiene un semplice progetto in Lean che può essere lanciato con un click su GitHub CodeSpaces (ambiente di sviluppo nel cloud dal browser) provarlo senza dover installare nulla in locale.
+Questa repo contiene un semplice progetto in Lean con Mathlib che può essere lanciato con un click su GitHub CodeSpace (ambiente di sviluppo nel cloud dal browser) provarlo senza dover installare nulla in locale.
 
 ## GitHub / GitHub Pro con Unipi
 
 GitHub già offre 120h gratuite al mese di utilizzo di CodeSpaces, inoltre [Unipi con GitHub Pro](https://www.dm.unipi.it/github-pro/) ci fa arrivare a 180h gratuite di utilizzo al mese.  
 
-[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?skip_quickstart=true&hide_repo_select=true&ref=main&repo=698191991&machine=basicLinux32gb&location=WestEurope)
+[![Open in GitHub Codespaces](https://github.com/codespaces/badge.svg)](https://github.com/codespaces/new?skip_quickstart=true&hide_repo_select=true&ref=main&repo=698191991&machine=standardLinux32gb&location=WestEurope)
 
 > :warning: **Achtung** :warning: 
 > 
-> - Le 120h o 180h sono "core hours" quindi con la macchina da 2 core sono complessivamente 60h o 90h effettive al mese (le opzioni sono 2 o 4 core ma già quella da 2 dovrebbe bastare). Essenzialmente conviene usare con parsimonia le ore di questi GitHub CodeSpaces.
+> - Le 120h o 180h sono "core hours" quindi con la macchina da 2 core sono complessivamente 60h o 90h effettive al mese (per far compilare tutto più velocemente all'inizio conviene usare quella da 4 core ma poi si può passare a quella da 2). Essenzialmente conviene usare con parsimonia le ore di questi GitHub CodeSpaces.
 > 
 > - In particolare quando si ha finito di utilizzare il codespace ricordarsi di spegnerlo dalla pagina <https://github.com/codespaces>, dalla lista di codespaces se c'è scritto ancora **"Active"** premere sui tre puntini e fare **"Stop Container"**.
 
-Per provare che tutto funzioni andare in `./Main.lean` e verificare che si apra il pannello laterale e che mettendo il mouse sopra `#eval` venga mostrata la stringa `Hello, World!`.
+Per provare che tutto funzioni andare in `./Prova/MathlibExample.lean` e verificare che si apra il pannello laterale e che mettendo il mouse sopra `#check TopologicalSpace` venga mostrata la stringa `TopologicalSpace.{u} (α : Type u) : Type u` (all'inizio vengono compilate molte cose quindi potrebbe comparire per qualche minuto un underline blue sotto il primo import)
 
 ## Siti Utili
 
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..c64c97f
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,52 @@
+{"version": 6,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "071f47d27115f6b801ba2e4ba42334817abf2446",
+    "opts": {},
+    "name": "mathlib",
+    "inputRev?": null,
+    "inherited": false}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "opts": {},
+    "name": "Qq",
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "4f8b397237411249930791f1cba0a9d2880a02dd",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/mhuisi/lean4-cli.git",
+    "subDir?": null,
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/EdAyers/ProofWidgets4",
+    "subDir?": null,
+    "rev": "9f68f14df384f43b74aeb2908b97ae54a0ad9d95",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.17",
+    "inherited": true}}],
+ "name": "prova"}
diff --git a/lakefile.lean b/lakefile.lean
index 92e2815..3ffec2a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,6 +7,9 @@ package prova where
 lean_lib Prova where
   -- add library configuration options here
 
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
+    
 @[default_target]
 lean_exe «prova» where
   root := `Main