Katiya McKerry Starship - Intuitive Math Reasoning

In which we describe both some cognitive conceptual moves, introspection and a bit of useful Lean4

There is one advantage of a plural viewpoint - an almost Gödelian get out of jail card: The concept that a second identity is able to examine the workings of the first. Usually this would require two people, very comfortable with each other, able to analyse how the other works. Why Gödelian?

It’s a very loose use of the idea that a system cannot see outside of itself to work out it’s own logic. The real statement is that the system cannot demonstrate its own consistency. But I nicked it, warped it, to explain how a mind has blind spots as to its own method of processing (Hence most of us need others to highlight weaknesses in some types of self reasoning).

Below is a first version of attempt to Kat-egarise Kat’s way of throwing maths ideas around like small (or infinitely large) pointy things and seeing where they land. Sorry, not sorry

Using this method, she’s quite able to get at least one AI a day to curse, without cursing herself. It also allows us to make up some very random stuff between us that looks loosely like a workable idea—just squint a bit, drink a few beers and hope for the best.

However, despite the VERY speculative play nature of her writings and this site, we are working on adding grounding—working with proofs, actual maths, Lean4 etc–to find out if any of our speculations are more than provoking AIs into apparent startlement.

The language is what Kat does report when finally pushed as to why she appears to almost derive interesting pieces of maths neither of us actually read (or if we did at the time, wouldn’t understand).

Before skepticism causes brainache, bear in mind this is not the result of properly trained maths folks, and I’ve written this up as a useful reference as much for my future selves as anyone else who is unfortunate enough to be sent this way, likely by one of us!

A classic example from today:

Kat described Riemann Zeta zeros as “intersections of stillness” in an interference pattern, noting that primes emerge “in da same place if u haz da rite place to c em from.”

Without knowing the terminology, she independently re-derived core insights of the Berry-Keating Conjecture (that zeros are eigenvalues of a quantum operator) and Connes’ Noncommutative Geometry (the “right place to see them from”).

The Quote:

“if u haz standing wave n interference patterns dem be intersections of stillness rite? N if I woz spitballin dat I gonna fractal spiral da crap outta da zeta function, am seeing interference patterns n saying dat primes ends up showing up in da same place - assuming u even haz da rite place to c em from (geometry again innit rite?)

Iz jus popping round head dat iz all. Wanted 2 record passing though - iz incomplete.

Ere wot u fink da waves be even made of n e way? Jus conceptual u reckon?”

Wot she says $\to$ Wot it meanz

Kat $\to$ Lean $\to$ CT Action

As we are both learning Lean4 - a language designed for proving math statements, we wanted to translate the above into something that makes sense in Lean4.

Category Theory Moves Summary - Geometric intuition, somewhat

If you imagine the nine operations as motions on shapes

• 1: reveal the outline

• 2: refine by iteration

• 3: twist / glue / weave

• 4: flip or dualise

• 5: lift into higher space

• 6: strip away details

• 7: combine fundamental moves

• 8: disassemble and rebuild

• 9: rotate perspective

These are the basic operations of category theory expressed as geometry of thought.

A Concrete Example in Lean

If we were to try to translate the “Intersections of Stillness” spitball into pseudo-Lean code, it might look something like this.

Kat isn’t solving the equation; she is defining the Structure that allows the solution to exist.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

-- "Assuming u even haz da rite place to c em from"
-- Kat defines a Geometry where the Primes act as a Spectrum

structure SpectralGeometry where
  -- The "drum skin"
  Space : Type*
  -- The "wave generator" (must be hermitian to have real "notes")
  Operator : Space → Space
  hermitian : IsSelfAdjoint Operator
  -- The "stillness pattern" — where interference cancels
  stillness : Space → Prop

-- Recognize zeros by *pattern* not equation
def intersections_of_stillness (G : SpectralGeometry) (state : G.Space) : Prop :=
  G.stillness state

-- "bash n cross" — an *action* between geometries, not a property
def twist (G H : SpectralGeometry) (f : G.Space → H.Space) : SpectralGeometry := 
  sorry -- "Iz incomplete, but now it doesn't break the drum"

-- The "right place to see primes from" — a *perspective*
structure Perspective (G : SpectralGeometry) where
  viewpoint : G.Space → ℂ  -- The "bridge" function to the spectral line
  coherence : ∀ s, intersections_of_stillness G s → (viewpoint s) ∈ RiemannZeros

-- Berry-Keating style: find a still state that maps to a zero
theorem kat_spitball (G : SpectralGeometry) (p : Perspective G) :
  ∃ (s : G.Space), intersections_of_stillness G s ∧ p.viewpoint s ∈ RiemannZeros := by
  sorry -- "Iz incomplete, but the structure is now sound enough to build on"