Context: after the lean4 fix in leanprover/lean4#13562 routing the [reducible_proj] bump through reduceProj? (so simp, grind canon, cbv, vcgen and unfoldProjInst? all honour the attribute, not just whnfCore's .proj arm), enabling attribute [reducible_proj] Functor.obj in mathlib (commit a8aa749971f on the lean-pr-testing-13562 branch) produces a substantial wave of build failures across Mathlib.CategoryTheory.* and its dependents.

This is a triage / diagnosis writeup. Done in collaboration with Claude Opus 4.7 (1M context) on 2026-05-12.

[reducible_proj] Functor.obj makes Functor.obj <structure-with-unfoldable-body> X reduce one extra step at low transparency. Concretely: when grind canon, simp's whnf, aesop's safe-rule matcher, @[simps]'s elaborator, or simps!'s signature generator processes a goal term containing `

A meta-skill for Claude Code that documents how to write new skills. When invoked, it tells Claude how to structure a new SKILL.md, where to put it, what makes a good trigger description, when to add helper scripts, and how to iterate on skills as you use them.

Drop SKILL.md into ~/.claude/skills/acquiring-skills/:

mkdir -p ~/.claude/skills/acquiring-skills

A skill for Claude Code that converts YouTube talks/seminars into a markdown transcript with the speaker's slides transcribed (LaTeX math intact) and interleaved at the correct timestamps.

Drop all five files into ~/.claude/skills/youtube-to-markdown/ and make the scripts executable:

mkdir -p ~/.claude/skills/youtube-to-markdown

New York Number Theory Seminar, 2026-04-30. YouTube.

Transcript with slides interleaved. Slides reproduced from the speaker's deck; transcript from auto-captions (lightly cleaned).

📊 Slide @ 00:00