diff --git a/README.md b/README.md
index c4bfbda..f63947c 100644
--- a/README.md
+++ b/README.md
@@ -29,12 +29,9 @@ python3 -m pantograph.search_llm
 
 ## Experiments
 
-In `experiments/`, there is an experiment on running a LLM prover on miniF2F
-data. Run with
-
-```sh
-python3 experiments/miniF2F_search.py [--dry-run]
-```
+In `experiments/`, there are some experiments:
+1. `minif2f/` is an example of executing a SGLANG based prover on the miniF2F dataset
+2. `dsp` is an Lean implementation of Draft-Sketch-Prove
 
 ## Referencing
 
diff --git a/examples/lean4_dsp/readme.md b/examples/lean4_dsp/readme.md
deleted file mode 100644
index f605932..0000000
--- a/examples/lean4_dsp/readme.md
+++ /dev/null
@@ -1,34 +0,0 @@
-# Lean Draft Sketch Prove (DSP)
-
-based on Sean Welleck's DSP for Isabelle: https://github.com/wellecks/ntptutorial/tree/main/partII_dsp
-
-## Related work
-
-### Tony's AF
-Ton'y original AF: ((Yuhuai et al.))[https://arxiv.org/abs/2205.12615]
-Tony's paper improve MiniF2F from: `29.6% to 35.2%`, by `5.6%`. 
-
-Expert Iteration:
--  AF used: "We explore if one can improve neural theorem provers by training the neural models on proofs of automatically translated theorems".
-    - they only translate **problem theorems** (nl_thm := "problem + answer") then use a prover to get the formal proof.
-- ExpIt algorithn:
-    - `M_0 := Isabelle_Thor()`
-    - `Search/Prover := Best_First_Search()`  # TODO recall best first search
-    - ExpIT.fine_tune := "train model to predict next proof_step/tactic given current proof_state and previous proof_step on successful proofs.
-        - i.e., `<x=(proof_state_{t}, proof_step_{t-1}), y=(proof_step_{t})>`  #TODO: I think, confirm with Albert https://twitter.com/messages/1253358235-1267913180153548800
-
-Base Model for Neural Theorem Prover (NTP):
-- Thor_GPT2 := "We use a pre-trained and fine-tuned Thor based on a GPT-2 with 700M non-embedding parameters." Note: ReProver used 299M parameters enc-dec. 
-- fine-tuned on the PILE arxiv + github
-
-Neural Theorem Prover (NTP) for `M_0`:
-- Thor := 
-    - The Thor agent is fine-tuned on the PISA dataset which consists of 2.49 million proof steps from the Isabelle/HOL library.
-    - The model is trained with the objective to predict the next token in va proof step, given the proof state and the last proof step.
-    - proof step := "tactic in Isabelle"  #TODO confirm with Albert https://twitter.com/messages/1253358235-1267913180153548800
-
-Questions: 
-- Q1: what is this: "we perform deduplication by problem statements" when does it matter? All MATH train are unique, so why would I care about this?
-
-Idea:
-- Idea1: use the formal ground truth solution string in MATH, implement Draft Sketch Proof (DSP) for Lean4 + use some symbolic/ntp solver (hammer/tidy/ReProver)
diff --git a/experiments/Example/.gitignore b/experiments/Example/.gitignore
deleted file mode 100644
index 1824d0c..0000000
--- a/experiments/Example/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-/build
-/lakefile.olean
-/lake-packages/*
diff --git a/experiments/Example/Example.lean b/experiments/Example/Example.lean
deleted file mode 100644
index 691b6f7..0000000
--- a/experiments/Example/Example.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Mathlib
-
--- Ensure that Aesop is running
diff --git a/experiments/Example/lake-manifest.json b/experiments/Example/lake-manifest.json
deleted file mode 100644
index 819b64e..0000000
--- a/experiments/Example/lake-manifest.json
+++ /dev/null
@@ -1,75 +0,0 @@
-{"version": "1.1.0",
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "ade8c50c8d1172b974738a01447c29bf6f85f7f8",
-   "name": "proofwidgets",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "ade8c50c8d1172b974738a01447c29bf6f85f7f8",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop.git",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.10.0-rc1",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
-   "name": "Qq",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
-   "name": "importGraph",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "f5c3f06aa7f6d6c221786d2890c345a00e6341f8",
-   "name": "mathlib",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.10.0-rc1",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
- "name": "Example",
- "lakeDir": ".lake"}
diff --git a/experiments/Example/lakefile.lean b/experiments/Example/lakefile.lean
deleted file mode 100644
index 6159006..0000000
--- a/experiments/Example/lakefile.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-import Lake
-open Lake DSL
-
-require proofwidgets from git
-  "https://github.com/leanprover-community/ProofWidgets4" @ "ade8c50c8d1172b974738a01447c29bf6f85f7f8"
-
-require aesop from git
-  "https://github.com/leanprover-community/aesop.git" @ "v4.10.0-rc1"
-
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4" @ "v4.10.0-rc1"
-
-package Example
-
-@[default_target]
-lean_lib Example
diff --git a/experiments/Example/lean-toolchain b/experiments/Example/lean-toolchain
deleted file mode 120000
index 5b8e574..0000000
--- a/experiments/Example/lean-toolchain
+++ /dev/null
@@ -1 +0,0 @@
-../../src/lean-toolchain
\ No newline at end of file
diff --git a/experiments/README.md b/experiments/README.md
deleted file mode 100644
index 8ccd495..0000000
--- a/experiments/README.md
+++ /dev/null
@@ -1,15 +0,0 @@
-# Usage Example
-
-This example showcases how to bind library dependencies and execute the `Aesop`
-tactic in Lean. First build the example project:
-``` sh
-pushd Example
-lake build
-popd
-```
-This would generate compiled `.olean` files. Then run the example from the
-project root:
-``` sh
-poetry run examples/aesop.py
-```
-
diff --git a/examples/lean4_dsp/debug/khan_debug.jsonl b/experiments/dsp/debug/khan_debug.jsonl
similarity index 100%
rename from examples/lean4_dsp/debug/khan_debug.jsonl
rename to experiments/dsp/debug/khan_debug.jsonl
diff --git a/examples/lean4_dsp/debug/mathematica_debug.jsonl b/experiments/dsp/debug/mathematica_debug.jsonl
similarity index 100%
rename from examples/lean4_dsp/debug/mathematica_debug.jsonl
rename to experiments/dsp/debug/mathematica_debug.jsonl
diff --git a/examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug2_sf/n_plus_zero_full_proof.json b/experiments/dsp/debug/toy_example1_dsp/dsp_debug2_sf/n_plus_zero_full_proof.json
similarity index 100%
rename from examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug2_sf/n_plus_zero_full_proof.json
rename to experiments/dsp/debug/toy_example1_dsp/dsp_debug2_sf/n_plus_zero_full_proof.json
diff --git a/examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug2_sf/zero_plus_n_informal_full_proof.json b/experiments/dsp/debug/toy_example1_dsp/dsp_debug2_sf/zero_plus_n_informal_full_proof.json
similarity index 100%
rename from examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug2_sf/zero_plus_n_informal_full_proof.json
rename to experiments/dsp/debug/toy_example1_dsp/dsp_debug2_sf/zero_plus_n_informal_full_proof.json
diff --git a/examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug2_sf/zero_plus_n_informal_proof.json b/experiments/dsp/debug/toy_example1_dsp/dsp_debug2_sf/zero_plus_n_informal_proof.json
similarity index 100%
rename from examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug2_sf/zero_plus_n_informal_proof.json
rename to experiments/dsp/debug/toy_example1_dsp/dsp_debug2_sf/zero_plus_n_informal_proof.json
diff --git a/examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug3_sf.json b/experiments/dsp/debug/toy_example1_dsp/dsp_debug3_sf.json
similarity index 100%
rename from examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug3_sf.json
rename to experiments/dsp/debug/toy_example1_dsp/dsp_debug3_sf.json
diff --git a/examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug4_sf.json b/experiments/dsp/debug/toy_example1_dsp/dsp_debug4_sf.json
similarity index 100%
rename from examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug4_sf.json
rename to experiments/dsp/debug/toy_example1_dsp/dsp_debug4_sf.json
diff --git a/examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_test.json b/experiments/dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_test.json
similarity index 100%
rename from examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_test.json
rename to experiments/dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_test.json
diff --git a/examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_train.json b/experiments/dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_train.json
similarity index 100%
rename from examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_train.json
rename to experiments/dsp/debug/toy_example1_dsp/dsp_debug5_sf/dsp_debug5_sf_train.json
diff --git a/examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug5_sf/readme.md b/experiments/dsp/debug/toy_example1_dsp/dsp_debug5_sf/readme.md
similarity index 100%
rename from examples/lean4_dsp/debug/toy_example1_dsp/dsp_debug5_sf/readme.md
rename to experiments/dsp/debug/toy_example1_dsp/dsp_debug5_sf/readme.md
diff --git a/examples/lean4_dsp/dsp_for_lean4.py b/experiments/dsp/dsp_for_lean4.py
similarity index 100%
rename from examples/lean4_dsp/dsp_for_lean4.py
rename to experiments/dsp/dsp_for_lean4.py
diff --git a/examples/lean4_dsp/dsp_lean_prompts.py b/experiments/dsp/dsp_lean_prompts.py
similarity index 100%
rename from examples/lean4_dsp/dsp_lean_prompts.py
rename to experiments/dsp/dsp_lean_prompts.py
diff --git a/examples/lean4_dsp/dsp_prompt_draft_4_isabelle.py b/experiments/dsp/dsp_prompt_draft_4_isabelle.py
similarity index 100%
rename from examples/lean4_dsp/dsp_prompt_draft_4_isabelle.py
rename to experiments/dsp/dsp_prompt_draft_4_isabelle.py
diff --git a/examples/lean4_dsp/lean_src_proj/.gitignore b/experiments/dsp/lean_src_proj/.gitignore
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/.gitignore
rename to experiments/dsp/lean_src_proj/.gitignore
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/basic_nats/basic_nats.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/basic_nats/basic_nats.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/basic_nats/basic_nats.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/basic_nats/basic_nats.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/basic_nats/basic_nats_af_eval.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/basic_nats/basic_nats_af_eval.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/basic_nats/basic_nats_af_eval.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/basic_nats/basic_nats_af_eval.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/linear_func_eps_delta_limit/linear_func_eps_delta_limit_1.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/linear_func_eps_delta_limit/linear_func_eps_delta_limit_1.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/linear_func_eps_delta_limit/linear_func_eps_delta_limit_1.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/linear_func_eps_delta_limit/linear_func_eps_delta_limit_1.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/linked_lists/linked_lists.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/linked_lists/linked_lists.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/linked_lists/linked_lists.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/linked_lists/linked_lists.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/readme.md b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/readme.md
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/readme.md
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/readme.md
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values_2.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values_2.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values_2.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values_2.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values_3.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values_3.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values_3.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_1_over_x_with_abs_values/vertical_asymptote_1_over_x_with_abs_values_3.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/one_vertical_asymptote.json b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/one_vertical_asymptote.json
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/one_vertical_asymptote.json
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/one_vertical_asymptote.json
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/veritcal_asymptote_of_1_over_x.json b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/veritcal_asymptote_of_1_over_x.json
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/veritcal_asymptote_of_1_over_x.json
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/veritcal_asymptote_of_1_over_x.json
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/veritcal_asymptote_of_1_over_x_2.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/veritcal_asymptote_of_1_over_x_2.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/veritcal_asymptote_of_1_over_x_2.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/veritcal_asymptote_of_1_over_x_2.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_1.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_1.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_1.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_1.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_2.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_2.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_2.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_2.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_3.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_3.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_3.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_3.lean
diff --git a/examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_4.lean b/experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_4.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_4.lean
rename to experiments/dsp/lean_src_proj/AF_manual_evals_examples/vertical_asymptote_of_1_over_x/vertical_asymptote_of_1_over_x_4.lean
diff --git a/examples/lean4_dsp/lean_src_proj/LeanSrcProj.lean b/experiments/dsp/lean_src_proj/LeanSrcProj.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/LeanSrcProj.lean
rename to experiments/dsp/lean_src_proj/LeanSrcProj.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MATH/algebra_379.lean b/experiments/dsp/lean_src_proj/MATH/algebra_379.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MATH/algebra_379.lean
rename to experiments/dsp/lean_src_proj/MATH/algebra_379.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MATH/algebra_4.lean b/experiments/dsp/lean_src_proj/MATH/algebra_4.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MATH/algebra_4.lean
rename to experiments/dsp/lean_src_proj/MATH/algebra_4.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MATH/algebra_683.lean b/experiments/dsp/lean_src_proj/MATH/algebra_683.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MATH/algebra_683.lean
rename to experiments/dsp/lean_src_proj/MATH/algebra_683.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MATH/limit_linear_khan_academy.lean b/experiments/dsp/lean_src_proj/MATH/limit_linear_khan_academy.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MATH/limit_linear_khan_academy.lean
rename to experiments/dsp/lean_src_proj/MATH/limit_linear_khan_academy.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MATH/test_algebra_1json.lean b/experiments/dsp/lean_src_proj/MATH/test_algebra_1json.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MATH/test_algebra_1json.lean
rename to experiments/dsp/lean_src_proj/MATH/test_algebra_1json.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C01_Introduction/S01_Getting_Started.lean b/experiments/dsp/lean_src_proj/MIL/C01_Introduction/S01_Getting_Started.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C01_Introduction/S01_Getting_Started.lean
rename to experiments/dsp/lean_src_proj/MIL/C01_Introduction/S01_Getting_Started.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C01_Introduction/S02_Overview.lean b/experiments/dsp/lean_src_proj/MIL/C01_Introduction/S02_Overview.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C01_Introduction/S02_Overview.lean
rename to experiments/dsp/lean_src_proj/MIL/C01_Introduction/S02_Overview.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C01_Introduction/solutions/Solutions_S01_Getting_Started.lean b/experiments/dsp/lean_src_proj/MIL/C01_Introduction/solutions/Solutions_S01_Getting_Started.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C01_Introduction/solutions/Solutions_S01_Getting_Started.lean
rename to experiments/dsp/lean_src_proj/MIL/C01_Introduction/solutions/Solutions_S01_Getting_Started.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C01_Introduction/solutions/Solutions_S02_Overview.lean b/experiments/dsp/lean_src_proj/MIL/C01_Introduction/solutions/Solutions_S02_Overview.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C01_Introduction/solutions/Solutions_S02_Overview.lean
rename to experiments/dsp/lean_src_proj/MIL/C01_Introduction/solutions/Solutions_S02_Overview.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/S01_Calculating.lean b/experiments/dsp/lean_src_proj/MIL/C02_Basics/S01_Calculating.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/S01_Calculating.lean
rename to experiments/dsp/lean_src_proj/MIL/C02_Basics/S01_Calculating.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean b/experiments/dsp/lean_src_proj/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
rename to experiments/dsp/lean_src_proj/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean b/experiments/dsp/lean_src_proj/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean
rename to experiments/dsp/lean_src_proj/MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean b/experiments/dsp/lean_src_proj/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean
rename to experiments/dsp/lean_src_proj/MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean b/experiments/dsp/lean_src_proj/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean
rename to experiments/dsp/lean_src_proj/MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S01_Calculating.lean b/experiments/dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S01_Calculating.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S01_Calculating.lean
rename to experiments/dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S01_Calculating.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean b/experiments/dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean
rename to experiments/dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S03_Using_Theorems_and_Lemmas.lean b/experiments/dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S03_Using_Theorems_and_Lemmas.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S03_Using_Theorems_and_Lemmas.lean
rename to experiments/dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S03_Using_Theorems_and_Lemmas.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean b/experiments/dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean
rename to experiments/dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean b/experiments/dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean
rename to experiments/dsp/lean_src_proj/MIL/C02_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S02_The_Existential_Quantifier.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/S02_The_Existential_Quantifier.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S02_The_Existential_Quantifier.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/S02_The_Existential_Quantifier.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S03_Negation.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/S03_Negation.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S03_Negation.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/S03_Negation.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S04_Conjunction_and_Iff.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/S04_Conjunction_and_Iff.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S04_Conjunction_and_Iff.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/S04_Conjunction_and_Iff.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S05_Disjunction.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/S05_Disjunction.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S05_Disjunction.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/S05_Disjunction.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S06_Sequences_and_Convergence.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/S06_Sequences_and_Convergence.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/S06_Sequences_and_Convergence.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/S06_Sequences_and_Convergence.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S03_Negation.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S03_Negation.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S03_Negation.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S03_Negation.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S04_Conjunction_and_Iff.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S04_Conjunction_and_Iff.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S04_Conjunction_and_Iff.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S04_Conjunction_and_Iff.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean b/experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean
rename to experiments/dsp/lean_src_proj/MIL/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S01_Sets.lean b/experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S01_Sets.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S01_Sets.lean
rename to experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S01_Sets.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S02_Functions.lean b/experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S02_Functions.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S02_Functions.lean
rename to experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S02_Functions.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean b/experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
rename to experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S01_Sets.lean b/experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S01_Sets.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S01_Sets.lean
rename to experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S01_Sets.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean b/experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean
rename to experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean b/experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean
rename to experiments/dsp/lean_src_proj/MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean b/experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean
rename to experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean b/experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
rename to experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean b/experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean
rename to experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S01_Irrational_Roots.lean b/experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S01_Irrational_Roots.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S01_Irrational_Roots.lean
rename to experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S01_Irrational_Roots.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean b/experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean
rename to experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean b/experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean
rename to experiments/dsp/lean_src_proj/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/S01_Structures.lean b/experiments/dsp/lean_src_proj/MIL/C06_Structures/S01_Structures.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/S01_Structures.lean
rename to experiments/dsp/lean_src_proj/MIL/C06_Structures/S01_Structures.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/S02_Algebraic_Structures.lean b/experiments/dsp/lean_src_proj/MIL/C06_Structures/S02_Algebraic_Structures.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/S02_Algebraic_Structures.lean
rename to experiments/dsp/lean_src_proj/MIL/C06_Structures/S02_Algebraic_Structures.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean b/experiments/dsp/lean_src_proj/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean
rename to experiments/dsp/lean_src_proj/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S01_Structures.lean b/experiments/dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S01_Structures.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S01_Structures.lean
rename to experiments/dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S01_Structures.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S02_Algebraic_Structures.lean b/experiments/dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S02_Algebraic_Structures.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S02_Algebraic_Structures.lean
rename to experiments/dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S02_Algebraic_Structures.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean b/experiments/dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean
rename to experiments/dsp/lean_src_proj/MIL/C06_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/S01_Basics.lean b/experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/S01_Basics.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/S01_Basics.lean
rename to experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/S01_Basics.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/S02_Morphisms.lean b/experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/S02_Morphisms.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/S02_Morphisms.lean
rename to experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/S02_Morphisms.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/S03_Subobjects.lean b/experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/S03_Subobjects.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/S03_Subobjects.lean
rename to experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/S03_Subobjects.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S01_Basics.lean b/experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S01_Basics.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S01_Basics.lean
rename to experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S01_Basics.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S02_Morphisms.lean b/experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S02_Morphisms.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S02_Morphisms.lean
rename to experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S02_Morphisms.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S03_Subobjects.lean b/experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S03_Subobjects.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S03_Subobjects.lean
rename to experiments/dsp/lean_src_proj/MIL/C07_Hierarchies/solutions/Solutions_S03_Subobjects.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C08_Groups_and_Rings/S01_Groups.lean b/experiments/dsp/lean_src_proj/MIL/C08_Groups_and_Rings/S01_Groups.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C08_Groups_and_Rings/S01_Groups.lean
rename to experiments/dsp/lean_src_proj/MIL/C08_Groups_and_Rings/S01_Groups.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C08_Groups_and_Rings/S02_Rings.lean b/experiments/dsp/lean_src_proj/MIL/C08_Groups_and_Rings/S02_Rings.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C08_Groups_and_Rings/S02_Rings.lean
rename to experiments/dsp/lean_src_proj/MIL/C08_Groups_and_Rings/S02_Rings.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C08_Groups_and_Rings/solutions/Solutions_S01_Groups.lean b/experiments/dsp/lean_src_proj/MIL/C08_Groups_and_Rings/solutions/Solutions_S01_Groups.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C08_Groups_and_Rings/solutions/Solutions_S01_Groups.lean
rename to experiments/dsp/lean_src_proj/MIL/C08_Groups_and_Rings/solutions/Solutions_S01_Groups.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C08_Groups_and_Rings/solutions/Solutions_S02_Rings.lean b/experiments/dsp/lean_src_proj/MIL/C08_Groups_and_Rings/solutions/Solutions_S02_Rings.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C08_Groups_and_Rings/solutions/Solutions_S02_Rings.lean
rename to experiments/dsp/lean_src_proj/MIL/C08_Groups_and_Rings/solutions/Solutions_S02_Rings.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/S01_Filters.lean b/experiments/dsp/lean_src_proj/MIL/C09_Topology/S01_Filters.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/S01_Filters.lean
rename to experiments/dsp/lean_src_proj/MIL/C09_Topology/S01_Filters.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/S02_Metric_Spaces.lean b/experiments/dsp/lean_src_proj/MIL/C09_Topology/S02_Metric_Spaces.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/S02_Metric_Spaces.lean
rename to experiments/dsp/lean_src_proj/MIL/C09_Topology/S02_Metric_Spaces.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/S03_Topological_Spaces.lean b/experiments/dsp/lean_src_proj/MIL/C09_Topology/S03_Topological_Spaces.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/S03_Topological_Spaces.lean
rename to experiments/dsp/lean_src_proj/MIL/C09_Topology/S03_Topological_Spaces.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S01_Filters.lean b/experiments/dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S01_Filters.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S01_Filters.lean
rename to experiments/dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S01_Filters.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S02_Metric_Spaces.lean b/experiments/dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S02_Metric_Spaces.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S02_Metric_Spaces.lean
rename to experiments/dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S02_Metric_Spaces.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S03_Topological_Spaces.lean b/experiments/dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S03_Topological_Spaces.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S03_Topological_Spaces.lean
rename to experiments/dsp/lean_src_proj/MIL/C09_Topology/solutions/Solutions_S03_Topological_Spaces.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C10_Differential_Calculus/S01_Elementary_Differential_Calculus.lean b/experiments/dsp/lean_src_proj/MIL/C10_Differential_Calculus/S01_Elementary_Differential_Calculus.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C10_Differential_Calculus/S01_Elementary_Differential_Calculus.lean
rename to experiments/dsp/lean_src_proj/MIL/C10_Differential_Calculus/S01_Elementary_Differential_Calculus.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C10_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean b/experiments/dsp/lean_src_proj/MIL/C10_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C10_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean
rename to experiments/dsp/lean_src_proj/MIL/C10_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C10_Differential_Calculus/solutions/Solutions_S01_Elementary_Differential_Calculus.lean b/experiments/dsp/lean_src_proj/MIL/C10_Differential_Calculus/solutions/Solutions_S01_Elementary_Differential_Calculus.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C10_Differential_Calculus/solutions/Solutions_S01_Elementary_Differential_Calculus.lean
rename to experiments/dsp/lean_src_proj/MIL/C10_Differential_Calculus/solutions/Solutions_S01_Elementary_Differential_Calculus.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C10_Differential_Calculus/solutions/Solutions_S02_Differential_Calculus_in_Normed_Spaces.lean b/experiments/dsp/lean_src_proj/MIL/C10_Differential_Calculus/solutions/Solutions_S02_Differential_Calculus_in_Normed_Spaces.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C10_Differential_Calculus/solutions/Solutions_S02_Differential_Calculus_in_Normed_Spaces.lean
rename to experiments/dsp/lean_src_proj/MIL/C10_Differential_Calculus/solutions/Solutions_S02_Differential_Calculus_in_Normed_Spaces.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S01_Elementary_Integration.lean b/experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S01_Elementary_Integration.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S01_Elementary_Integration.lean
rename to experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S01_Elementary_Integration.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S02_Measure_Theory.lean b/experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S02_Measure_Theory.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S02_Measure_Theory.lean
rename to experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S02_Measure_Theory.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S03_Integration.lean b/experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S03_Integration.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S03_Integration.lean
rename to experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/S03_Integration.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S01_Elementary_Integration.lean b/experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S01_Elementary_Integration.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S01_Elementary_Integration.lean
rename to experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S01_Elementary_Integration.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S02_Measure_Theory.lean b/experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S02_Measure_Theory.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S02_Measure_Theory.lean
rename to experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S02_Measure_Theory.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S03_Integration.lean b/experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S03_Integration.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S03_Integration.lean
rename to experiments/dsp/lean_src_proj/MIL/C11_Integration_and_Measure_Theory/solutions/Solutions_S03_Integration.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Common.lean b/experiments/dsp/lean_src_proj/MIL/Common.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Common.lean
rename to experiments/dsp/lean_src_proj/MIL/Common.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/basic_nats.lean b/experiments/dsp/lean_src_proj/MIL/Rudin/basic_nats.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/basic_nats.lean
rename to experiments/dsp/lean_src_proj/MIL/Rudin/basic_nats.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/cuts.lean b/experiments/dsp/lean_src_proj/MIL/Rudin/cuts.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/cuts.lean
rename to experiments/dsp/lean_src_proj/MIL/Rudin/cuts.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/example_1p1_thm_A_no_max.lean b/experiments/dsp/lean_src_proj/MIL/Rudin/example_1p1_thm_A_no_max.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/example_1p1_thm_A_no_max.lean
rename to experiments/dsp/lean_src_proj/MIL/Rudin/example_1p1_thm_A_no_max.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/field_bm.lean b/experiments/dsp/lean_src_proj/MIL/Rudin/field_bm.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/field_bm.lean
rename to experiments/dsp/lean_src_proj/MIL/Rudin/field_bm.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/play_ground_lean.lean b/experiments/dsp/lean_src_proj/MIL/Rudin/play_ground_lean.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/play_ground_lean.lean
rename to experiments/dsp/lean_src_proj/MIL/Rudin/play_ground_lean.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/playground/carrier_equivalence_thm.lean b/experiments/dsp/lean_src_proj/MIL/Rudin/playground/carrier_equivalence_thm.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/playground/carrier_equivalence_thm.lean
rename to experiments/dsp/lean_src_proj/MIL/Rudin/playground/carrier_equivalence_thm.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/playground/show_universe_is_not_empty.lean b/experiments/dsp/lean_src_proj/MIL/Rudin/playground/show_universe_is_not_empty.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/playground/show_universe_is_not_empty.lean
rename to experiments/dsp/lean_src_proj/MIL/Rudin/playground/show_universe_is_not_empty.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/md/rudin_real_analysis.md b/experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/md/rudin_real_analysis.md
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/md/rudin_real_analysis.md
rename to experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/md/rudin_real_analysis.md
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/rudin_real_analysis.pdf b/experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/rudin_real_analysis.pdf
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/rudin_real_analysis.pdf
rename to experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/rudin_real_analysis.pdf
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/rudin_real_analysis.zip b/experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/rudin_real_analysis.zip
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/rudin_real_analysis.zip
rename to experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/rudin_real_analysis.zip
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/2023_08_17_055ccbec3ce53a1b74ebg.tex b/experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/2023_08_17_055ccbec3ce53a1b74ebg.tex
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/2023_08_17_055ccbec3ce53a1b74ebg.tex
rename to experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/2023_08_17_055ccbec3ce53a1b74ebg.tex
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-001.jpg b/experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-001.jpg
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-001.jpg
rename to experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-001.jpg
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-039.jpg b/experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-039.jpg
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-039.jpg
rename to experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-039.jpg
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-086.jpg b/experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-086.jpg
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-086.jpg
rename to experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-086.jpg
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-226.jpg b/experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-226.jpg
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-226.jpg
rename to experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-226.jpg
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-348.jpg b/experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-348.jpg
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-348.jpg
rename to experiments/dsp/lean_src_proj/MIL/Rudin/rudin_real_analysis_txt/tex/images/2023_08_17_055ccbec3ce53a1b74ebg-348.jpg
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/theorem_1p19_orderded_field_with_lub_exists.lean b/experiments/dsp/lean_src_proj/MIL/Rudin/theorem_1p19_orderded_field_with_lub_exists.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/theorem_1p19_orderded_field_with_lub_exists.lean
rename to experiments/dsp/lean_src_proj/MIL/Rudin/theorem_1p19_orderded_field_with_lub_exists.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MIL/Rudin/thm_1p11_sup_eq_lub.lean b/experiments/dsp/lean_src_proj/MIL/Rudin/thm_1p11_sup_eq_lub.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MIL/Rudin/thm_1p11_sup_eq_lub.lean
rename to experiments/dsp/lean_src_proj/MIL/Rudin/thm_1p11_sup_eq_lub.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MyProject/Test.lean b/experiments/dsp/lean_src_proj/MyProject/Test.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MyProject/Test.lean
rename to experiments/dsp/lean_src_proj/MyProject/Test.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MyProject/basic_nats.lean b/experiments/dsp/lean_src_proj/MyProject/basic_nats.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MyProject/basic_nats.lean
rename to experiments/dsp/lean_src_proj/MyProject/basic_nats.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MyProject/inference_rules/intro_elim_rules.lean b/experiments/dsp/lean_src_proj/MyProject/inference_rules/intro_elim_rules.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MyProject/inference_rules/intro_elim_rules.lean
rename to experiments/dsp/lean_src_proj/MyProject/inference_rules/intro_elim_rules.lean
diff --git a/examples/lean4_dsp/lean_src_proj/MyProject/playground.lean b/experiments/dsp/lean_src_proj/MyProject/playground.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/MyProject/playground.lean
rename to experiments/dsp/lean_src_proj/MyProject/playground.lean
diff --git a/examples/lean4_dsp/lean_src_proj/PlayGround/aesop_pg.lean b/experiments/dsp/lean_src_proj/PlayGround/aesop_pg.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/PlayGround/aesop_pg.lean
rename to experiments/dsp/lean_src_proj/PlayGround/aesop_pg.lean
diff --git a/examples/lean4_dsp/lean_src_proj/Putnam_in_lean4/putnam_2023.lean b/experiments/dsp/lean_src_proj/Putnam_in_lean4/putnam_2023.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/Putnam_in_lean4/putnam_2023.lean
rename to experiments/dsp/lean_src_proj/Putnam_in_lean4/putnam_2023.lean
diff --git a/examples/lean4_dsp/lean_src_proj/Putnam_in_lean4/readme.md b/experiments/dsp/lean_src_proj/Putnam_in_lean4/readme.md
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/Putnam_in_lean4/readme.md
rename to experiments/dsp/lean_src_proj/Putnam_in_lean4/readme.md
diff --git a/examples/lean4_dsp/lean_src_proj/README.md b/experiments/dsp/lean_src_proj/README.md
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/README.md
rename to experiments/dsp/lean_src_proj/README.md
diff --git a/examples/lean4_dsp/lean_src_proj/Toy_Examples_For_PyPantograph/basic_nats_using_mathlib_nats.lean b/experiments/dsp/lean_src_proj/Toy_Examples_For_PyPantograph/basic_nats_using_mathlib_nats.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/Toy_Examples_For_PyPantograph/basic_nats_using_mathlib_nats.lean
rename to experiments/dsp/lean_src_proj/Toy_Examples_For_PyPantograph/basic_nats_using_mathlib_nats.lean
diff --git a/examples/lean4_dsp/lean_src_proj/Toy_Examples_For_PyPantograph/basic_nats_using_mathlib_nats2_simp_no_rw.lean b/experiments/dsp/lean_src_proj/Toy_Examples_For_PyPantograph/basic_nats_using_mathlib_nats2_simp_no_rw.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/Toy_Examples_For_PyPantograph/basic_nats_using_mathlib_nats2_simp_no_rw.lean
rename to experiments/dsp/lean_src_proj/Toy_Examples_For_PyPantograph/basic_nats_using_mathlib_nats2_simp_no_rw.lean
diff --git a/examples/lean4_dsp/lean_src_proj/lake-manifest.json b/experiments/dsp/lean_src_proj/lake-manifest.json
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/lake-manifest.json
rename to experiments/dsp/lean_src_proj/lake-manifest.json
diff --git a/examples/lean4_dsp/lean_src_proj/lakefile.lean b/experiments/dsp/lean_src_proj/lakefile.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/lakefile.lean
rename to experiments/dsp/lean_src_proj/lakefile.lean
diff --git a/examples/lean4_dsp/lean_src_proj/lean-toolchain b/experiments/dsp/lean_src_proj/lean-toolchain
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/lean-toolchain
rename to experiments/dsp/lean_src_proj/lean-toolchain
diff --git a/examples/lean4_dsp/lean_src_proj/lean_basics/basic_nats.lean b/experiments/dsp/lean_src_proj/lean_basics/basic_nats.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/lean_basics/basic_nats.lean
rename to experiments/dsp/lean_src_proj/lean_basics/basic_nats.lean
diff --git a/examples/lean4_dsp/lean_src_proj/lean_basics/lim_lin.lean b/experiments/dsp/lean_src_proj/lean_basics/lim_lin.lean
similarity index 100%
rename from examples/lean4_dsp/lean_src_proj/lean_basics/lim_lin.lean
rename to experiments/dsp/lean_src_proj/lean_basics/lim_lin.lean
diff --git a/examples/lean4_dsp/solve/dsp_lean_prompts.py b/experiments/dsp/solve/dsp_lean_prompts.py
similarity index 100%
rename from examples/lean4_dsp/solve/dsp_lean_prompts.py
rename to experiments/dsp/solve/dsp_lean_prompts.py
diff --git a/examples/lean4_dsp/solve/dsp_prompt_draft_4_isabelle.py b/experiments/dsp/solve/dsp_prompt_draft_4_isabelle.py
similarity index 100%
rename from examples/lean4_dsp/solve/dsp_prompt_draft_4_isabelle.py
rename to experiments/dsp/solve/dsp_prompt_draft_4_isabelle.py
diff --git a/examples/lean4_dsp/solve/readme.md b/experiments/dsp/solve/readme.md
similarity index 100%
rename from examples/lean4_dsp/solve/readme.md
rename to experiments/dsp/solve/readme.md
diff --git a/experiments/miniF2F_search.py b/experiments/minif2f/main.py
similarity index 100%
rename from experiments/miniF2F_search.py
rename to experiments/minif2f/main.py
diff --git a/experiments/test.jsonl b/experiments/minif2f/test.jsonl
similarity index 100%
rename from experiments/test.jsonl
rename to experiments/minif2f/test.jsonl
diff --git a/experiments/valid.jsonl b/experiments/minif2f/valid.jsonl
similarity index 100%
rename from experiments/valid.jsonl
rename to experiments/minif2f/valid.jsonl