🦄 Lean4 Puzzle, 🐢 C Puzzle, 🐍 Python Puzzle

• 07 August 2025
• Mathematics,
• Process book,
• Learning

🦄 Lean4 Puzzle:

inductive 𝒲 where
| α : 𝒲
| β : 𝒲 → 𝒲

def 𝒮 (ζ : Type) := Unit ⊕ ζ

def φ : 𝒮 𝒲 → 𝒲
| .inl _ => 𝒲.α
| .inr z => 𝒲.β z

#eval φ (.inr (.β (.β 𝒲.α)))

❓Guess: How deep is this number in Peano steps?

🐢 C Puzzle:

typedef struct Ω {
  int tag;
  struct Ω* next;
} Ω;

Ω* Φ(Ω* x) {
  if (!x) return NULL;
  Ω* y = malloc(sizeof(Ω));
  y->tag = 1;
  y->next = x;
  return y;
}

❓Guess: How many Φ calls before NULL?

🐍 Python Puzzle:

def 𝓕(x): return ("1", None) if x is None else ("+", x)

x = 𝓕(("+", ("+", None)))
print(x[1][1])

❓Guess: What does x[1][1] yield?

I find it sort of fun, that this is a number, because it doesn't look like a number:

inductive 𝒲 where
| α : 𝒲
| β : 𝒲 → 𝒲

✨ Keep puzzling! Every function is a tiny theorem you can prove or refactor — functional code is mathematical art. 🎨🐙

𝒮 𝒲 := Unit ⊕ 𝒲  
-- ∅       🐾 something

• Previous: Mini Puzzle - ∀, ∃, normalization challenge
• Next: moments of sheaf - fragments