-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
mike dupont
committed
Feb 1, 2024
1 parent
86f920d
commit 6bc8bdc
Showing
5 changed files
with
54 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
* updated idea. | ||
|
||
1. create high hevel english text | ||
2. extract the list of sets,types,kinds,sorts,categories,and universes in the text. | ||
3. create a definitions in coq that represent the basic ideas from the text, the dsl. | ||
4. add in decriptions of coq, the os, the languages around it and in it. | ||
5. now write basic theories and proofs about the dsl, even trival ones. | ||
6. now look in unimath for what parts could apply to this DSL | ||
7. connect the proof of the application DSL to unimath | ||
8. show how unimath applys to the application of the user | ||
9. extract a workflow from the unimath proof to apply to the user data. | ||
10. use the llm to interpret the applied proof of the unimath to the domain specific language | ||
|
||
* extract chunks out of org mode file and feed them to the llm. | ||
keep track of each chunk as a goal to be followed in the proof engine. | ||
use hashs and content addressable lookup and canonical form to break up the data. | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
* orfeus as actor/demigod | ||
|
||
the orfeus character acts as a god and human, as composor and actor in his own art. | ||
he represents the story teller who writes himself into the story. | ||
|
||
so the idea of the introspector as the bard warrior that explains what | ||
we are seeing in an easier to consume manner, | ||
singing a tale of the data but also being an actor in it. | ||
|
||
in that respect the story is about the poet and the story creates the poet, so it is autopoetic and writes itself into existance. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
* comic book | ||
|
||
we can think of this idea of translating unimath into a video or comic book | ||
as a translation of the module of unimath into pages or chapters or series of books. | ||
the entire unimath would be an epic amount of books to contain all the details. | ||
so there would be a function mapping one system onto the other and back | ||
a multi layered encoding of colors and symmetries and eigenvalues and eigenvectors | ||
and directions and morphisms between the math and the art that it is embedded into. | ||
we can then later embed the art back into unimath and show that there are layered representations | ||
of the same thing. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
create an ocaml function that takes a string and converts it into a one way function checksum shorter string by hashing or other summarization techniques. | ||
it should create a content address that includes projects,lanuage,syntax,semantics,and pointers for more information. | ||
it can be structured or an autoencoder. It can be lossy up to the parameter specified so we can generate a range of functions with different attributes. | ||
it has the ability to emit itself as a new function so it can rewrite itself. | ||
it can reflect over its own source code. | ||
it can write itself into existance. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters