kim-em

LeanEval Lifecycle-Overhaul Implementation Program

Summary

Implement the full lifecycle overhaul through production rollout: immutable v1, problem lifecycle metadata, results schema version 2, append-only state, replay and kernel validation, a Cloudflare submission server, automatic publication, the lifecycle-aware leaderboard, generator extraction, software verification, FC100 integration, and later comparator disproof support.

Terminology: unqualified v1 and v2 refer only to problem sets. This program calls the platform work the lifecycle overhaul, and the resulting system the lifecycle-aware platform. Versioned machine formats are always qualified, for example results schema version 2; frozen identifiers and

kim-em

import Mathlib.Data.Real.Basic
import EvalTools.Markers

/-!
# Quantifier elimination for real closed fields

## The task

Work in the first-order language of ordered rings: `Term`s are built from variables, integer
constants, `+`, `*` and `-`, and `Formula`s are built from the atoms `<` and `=` using `⊥`, `→`

kim-em

import EvalTools.Markers

/-!
# Strong normalization for the calculus of constructions with universes

## The system

`Tm` is the usual lambda syntax with de Bruijn variables: variables, sorts, application,
`lam A b` for `λ (x : A). b`, and `pi A B` for `Π (x : A). B`. The sorts `Srt` are an
impredicative `Prop` together with a predicative hierarchy `Type 0`, `Type 1`, ..., typed by

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