feat(extract): Phase A push — Lean 3 + Mathcomp toward 100K

Lean 3 (89 907 → 93 737, +3 830):
- Walk lean-liquid + flt-regular alongside mathlib3/src/.
- Still ~ 6K short of 100K — more Lean 3 community libs needed
  (perfectoid-spaces is gone; most Lean 3 projects have migrated
  to mathlib4).

Mathcomp (15 741 → 23 902, +8 161, 1.5×):
- Walk mathcomp + mathcomp-analysis + mathcomp-finmap +
  mathcomp-algebra-tactics + mathcomp-mczify.
- Fix a latent UTF-8 crash: byte-index slice at `content[proof_start:end]`
  crashed on multi-byte glyphs (°, µ, Σ) that mathcomp-analysis
  uses heavily. Now clamps to a valid character boundary via
  `thisind`.
- 24K is well past ML threshold but not 100K — Mathcomp's public
  ecosystem is genuinely smaller than mathlib4's.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

scripts/extract_lean3.jl

@@ -50,25 +50,35 @@ function extract_lean3_proofs()
     premises = Dict{String,Any}[]
     current_id = START_ID
 
+    # Widening (2026-04-18): walk mathlib3 plus additional Lean 3
+    # community libraries (lean-liquid, flt-regular) to push toward
+    # the 100K ML threshold.
+    roots = String[]
     mathlib3_src = joinpath(MATHLIB3_DIR, "src")
-
-    if !isdir(mathlib3_src)
+    isdir(mathlib3_src) && push!(roots, mathlib3_src)
+    for sibling in ("lean-liquid", "flt-regular")
+        p = joinpath(dirname(MATHLIB3_DIR), sibling)
+        isdir(p) && push!(roots, p)
+    end
+    if isempty(roots)
         println("mathlib3 source directory not found: $mathlib3_src")
         println("Clone with: git clone https://github.com/leanprover-community/mathlib " *
                 "$MATHLIB3_DIR")
         return Dict{String,Any}[], Dict{String,Any}[], Dict{String,Any}[]
     end
 
     lean_files = String[]
-    for (root, _dirs, files) in walkdir(mathlib3_src)
-        for file in files
-            if endswith(file, ".lean")
-                push!(lean_files, joinpath(root, file))
+    for root in roots
+        for (rr, _dirs, files) in walkdir(root)
+            for file in files
+                if endswith(file, ".lean")
+                    push!(lean_files, joinpath(rr, file))
+                end
             end
         end
     end
 
-    println("Found $(length(lean_files)) Lean 3 files in mathlib3")
+    println("Found $(length(lean_files)) Lean 3 files across $(length(roots)) root(s)")
 
     # Lean 3 theorem-with-tactic-proof: `theorem NAME STATEMENT := begin … end`
     # Also matches `lemma`, `protected theorem`, etc. The `[^:]*?` eats the

scripts/extract_mathcomp.jl

@@ -91,9 +91,17 @@ function extract_all(base_dir::String)
             kind, name, binders, stmt = tm.captures
             record_id = ID_BASE + length(proof_states)
 
-            # Look for Proof block immediately after the theorem statement
+            # Look for Proof block immediately after the theorem statement.
+            # Use thisind/nextind to keep the slice on a valid UTF-8
+            # character boundary — raw byte indices crash on multi-
+            # byte glyphs (° µ ε Σ etc. appear in mathcomp-analysis).
             proof_start = tm.offset + length(tm.match)
-            rest = content[min(proof_start, lastindex(content)):end]
+            rest = if proof_start > lastindex(content)
+                ""
+            else
+                idx = thisind(content, min(proof_start, lastindex(content)))
+                content[idx:end]
+            end
             pm = try
                 match(PROOF_PAT, rest)
             catch
@@ -180,12 +188,36 @@ function main()::Int
     println("=" ^ 60)
     println("ECHIDNA Mathcomp Extractor")
     println("=" ^ 60)
-    base_dir = "external_corpora/mathcomp"
-    if !isdir(base_dir)
-        println("ERROR: Corpus directory not found: $base_dir")
+    # Widening (2026-04-18): walk the main math-comp repo plus
+    # additional mathcomp-family libraries to push past 20K.
+    candidates = [
+        "external_corpora/mathcomp",
+        "external_corpora/mathcomp-analysis",
+        "external_corpora/mathcomp-finmap",
+        "external_corpora/mathcomp-algebra-tactics",
+        "external_corpora/mathcomp-mczify",
+    ]
+    roots = filter(isdir, candidates)
+    if isempty(roots)
+        println("ERROR: No mathcomp corpus directories found")
         return 1
     end
-    proof_states, tactics, stats = extract_all(base_dir)
+    println("Walking $(length(roots)) mathcomp roots: $(join(basename.(roots), ", "))")
+    base_dir = roots[1]
+    # Override extract_all to scan every root.
+    proof_states = Dict{String,Any}[]
+    tactics = Dict{String,Any}[]
+    stats = Dict{String,Any}()
+    for root in roots
+        ps, ts, st = extract_all(root)
+        append!(proof_states, ps)
+        append!(tactics, ts)
+        stats = st  # keep last
+    end
+    stats["total_proofs"] = length(proof_states)
+    stats["total_tactics"] = length(tactics)
+    stats["id_range"] = isempty(proof_states) ? "none" :
+        "$(ID_BASE)-$(ID_BASE + length(proof_states) - 1)"
     if isempty(proof_states)
         println("\nWARNING: No proof states extracted.")
         return 1