kim-em

Review notes: feat(lake): wrapped exec (#13948)

A skeptical review of the $LAKE_WRAPPED_EXEC hook, cross-checked by Claude (Opus 4.8) and OpenAI Codex. Both read the PR branch directly; every concern below was independently confirmed against the code.

Solid

• The Build/Actions.lean refactor is behavior-preserving. mkLeanModuleArgs / mkCcCompileArgs preserve argv order, escapeRspArg is the same escaping factored out, and compileLeanModule keeps the same createParentDirs calls.
• The unset path matches upstream for the spawn itself — runRawProcOrWrapped falls through to rawProc with the same logging.

Concerns

kim-em

#!/usr/bin/env python3
"""
Reproducer for mathlib4 PR #40110 — linarith atomization speedup.

Generates two Lean files (Bench80.lean, Bench160.lean) that each call
`linarith (config := {})` several times on a dense rational LP:
  0 ≤ xᵢ, xᵢ ≤ 1, Σxᵢ ≤ n
with n distinct atoms and 2n bound hypotheses.

Usage

kim-em

import Mathlib
import Submission.Helpers

namespace Submission

theorem two_plus_two_eq_four : (2 : Nat) + 2 = 4 := by
  norm_num

end Submission

kim-em

Diagnosis: downstream failures from [reducible_proj] Functor.obj in mathlib

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.

The underlying mechanism

[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 `

kim-em

Claude Code skill: acquiring-skills

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.

Installation

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

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

kim-em

Claude Code skill: youtube-to-markdown

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.

Installation

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

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

kim-em

Mel Nathanson — How Harmonic's Aristotle solved some of my problems

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

kim-em

import ChallengeDeps

open LeanEval.Analysis.ODE
open Real MeasureTheory

theorem heat_kernel_solves_heat_equation (f : ℝ → ℝ) (hf_cont : Continuous f) (hf_bdd : ∃ M : ℝ, ∀ x, |f x| ≤ M) :
    -- The PDE on (0, ∞) × ℝ.
    (∀ t : ℝ, 0 < t → ∀ x : ℝ, ∃ ux : ℝ → ℝ, ∃ uxx : ℝ,
        (∀ y : ℝ, HasDerivAt (fun z => heatSolution f t z) (ux y) y) ∧
        HasDerivAt ux uxx x ∧

kim-em

import Mathlib
/-!
Minimal example exercising `instance` holes in the multi-hole
eval-problem pipeline. The carrier type is itself a hole so the source
has no non-hole declarations and the generator does not need a
`ChallengeDeps` split.
-/
def WidgetCarrier : Type := sorry
instance instInhabitedWidget : Inhabited WidgetCarrier := sorry

kim-em

import Mathlib

open scoped Real

theorem dirichlet_eigenvalues_eq_nat_sq (lam : ℝ) :
    (∃ (y : ℝ → ℝ) (J : Set ℝ),
        IsOpen J ∧ Set.Icc (0 : ℝ) Real.pi ⊆ J ∧
        (∀ x ∈ J, HasDerivAt y (deriv y x) x) ∧
        (∀ x ∈ J, HasDerivAt (deriv y) (-(lam * y x)) x) ∧
        y 0 = 0 ∧ y Real.pi = 0 ∧