Commit 3762a58
committed
feat(corpus): expand synthetic proofs for least-represented provers
Grow the per-prover corpora for the four provers with no public downloadable
training data (tiny communities, small libraries):
Nuprl: 50 -> 152 (+102, +204%)
Minlog: 46 -> 148 (+102, +221%)
Imandra: 47 -> 133 (+86, +183%)
Twelf: 33 -> 118 (+85, +258%)
New categories added to scripts/generate_synthetic_provers.jl:
Nuprl: sets, relations, number_theory, real_analysis, computability,
category_theory, topology, algebra, probability, bishop_analysis,
proof_theory, information, quotient_types, w_types
Minlog: lists, trees, classical_logic, sequent_calculus, induction_advanced,
higher_order, program_verification, modal_logic, intuitionistic,
games, realizers_advanced, bounded_arithmetic, finite_logic
Twelf: binary_trees, substitution, session_types, linear_lf, metatheory,
polymorphism, modules, records, traces, bigstep, hoas, parsing,
automata, effects, numerics
Imandra: trees, numerics, records, state_machines, crypto, blockchain,
algebra, concurrency, databases, networking, security, ml_correctness
Regenerated proof_states_{nuprl,minlog,twelf,imandra}.jsonl match the script.
https://claude.ai/code/session_0173ntsBsELMiXaTWvtjXdN81 parent 9f06c46 commit 3762a58
5 files changed
Lines changed: 1142 additions & 176 deletions
0 commit comments