Commit 8b79af5
feat(corpus): expand synthetic proofs for least-represented provers (#20)
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_0173ntsBsELMiXaTWvtjXdN8
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>1 parent 1211f02 commit 8b79af5
5 files changed
Lines changed: 1142 additions & 8800 deletions
0 commit comments