feat: migrate all 26 corpus extraction scripts from Python to Julia

Converted extract_acl2, extract_coqgym, extract_dafny, extract_fstar,
extract_hol4, extract_hol_light, extract_idris2, extract_mathlib4,
extract_metamath, extract_minizinc, extract_mizar, extract_pvs,
extract_smtlib, extract_tptp, extract_why3, balance_corpus,
final_complete_merge, final_normalization, generate_synthetic_provers,
max_extract_coqgym, max_extract_mathlib4, merge_corpus, metamath_final,
ultimate_expansion, vocabulary_expansion, vocabulary_final.

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

Author: hyperpolymath

scripts/balance_corpus.jl

@@ -0,0 +1,295 @@
+#!/usr/bin/env julia
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-FileCopyrightText: 2026 ECHIDNA Project Team
+#
+# Balanced corpus extraction - ensure minimum proofs from each prover.
+# Target: at least 12 proofs from every prover system. Extracts additional
+# proofs from CoqGym and adds placeholder examples for under-represented provers.
+
+using JSON3
+
+# Configuration
+const OUTPUT_DIR = "training_data"
+const TARGET_PER_PROVER = 12
+
+# Provers we want to balance
+const TARGET_PROVERS = [
+    "Coq", "Isabelle", "PVS", "HOL4", "ACL2", "Agda", "Z3", "CVC5",
+    "Mizar", "Lean", "Metamath"
+]
+
+"""
+    extract_additional_proofs() -> Union{Vector{Dict{String,Any}}, Nothing}
+
+Extract additional proofs to balance the corpus. Reads existing data, identifies
+under-represented provers, and adds proofs from external corpora or placeholder
+examples.
+"""
+function extract_additional_proofs()
+    println("BALANCED CORPUS EXTRACTION")
+    println("=" ^ 40)
+    println("Target: $TARGET_PER_PROVER proofs per prover")
+
+    # Load existing data to see what we have
+    existing_proofs = Dict{String,Vector{Dict{String,Any}}}()
+
+    # Check existing files
+    files_to_check = [
+        "proof_states_COMPLETE.jsonl",
+        "proof_states.jsonl",
+        "proof_states_all.jsonl"
+    ]
+
+    for filename in files_to_check
+        filepath = joinpath(OUTPUT_DIR, filename)
+        if isfile(filepath)
+            open(filepath, "r") do f
+                for line in eachline(f)
+                    try
+                        proof = JSON3.read(strip(line), Dict{String,Any})
+                        prover = get(proof, "prover", "unknown")
+                        if !haskey(existing_proofs, prover)
+                            existing_proofs[prover] = Dict{String,Any}[]
+                        end
+                        push!(existing_proofs[prover], proof)
+                    catch
+                        continue
+                    end
+                end
+            end
+        end
+    end
+
+    # Count what we have
+    current_counts = Dict(prover => length(proofs) for (prover, proofs) in existing_proofs)
+
+    println("\nCurrent Corpus Balance:")
+    for prover in sort(TARGET_PROVERS)
+        count = get(current_counts, prover, 0)
+        status = count >= TARGET_PER_PROVER ? "[OK]" : "[!!]"
+        println("  $status $(rpad(prover, 12)): $(lpad(string(count), 6)) proofs")
+    end
+
+    # Identify which provers need more proofs
+    deficient_provers = [p for p in TARGET_PROVERS if get(current_counts, p, 0) < TARGET_PER_PROVER]
+
+    if isempty(deficient_provers)
+        println("\nAll provers already have sufficient proofs!")
+        return nothing
+    end
+
+    println("\nNeed more proofs for: $(join(deficient_provers, ", "))")
+
+    # Try to extract more from existing corpora
+    new_proofs = Dict{String,Any}[]
+
+    # 1. Check if we have CoqGym data that wasn't fully extracted
+    coqgym_files = [
+        "external_corpora/CoqGym/coq_projects/Categories/Adjunction/Adj_Cat.v",
+        "external_corpora/CoqGym/coq_projects/Categories/Cat/Terminal.v",
+        "external_corpora/CoqGym/coq_projects/Algebra/GroupDef.v"
+    ]
+
+    for filepath in coqgym_files
+        if isfile(filepath)
+            println("\nExtracting from $filepath...")
+            try
+                content = read(filepath, String)
+
+                # Extract theorems
+                theorem_pattern = r"Theorem\s+([a-zA-Z0-9_]+)\s*:\s*(.*?)(?=\n\s*Proof\.)"s
+                for m in eachmatch(theorem_pattern, content)
+                    try
+                        name = strip(m.captures[1])
+                        statement = strip(m.captures[2])
+
+                        if !isempty(name) && !isempty(statement)
+                            proof = Dict{String,Any}(
+                                "id" => 100000 + length(new_proofs),
+                                "prover" => "Coq",
+                                "theorem" => name,
+                                "goal" => first(statement, 500),
+                                "context" => Any[],
+                                "source" => "CoqGym_balanced"
+                            )
+                            push!(new_proofs, proof)
+                            if length(new_proofs) >= 50  # Limit for now
+                                break
+                            end
+                        end
+                    catch
+                        continue
+                    end
+                end
+            catch e
+                println("  Error: $e")
+            end
+        end
+    end
+
+    # 2. Check Isabelle examples
+    isabelle_examples = [
+        ("HOL", "If P then Q implies not P implies not Q"),
+        ("ZF", "Set theory basics"),
+        ("Algebra", "Group theory examples")
+    ]
+
+    for (i, (domain, desc)) in enumerate(isabelle_examples)
+        if count(p -> p["prover"] == "Isabelle", new_proofs) < 3
+            proof = Dict{String,Any}(
+                "id" => 200000 + i - 1,
+                "prover" => "Isabelle",
+                "theorem" => "example_$i",
+                "goal" => "Example from $domain: $desc",
+                "context" => Any[],
+                "source" => "balanced_corpus"
+            )
+            push!(new_proofs, proof)
+        end
+    end
+
+    # 3. Add PVS examples
+    if count(p -> p["prover"] == "PVS", new_proofs) < 3
+        for i in 0:2
+            proof = Dict{String,Any}(
+                "id" => 300000 + i,
+                "prover" => "PVS",
+                "theorem" => "pvs_example_$(i + 1)",
+                "goal" => "PVS verification example $(i + 1)",
+                "context" => Any[],
+                "source" => "balanced_corpus"
+            )
+            push!(new_proofs, proof)
+        end
+    end
+
+    # 4. Add HOL4 examples
+    if count(p -> p["prover"] == "HOL4", new_proofs) < 3
+        for i in 0:2
+            proof = Dict{String,Any}(
+                "id" => 400000 + i,
+                "prover" => "HOL4",
+                "theorem" => "hol4_example_$(i + 1)",
+                "goal" => "HOL4 theorem example $(i + 1)",
+                "context" => Any[],
+                "source" => "balanced_corpus"
+            )
+            push!(new_proofs, proof)
+        end
+    end
+
+    println("\nExtracted $(length(new_proofs)) additional proofs")
+
+    # Save new proofs
+    if !isempty(new_proofs)
+        output_file = joinpath(OUTPUT_DIR, "proof_states_BALANCED.jsonl")
+        open(output_file, "w") do f
+            for proof in new_proofs
+                println(f, JSON3.write(proof))
+            end
+        end
+
+        println("Saved to $output_file")
+
+        # Update statistics
+        stats = Dict{String,Any}(
+            "version" => "v2.0-balanced",
+            "date" => "2026-03-20",
+            "additional_proofs" => length(new_proofs),
+            "target_provers" => deficient_provers,
+            "achieved_balance" => true
+        )
+
+        open(joinpath(OUTPUT_DIR, "stats_BALANCED.json"), "w") do f
+            JSON3.pretty(f, stats)
+        end
+
+        println("Balance improvement complete!")
+    else
+        println("No additional proofs extracted")
+    end
+
+    return new_proofs
+end
+
+"""
+    merge_balanced_data()
+
+Merge balanced data with the complete corpus, deduplicating by ID.
+"""
+function merge_balanced_data()
+    println("\nMerging balanced data...")
+
+    # Read all proof files
+    files = [
+        "proof_states_COMPLETE.jsonl",
+        "proof_states_BALANCED.jsonl"
+    ]
+
+    all_proofs = Dict{String,Any}[]
+    seen_ids = Set{Int}()
+
+    for filename in files
+        filepath = joinpath(OUTPUT_DIR, filename)
+        if isfile(filepath)
+            open(filepath, "r") do f
+                for line in eachline(f)
+                    try
+                        proof = JSON3.read(strip(line), Dict{String,Any})
+                        pid = get(proof, "id", nothing)
+                        if !isnothing(pid) && !(pid in seen_ids)
+                            push!(all_proofs, proof)
+                            push!(seen_ids, pid)
+                        end
+                    catch
+                        continue
+                    end
+                end
+            end
+        end
+    end
+
+    # Save merged data
+    output_file = joinpath(OUTPUT_DIR, "proof_states_FINAL_BALANCED.jsonl")
+    open(output_file, "w") do f
+        for proof in all_proofs
+            println(f, JSON3.write(proof))
+        end
+    end
+
+    println("Merged data saved to $output_file")
+    println("   Total proofs: $(length(all_proofs))")
+
+    # Check final balance
+    final_counts = Dict{String,Int}()
+    for proof in all_proofs
+        prover = get(proof, "prover", "unknown")
+        final_counts[prover] = get(final_counts, prover, 0) + 1
+    end
+
+    println("\nFinal Balanced Corpus:")
+    for prover in sort(TARGET_PROVERS)
+        count = get(final_counts, prover, 0)
+        status = count >= TARGET_PER_PROVER ? "[OK]" : "[!!]"
+        println("  $status $(rpad(prover, 12)): $(lpad(string(count), 6)) proofs")
+    end
+end
+
+"""
+    main()
+
+Entry point. Extracts additional proofs for balance, then merges with existing data.
+"""
+function main()
+    # Extract additional proofs
+    new_proofs = extract_additional_proofs()
+
+    # Merge with existing data
+    if !isnothing(new_proofs)
+        merge_balanced_data()
+    end
+
+    println("\nBALANCE IMPROVEMENT COMPLETE!")
+end
+
+main()