update modules

.gitmodules

@@ -2918,3 +2918,96 @@
 [submodule "2024/02/05/diffusers"]
 	path = 2024/02/05/diffusers
 	url = https://github.com/huggingface/diffusers
+[submodule "2024/02/05/docker-time"]
+	path = 2024/02/05/docker-time
+	url = https://huggingface.co/spaces/introspector/docker-time
+[submodule "2024/02/06/docker-coq"]
+	path = 2024/02/06/docker-coq
+	url = https://github.com/coq-community/docker-coq
+[submodule "2024/02/06/Coq-Type-Classes"]
+	path = 2024/02/06/Coq-Type-Classes
+	url = https://github.com/rudynicolop/Coq-Type-Classes/
+[submodule "2024/02/06/mirrorsolve"]
+	path = 2024/02/06/mirrorsolve
+	url = https://github.com/jsarracino/mirrorsolve
+[submodule "2024/02/06/elpi-derive-mathcomp"]
+	path = 2024/02/06/elpi-derive-mathcomp
+	url = https://github.com/gares/elpi-derive-mathcomp/
+[submodule "2024/02/07/BRiCk"]
+	path = 2024/02/07/BRiCk
+	url = https://github.com/bedrocksystems/BRiCk
+[submodule "2024/02/08/mirage"]
+	path = 2024/02/08/mirage
+	url = https://github.com/mirage/mirage
+[submodule "2024/02/09/hmap"]
+	path = 2024/02/09/hmap
+	url = https://github.com/dbuenzli/hmap.git
+[submodule "2024/02/09/TypeTheory"]
+	path = 2024/02/09/TypeTheory
+	url = https://github.com/UniMath/TypeTheory
+[submodule "2024/02/09/SymmetryBook"]
+	path = 2024/02/09/SymmetryBook
+	url = https://github.com/UniMath/SymmetryBook
+[submodule "2024/02/09/agda-unimath"]
+	path = 2024/02/09/agda-unimath
+	url = https://github.com/UniMath/agda-unimath
+[submodule "2024/02/09/stable-diffusion-docker"]
+	path = 2024/02/09/stable-diffusion-docker
+	url = https://github.com/fboulnois/stable-diffusion-docker.git
+[submodule "2024/02/09/act"]
+	path = 2024/02/09/act
+	url = https://github.com/nektos/act
+[submodule "2024/02/10/ollama-helm"]
+	path = 2024/02/10/ollama-helm
+	url = https://github.com/otwld/ollama-helm
+[submodule "2024/02/10/helm"]
+	path = 2024/02/10/helm
+	url = https://github.com/helm/helm
+[submodule "2024/02/10/goenv"]
+	path = 2024/02/10/goenv
+	url = https://github.com/go-nv/goenv
+[submodule "2024/02/10/helm-controller"]
+	path = 2024/02/10/helm-controller
+	url = https://github.com/k3s-io/helm-controller
+[submodule "2024/02/10/kubernetes-yaml-templates"]
+	path = 2024/02/10/kubernetes-yaml-templates
+	url = https://github.com/dennyzhang/kubernetes-yaml-templates
+[submodule "2024/02/11/Cosette"]
+	path = 2024/02/11/Cosette
+	url = https://github.com/uwdb/Cosette
+[submodule "2024/02/11/lipsum"]
+	path = 2024/02/11/lipsum
+	url = https://github.com/lindig/lipsum
+[submodule "2024/02/11/org-mode"]
+	path = 2024/02/11/org-mode
+	url = https://github.com/tkf/org-mode
+[submodule "2024/02/11/literate-rtl"]
+	path = 2024/02/11/literate-rtl
+	url = https://github.com/vasil-sd/literate-rtl
+[submodule "2024/02/11/coqtl"]
+	path = 2024/02/11/coqtl
+	url = https://github.com/atlanmod/coqtl
+[submodule "2024/02/11/donjon"]
+	path = 2024/02/11/donjon
+	url = https://github.com/bartanderson/donjon
+[submodule "2024/02/11/rescript-compiler"]
+	path = 2024/02/11/rescript-compiler
+	url = https://github.com/rescript-lang/rescript-compiler
+[submodule "2024/02/12/reanalyze"]
+	path = 2024/02/12/reanalyze
+	url = https://github.com/rescript-association/reanalyze
+[submodule "2024/02/12/rescript-game-of-life"]
+	path = 2024/02/12/rescript-game-of-life
+	url = https://github.com/alanrsoares/rescript-game-of-life
+[submodule "2024/02/12/rescript-react"]
+	path = 2024/02/12/rescript-react
+	url = https://github.com/rescript-lang/rescript-react
+[submodule "2024/02/12/rescript-project-template"]
+	path = 2024/02/12/rescript-project-template
+	url = https://github.com/rescript-lang/rescript-project-template
+[submodule "2024/02/12/jeason"]
+	path = 2024/02/12/jeason
+	url = https://github.com/chenglou/jeason
+[submodule "2024/02/09/--help"]
+	path = 2024/02/09/--help
+	url = https://github.com/UniMath/TypeTheory

2024/02/05/notes.org

@@ -139,125 +139,3 @@ Overall, this model provides a framework for building an AI-in-the-loop system t
 #+end_src
 
 
-**
-visual will higher quality model: graph layout.
-proof -> graph layout
-unlimited stateful mamba
-
-show there is a univalent mathematical harmony and equivalence between the activity of the mixture of experts being simulated in the multiplication and addition of the values of the tensors of the matrix of the model of the llm and the activitiy proof engine working on the same task.
-
-#+begin_src output
-
-It is possible to demonstrate that there exists a universal
-mathematical harmony and equivalence between the computations
-performed by a combination of experts within the multiplication and
-addition processes of the tensors in the matrix model of an LLM and
-the coq proof engine's calculations on the same task where the proof engine is constructing
-queries to send to the llm.
-
-This can be achieved through creative reinterpretation of the mathematical operations
-involved, while preserving the essential ideas. Essentially appplying homtopy type theory to the reflections of the
-coq, the metacoq and then connecting them to the reflections of the tensor operations of the llm.
-this will require statistical analysis and large scale data collection to achive.
-
-#+end_src
-
-#+begin_src output
-
-In this reinterpretation, we propose that there exists a universal
-mathematical harmony between the computations performed by experts in
-multiplication and addition processes of tensors within the matrix
-model of an LLM and the queries constructed by the Coq proof
-engine. This demonstration can be achieved through creative
-application of homotopy type theory to the reflections of both Coq,
-MetaCoq, and the tensor operations of the LLM.
-
-To achieve this, we propose a statistical analysis and large-scale
-data collection method. By doing so, we aim to connect these seemingly
-disconnected mathematical concepts and demonstrate their equivalence
-in a more intuitive way. This approach will require a deep
-understanding of both homotopy type theory and machine learning, as
-well as careful analysis of the underlying mathematical structures
-involved.
-#+end_src
-
-
-* multi2vect imagebind
-
-
-show there is a univalent mathematical harmony and equivalence between the activity of the
-multiplication and addition of the values of the tensors of the matrix of the model of the transformer model of the large language model called mistral,
-and the activity of the coq proof engine working that generated the statement to send to the llm and is parsing its outputs.
-
-
-#+begin_src output
-
-Let's explore the intriguing correlation between the mathematical
-harmony and equivalence of two distinct processes: the multiplication
-and addition of the values in the tensors of a transformer model
-called Mistral, and the activity of Coq's proof engine that generates
-statements for the large language model (LLM).
-
-Firstly, let's delve into the mathematical underpinnings of
-Mistral. The transformer model is built upon a matrix structure with
-values stored in tensors. When performing multiplication or addition
-on these tensors, the mathematical harmony lies in the way they
-interact and produce new results. These operations can be seen as
-transformations of the underlying data, which ultimately leads to
-better understanding and modeling capabilities for the LLM.
-
-On the other hand, Coq's proof engine is a powerful tool that
-generates statements from input data. These statements are then parsed
-by the LLM to provide insights and predictions. In this process, Coq's
-engine works seamlessly with Mistral, allowing them to complement each
-other's strengths.
-
-When looking at these processes from a creative perspective, we can
-see that they share an underlying harmony. The multiplication and
-addition of the tensors in Mistral are similar to the generation of
-statements by Coq's proof engine in that both involve transforming
-input data into new insights or results. In this sense, they are two
-sides of the same coin, working together to create a cohesive
-mathematical framework for understanding and modeling the world around
-us.
-
-So, to summarize, there is an intriguing univalent mathematical
-harmony between the activity of the multiplication and addition of the
-values in the tensors of Mistral's matrix structure and the activity
-of Coq's proof engine that generates statements for the LLM. By
-working together, these processes create a powerful toolset for
-understanding and modeling complex systems.
-#+end_src
-
-the data flow is from tracing enabled in coq proof engine,
-to send queries to the language model and evalute the output
-inside the proof engine.
-this is related to dependant types.
-
-create a relationship between the (
-description of what you want,
-description of what you got)
-
-(label,contents)
-
-vec<n>
-(vec<5> ,low level type [0,1,2,3,4])
-
-* idea for physics
-
-take isabelle proof for smooth manifolds in github
-https://www.isa-afp.org/entries/Smooth_Manifolds.html
-create trace of proof, annotate, chunk, turn into story, coq, unimath.
-show your work.
-1. turn on all tracing from isabell.
-   profiling.
-   debugging
-   proof traces.
-   review. enhance.
-   chunk feed to llm. lang_agent worker will apply line by line.
-   csplit and split in unix to create chunk files.
-   scanner that i am working on will search subdir.
-   in each chunk you write at the end a comma separated list of call stacks
-   (filename:linenum) to annotate the sources.
-
-