diff --git a/Projects/mathlib-demo/MathlibLatest.lean b/Projects/mathlib-demo/MathlibLatest.lean
new file mode 100644
index 00000000..15744b2b
--- /dev/null
+++ b/Projects/mathlib-demo/MathlibLatest.lean
@@ -0,0 +1,8 @@
+import Webeditor
+import Mathlib
+import ProofWidgets
+
+import MathlibLatest.Bijection
+import MathlibLatest.Logic
+import MathlibLatest.Rational
+import MathlibLatest.Ring
diff --git a/Projects/mathlib-demo/MathlibLatest/Bijection.lean b/Projects/mathlib-demo/MathlibLatest/Bijection.lean
new file mode 100644
index 00000000..1c135014
--- /dev/null
+++ b/Projects/mathlib-demo/MathlibLatest/Bijection.lean
@@ -0,0 +1,25 @@
+import Mathlib.Logic.Equiv.Basic -- import the theory
+-- of bijections as functions with two-sided inverses
+
+-- Let X, Y and Z be sets
+variable (X Y Z : Type)
+
+-- Then there's a bijection between functions `X × Y → Z`
+-- and functions from `X` to (the space of functions from `Y` to `Z`).
+
+example : (X × Y → Z) ≃ (X → (Y → Z)) :=
+{ -- to go from f : X × Y → Z to a function X → (Y → Z),
+  -- send x and y to f(x,y)
+  toFun := fun f ↦ (fun x y ↦ f (x,y))
+  -- to go from g : X → (Y → Z) to a function X × Y → Z,
+  -- send a pair p=(x,y) to (g p.1) (p.2) where p.i is the i'th element of p
+  invFun := fun g ↦ (fun p ↦ g p.1 p.2)
+  -- Here we prove that if f ↦ g ↦ f' then f' = f
+  left_inv := by
+    intro f -- let f : X × Y → Z be arbitrary.
+    rfl -- turns out f' = f by definition
+  -- here we prove that if g ↦ f ↦ g' then g' = g
+  right_inv := by
+    intro g -- let f : X → (Y → Z) by arbitrary
+    rfl -- turns out that g' = g by definition
+}
diff --git a/Projects/mathlib-demo/MathlibLatest/Logic.lean b/Projects/mathlib-demo/MathlibLatest/Logic.lean
new file mode 100644
index 00000000..ddcfe43f
--- /dev/null
+++ b/Projects/mathlib-demo/MathlibLatest/Logic.lean
@@ -0,0 +1,15 @@
+import Mathlib.Logic.Basic -- basic facts in logic
+-- theorems in Lean's mathematics library
+
+-- Let P and Q be true-false statements
+variable (P Q : Prop)
+
+-- The following is a basic result in logic
+example : ¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q := by
+  -- its proof is already in Lean's mathematics library
+  exact not_and_or
+
+-- Here is another basic result in logic
+example : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q := by
+  apply? -- we can search for the proof in the library
+  -- we can also replace `apply?` with its output
diff --git a/Projects/mathlib-demo/MathlibLatest/Rational.lean b/Projects/mathlib-demo/MathlibLatest/Rational.lean
new file mode 100644
index 00000000..c8626d90
--- /dev/null
+++ b/Projects/mathlib-demo/MathlibLatest/Rational.lean
@@ -0,0 +1,16 @@
+import Mathlib.Data.Rat.Order -- import the rationals
+import Mathlib.Data.Rat.Init -- import notation ℚ for rationals
+import Mathlib.Tactic.Linarith -- a linear arithmetic tactic
+import Mathlib.Tactic.Ring -- import the `ring` tactic
+
+-- let `x`, `y` and `z` be rationals
+variable (x y z : ℚ)
+
+-- let's prove that if `x < y` and `y + 3 < z + 10` then `x + 37 < z + 44`
+example (h₁ : x < y) (h₂ : y + 3 < z + 10) : x + 37 < z + 44 := by
+  linarith -- the `linarith` tactic can do this automatically
+
+-- let's prove that (x+y)^2=x^2+2*x*y+y^2
+
+example : (x + y)^2 = x^2 + 2 * x * y + y^2 := by
+  ring -- the `ring` tactic can do this automatically
diff --git a/Projects/mathlib-demo/MathlibLatest/Ring.lean b/Projects/mathlib-demo/MathlibLatest/Ring.lean
new file mode 100644
index 00000000..e77849f0
--- /dev/null
+++ b/Projects/mathlib-demo/MathlibLatest/Ring.lean
@@ -0,0 +1,13 @@
+import Mathlib.Tactic.Ring -- import the `ring` tactic
+
+-- let R be a commutative ring (for example the real numbers)
+variable (R : Type) [CommRing R]
+
+-- let x and y be elements of R
+variable (x y : R)
+
+-- then (x+y)*(x+2y)=x^2+3xy+2y^2
+
+example : (x+y)*(x+2*y)=x^2+3*x*y+2*y^2 := by
+  -- the `ring` tactic solves this goal automatically
+  ring
diff --git a/Projects/mathlib-demo/build.sh b/Projects/mathlib-demo/build.sh
new file mode 100755
index 00000000..751de763
--- /dev/null
+++ b/Projects/mathlib-demo/build.sh
@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+
+# Operate in the directory where this file is located
+cd $(dirname $0)
+
+# Updating Mathlib: We follow the instructions at
+# https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4
+
+# Note: we had once problems with the `lake-manifest` when a new dependency got added
+# to `mathlib`, we may need to add `rm lake-manifest.json` again if that's still a problem.
+
+# currently the mathlib post-update-hook is not good enough to update the lean-toolchain.
+# things break if the new lakefile is not valid in the old lean version
+curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
+
+# note: mathlib has now a post-update hook that modifies the `lean-toolchain`
+# and calls `lake exe cache get`.
+
+lake update -R
+lake build
diff --git a/Projects/mathlib-demo/lake-manifest.json b/Projects/mathlib-demo/lake-manifest.json
new file mode 100644
index 00000000..2bff6b92
--- /dev/null
+++ b/Projects/mathlib-demo/lake-manifest.json
@@ -0,0 +1,77 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.30",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "rev": "61ad21e8d0386579b09dc2ecc8f34dc46877d02a",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/hhu-adam/lean4web-tools.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "9e6468e250c05450eedf4aff6e30290fb409af2b",
+   "name": "webeditor",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "mathlibLatest",
+ "lakeDir": ".lake"}
diff --git a/Projects/mathlib-demo/lakefile.lean b/Projects/mathlib-demo/lakefile.lean
new file mode 100644
index 00000000..2ae0b9ab
--- /dev/null
+++ b/Projects/mathlib-demo/lakefile.lean
@@ -0,0 +1,17 @@
+import Lake
+open Lake DSL
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4"@"master"
+
+require webeditor from git
+  "https://github.com/hhu-adam/lean4web-tools.git" @ "main"
+
+package mathlibLatest {
+  -- add package configuration options here
+}
+
+@[default_target]
+lean_lib MathlibLatest {
+  -- add library configuration options here
+}
diff --git a/Projects/mathlib-demo/lean-toolchain b/Projects/mathlib-demo/lean-toolchain
new file mode 100644
index 00000000..9ad30404
--- /dev/null
+++ b/Projects/mathlib-demo/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.7.0