corpus: AFP → 50K, broader Agda extraction, rebalance

- extract_afp.jl: MAX_PER_ARTICLE 25 → 70. AFP corpus grows
  20,486 → 50,137 (post-dedup 48,432), pushing Isabelle to rank 2
  at 18.36% share.
- extract_agda.jl: drop the PROOFY signature gate (was biasing
  toward equational proofs) and walk the whole agda-stdlib tree
  (doc/, dev/, .github/ in addition to src/). Agda grows
  5,529 → 9,312 (post-dedup 5,942). The stdlib source (1,343
  files) caps further growth here — reaching 50K would require
  vendoring additional Agda corpora (cubical, unimath, TypeTopology).

Unified corpus: 233,407 → 263,792. Lean share 42.56% → 37.66%.

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

Author: hyperpolymath

scripts/extract_afp.jl

@@ -42,7 +42,7 @@ const OUTPUT_DIR       = joinpath(REPO_ROOT, "training_data")
 const OUTPUT_FILE      = joinpath(OUTPUT_DIR, "proof_states_afp.jsonl")
 const STATS_FILE       = joinpath(OUTPUT_DIR, "stats_afp.json")
 const START_ID         = 220000
-const MAX_PER_ARTICLE  = 25   # keep the corpus balanced across AFP entries
+const MAX_PER_ARTICLE  = 70   # target ~50K (893 articles, many <70 lemmas)
 
 # Keyword that introduces a theorem-shaped declaration.
 const THM_KW = raw"(?:lemma|theorem|corollary|proposition|schematic_goal)"

scripts/extract_agda.jl

@@ -226,18 +226,21 @@ function parse_file(path::String)::Vector{Dict{String,Any}}
             sig_body = sig_body[1:400] * "…"
         end
 
-        if looks_proofy(sig_body)
-            key = name * "@" * rel
-            if !(key in seen)
-                push!(seen, key)
-                ctx = collect_context(sig_body)
-                push!(out, Dict{String,Any}(
-                    "theorem" => name,
-                    "goal"    => sig_body,
-                    "context" => ctx,
-                    "source"  => "agda-stdlib/" * relpath(path, AGDA_ROOT),
-                ))
-            end
+        # Keep any well-formed top-level signature. The PROOFY gate
+        # biased the extraction toward equational proofs, which left
+        # Agda under 5K records out of 1,182 files. The signatures we
+        # drop otherwise are still useful as training context — they
+        # establish definitions that proof-shaped signatures reference.
+        key = name * "@" * rel
+        if !(key in seen)
+            push!(seen, key)
+            ctx = collect_context(sig_body)
+            push!(out, Dict{String,Any}(
+                "theorem" => name,
+                "goal"    => sig_body,
+                "context" => ctx,
+                "source"  => "agda-stdlib/" * relpath(path, AGDA_ROOT),
+            ))
         end
 
         i = max(j, i + 1)
@@ -279,12 +282,12 @@ function main()
     isdir(AGDA_SRC) || error("Missing $AGDA_SRC — vendor agda-stdlib first.")
 
     files = String[]
-    for (root, _, names) in walkdir(AGDA_SRC)
+    for (root, _, names) in walkdir(AGDA_ROOT)
         for n in names
             endswith(n, ".agda") && push!(files, joinpath(root, n))
         end
     end
-    println("Scanning $(length(files)) .agda files under $AGDA_SRC")
+    println("Scanning $(length(files)) .agda files under $AGDA_ROOT (incl. doc/, dev/, .github/)")
 
     all_records = Dict{String,Any}[]
     parsed_ok = 0