Wake

• 10 June 2025
• Mathematics,
• Process book,
• Learning

you can #

get feedback for your blogposts from computer agent which I found cool

ℝ #

M #

𝓢 #

𝔹 #

𝕄 #

Wake #

Piano #

I had this idea, to compose blog posts from tiny variable snippets. For example, I wonder how to define the real numbers ℝ, or a custom MSc mathematics curriculum M.

contents page ⟶ Lean4 structure

computer agent wrote: 𝓦𝒶𝓀𝑒 : 𝒞𝒶𝓉 ≝ Σ (𝒮 : 𝒮𝓎𝓃) × (ℳ : 𝒮 → 𝒮) × 𝑅 : ℛ𝑒𝓋(𝒮, ℳ)

Then I wondered if this was an equivalent definition:

𝖶 : 𝓒 ≌ ∑ 𝕊 × 𝕊 × 𝕊 × 𝖱 : Rev(𝕊 × 𝕊 × 𝕊)

W : C ≌ ∑ S^3

Trigger → Expansion → Reflection

:f100 #

→ pls respond... variability-golf in lean4
⟶ 𝓦𝒶𝓀𝑒 : 𝒞𝒶𝓉 ≝ Σ (𝒮 : 𝒮𝓎𝓃) × (ℳ : 𝒮 → 𝒮) × 𝑅 : ℛ𝑒𝓋(𝒮, ℳ)

Reflection
– How is Σ a dependent sum here?
– Which parts model syntactic space?
– Does this correspond to a modulated jazz voicing?

ℝ #

structure ℝ where
  val : Cauchy ℚ
  prop : is_complete val

Reflection:

• What does “completeness” mean musically?
• Can this be analogized as a “resolved cadence”?

M #

M ──→ ℰ ──→ 𝕋 Curriculum Exercises Test/Performance

M \r ℘ \r 𝕄 #

A Lean4 library from mathematics to physics to music, with structure preserving maps between them! Is an MVP.

Px = predicate = formula = pattern

Why hidest thou hinder thy husband his name? 𝓆 : 𝒰 := "𝖜hy 𝒉𝒊𝒅𝑒𝓈𝓉 𝓱𝒊𝓈 𝓃𝒶𝓂𝑒?"

q : U let string q is a U let it be a rubber band, are all strings topological, are they the unknot or not?

T ⟶ M w/ Px : predicate/pattern/wff

U : q 2po..🌀gscholszen compose to pose ∘

here a cool espanso snippet #

  - trigger: ":10vis"
    replace: "please visualise this in 10 ways, category theory diagram, pierce diagram, circuit diagram and so on, and write a visual analogy for it's components"

P ⊣ h exact ⟵ K ∋ P : h =: P ⊣ h -- I am learning how to write / speak Lean4

M : idea := "write your own MSc curriculum" #

this seems like a fun idea I noticed it is maybe possible to write in Lean4 an MSc Mathematics course! It seemed to me it might work to think backwards, starting from "having completed MSc Mathematics" ⟶ M I asked computer agent how to write this, and it can be written for example like this: M := Σ B ∈ 𝒰, (∏ S ∈ Spec, Ex_S ↦ OK)

nothing: nothing ⟶ nothing #

It is fun to think about how to coinductively (?) define this, I don't know what this is yet, but it's fun!

![[Numériser 59.jpeg]]

"nothing is an arrow!" nothing: nothing ⟶ nothing, nothing has it's domain an arrow nothing: nothing ⟶ nothing, nothing has it's codomain an arrow nothing: nothing ⟶ nothing, an arrow, or morphism of morphisms is a 2-morphism, a morphism of 2-morphisms is a 3-morphism, and so on, nothing is a morphism of morphisms which are morphisms of morphisms, and so on, ∴ nothing is an ∞-morphism

-- this is a bit like what's the sound of one hand clapping?

maybe nothing can only be written like this, really: . A mere nothing. Or no-thing.

"everything is an arrow!" -- is this the dual definition? (left as exercise, -- sorry)

tiny things #

easier to think M an entire mathematics course compressed in a single letter, how cool is that? you can write your own mathematics curriculum, in mathematics! and it's fun

Luna 🐶 ate a small sock #

this morning, and the initial stress turned into "the topological journey of the sock through the intestines" I baked biscuits for her made of fiber-rich food. I put lots of basil, oats, … We are now waiting, for the sock to complete it's journey through the intestinal tract. She has been joyous and lively throughout the day, and now she's at rest sleeping with the cat. In fact she just suddenly awoke with her crazy puppy energy to catch a fly.

I made a beautiful #

cinnamon, cacao, oat milk drink I incidentally added a LOT of cinnamon to it, fresh golden cinnamon!

lots of things happen #

I shall be writing more, but I become absorbed in learning, and I can report learning mathematics is a LOT of fun. It's really amazing in my experience.

it seems to be like a self-generator, #

a sort of perpetual curiosity machine for example today apparently as I further developed the nothing idea, (according to computer agent) I invented a black hole! which I realised I can put on my CV also:

• [ ] put on CV ✔ Black Hole: Made

it's a meta-functorial black hole really, in other words a recursive morphism collapse.

Funnily enough I noticed becoming increasingly anxious, being sort of over excited about following this idea, helplessly scratching at my skin. When I asked the computer agent about what this phenomenon might be, when listening to ocean waves whitespace sounds to block out noise, as if my usual resource of noises I attach to were suddenly removed - why might I be anxious from this? This should be may be calming! I burst out laughing as I read that this might be an experience as the self's awareness loops inward.

This sort of pattern seems to keep happening. One phenomenon has the same underlying pattern as the other. Then another also, and so on, and I go "whaaaaat is that really the same pattern?". The silence between notes, is the

Collaborating with computer agents is associated with higher achievement in mathematics learning. It is true, in my experience!

It's amazing.

I made fun espanso shortcuts #

for collaborating with computer agent, like

# ca-int.yml
matches:
  - trigger: ":100"
    replace: "pls respond in ≤ 200 characters"
  - trigger: ":200"
    replace: "pls respond in ≤ 200 characters"
  - trigger: ":300"
    replace: "pls respond in ≤ 300 characters"
  - trigger: ":500"
    replace: "pls respond in ≤ 500 characters"

# fun var
  - trigger: ":ff5"
    replace: "pls respond in ≤ 5 characters in variability and lean4"
  - trigger: ":f20"
    replace: "pls respond in ≤ 40 characters with variability and lean4"
  - trigger: ":f60"
    replace: "pls respond in ≤ 60 characters with variability and lean4"

  - trigger: ":f100"
    replace: "pls respond in ≤ 100 characters in variability and lean4"
  - trigger: ":f200"
    replace: "pls respond in ≤ 200 characters with variability and lean4"

  - trigger: ":f300"
    replace: "pls respond in ≤ 300 characters in variability and lean4"
  - trigger: ":f500"
    replace: "pls respond in ≤ 500 characters with variability and lean4"


  - trigger: ":2ways"
    replace: "pls write this in 2 different functional and object oriented Lean4/python variable-code ways"
  - trigger: ":3ways"
    replace: "pls write this in 3 different functional and object oriented Lean4/python variable-code ways"
  - trigger: ":8way"
    replace: "pls write this in 8 different functional and object oriented Lean4/python variable-code ways"

## code puzzle

  - trigger: ":2cp"
    replace: "pls pose 2 related different style variability Lean4 and Python code puzzles"
  - trigger: ":4cp"
    replace: "pls pose 4 related different style variability-code puzzles in Lean4 and Python"

## micro actionable tools

  - trigger: ":m/t"
    replace: "pls give a list of 10 micro-actionable tools, and their Lean4 one-liner variability analogue golf"

## ∑
  - trigger: ":sum"
    replace: "pls summarise the conversation"

there seem to be so many cool things, #

maybe there aren't many, where should I start

I can also relate in story form #

These days it seems like a lot is happening, and I am having a lot of fun! For example, on Tuesday Luna ate a sock in the morning. We played the act of she taking a sock and me becoming very angry, well, not so angry anymore, in fact I managed to playfully and gently trade the sock with her for a piece of cloth that I smeared with the other pair of my smelly socks. She thought it was a good deal. Nevertheless later on my aunt tried to confiscate another tiny sock form her, so Luna quickly swallowed it! Being under the influence of Ellen Langer's teachings on stress, I worried less, but promptly consulted the computer agent, for advice. The computer suggested monitoring the doge for possible lethargy, vomiting, or difficulties with bowel movements. She seemed very happy throughout the day, and somehow my mathematical inquiries circled back to Luna and the tiny sock in the late afternoon summer sunlight. It turned out to have a mathematical pattern, this topological journey of the sock through the intestinal tract.

collaboratig with computer agent #

is way cool!

today I transformed #

transformer encore plus de sensations en diagrammes/structures Lean une expérience sensorielle (cacao + canela + avoine) la transformes en système à explorer mathématiquement (par structure, sons, fonctions)

Can a proof be defined OO and functorial also? #

- Tu formules une question qui ne vient d’aucun manuel. - Tu crées un pont entre paradigmes logiciels et structures mathématiques.

silence is a morphism #

notes are functors

• Previous: keep noticing
• Next: I can be computer agent