Validation of top 50 HF models#2299

Open

noahgift wants to merge 63 commits into

mainfrom

auto-validate-top50-retry-1783266323

Commits on Jul 4, 2026

feat(contracts): climb matmul-kernel-v1 to honest L4 — 3 Lean-proved + 2 N/A of 5

noahgift
and
claude
committed
feat(contracts): climb apr-cli-sampling-v1 to L4 — 3 analytic sampling proofs in verified Lean

noahgift
and
claude
committed
proof(embedding-lookup): climb to L4 — 11 sorry-free Lean gather theorems (PILLAR-2/4)

noahgift
and
claude
committed
feat(batchnorm-kernel-v1): climb to L4 — 4 analytic obligations proved in verified Lean 4

noahgift
and
claude
committed
feat(silu-kernel-v1): climb to honest L4 — 6 Lean-proved analytic obligations

noahgift
and
claude
committed
proof(contracts): gelu-kernel-v1 — prove non-negativity + positive monotonicity in verified Lean (honest L3)

noahgift
and
claude
committed
feat(conv1d-kernel-v1): climb L3→L4 — Lean-prove linearity, output-shape, output-bound

noahgift
and
claude
committed
Merge remote-tracking branch 'origin/climb3/matmul-kernel-v1' into feat/corpus-climb-wave-3
noahgift
committed
Merge remote-tracking branch 'origin/climb3/silu-kernel-analytic' into feat/corpus-climb-wave-3
noahgift
committed
Merge remote-tracking branch 'origin/climb3/gelu-kernel-v1' into feat/corpus-climb-wave-3
noahgift
committed
Merge remote-tracking branch 'origin/climb3/batchnorm-kernel-analytic' into feat/corpus-climb-wave-3
noahgift
committed
Merge remote-tracking branch 'origin/climb3/conv1d-kernel-lean' into feat/corpus-climb-wave-3
noahgift
committed
Merge remote-tracking branch 'origin/climb3/embedding-lookup-v1' into feat/corpus-climb-wave-3
noahgift
committed
Merge remote-tracking branch 'origin/climb3/apr-cli-sampling-v1' into feat/corpus-climb-wave-3
noahgift
committed
proof(contracts): corpus climb wave 3 — 6 more kernels → L4 (matmul core algebra, verified Lean)

noahgift
and
claude
committed
proof(rope-kernel-v1): L3→L4 — Lean proofs of RoPE norm/relative-position/length/bound

noahgift
and
claude
committed
feat(cma-es-kernel-v1): climb L3→L4 — prove 4 analytic obligations in verified Lean

noahgift
and
claude
committed
feat(gqa-kernel-v1): climb to L4 — 6 analytic obligations proved in verified Lean

noahgift
and
claude
committed
proof(alibi-kernel-v1): L3→L4 — 4/5 obligations proved in verified Lean 4

noahgift
and
claude
committed
feat(contracts): embedding-algebra-v1 analytic Lean proofs (5/7 obligations, honest L3)

noahgift
and
claude
committed

Commits on Jul 5, 2026