Skip to content

Commit 300d35e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
corpus: fold Agda + AFP into merge_corpus, regenerate UNIFIED stats
merge_corpus.jl now ingests proof_states_agda.jsonl and proof_states_afp.jsonl. After dedup the UNIFIED corpus moves from 207,975 → 233,407 unique (prover, theorem) pairs. Prover-share shift (most-imbalanced → balanced): - Lean: 47.42% → 42.56% (−4.9 pp, still top but less dominant) - Isabelle: 0.05% → 8.60% (98 → 20,073, now rank 3) - Agda: 0.0005% → 1.68% (1 → 3,916, now rank 12) vocabulary_UNIFIED.txt is regenerated — it's a raw frequency survey of all proof text and is not the training seed (vocabulary_CANON.txt is). The junk characteristic of raw dumps is therefore expected there and is intentionally excluded from CANON. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent b0cd92f commit 300d35e

3 files changed

Lines changed: 4204 additions & 1 deletion

File tree

‎scripts/merge_corpus.jl‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,8 @@ const PER_PROVER_FILES = [
4444
"proof_states_imandra.jsonl", # Imandra (synthetic)
4545
"proof_states_minizinc.jsonl", # MiniZinc / constraint solvers
4646
"proof_states_isabelle.jsonl", # Isabelle (tropical + theory extraction)
47+
"proof_states_afp.jsonl", # Isabelle AFP (extract_afp.jl, 20K+)
48+
"proof_states_agda.jsonl", # Agda stdlib (extract_agda.jl, 5K+)
4749
"proof_states_tptp.a2ml", # Vampire / EProver / SPASS from TPTP
4850
"proof_states_typechecker_ecosystem.jsonl", # Typechecker/prover expansion
4951
"proof_states_mathlib4.jsonl", # Additional mathlib4 (smaller set)

‎training_data/stats_UNIFIED.json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
{"source_files_used":{"proof_states_fstar.jsonl":76,"proof_states_hol_light.jsonl":7020,"proof_states_coqgym.jsonl":14,"proof_states_why3.jsonl":199,"proof_states_dafny.jsonl":48,"proof_states_minlog.jsonl":46,"proof_states_typechecker_ecosystem.jsonl":1972,"proof_states_twelf.jsonl":33,"proof_states_hol4.jsonl":1899,"proof_states_nuprl.jsonl":50,"proof_states_minizinc.jsonl":29,"proof_states_idris2.jsonl":87,"proof_states_coqgym_max.jsonl":15013,"proof_states_metamath.jsonl":47165,"proof_states_mizar.jsonl":66,"proof_states_isabelle.jsonl":97,"proof_states_pvs.jsonl":231,"proof_states_smtlib.jsonl":20527,"proof_states_acl2.jsonl":277,"proof_states_mathlib4_max.jsonl":131770,"proof_states_imandra.jsonl":47,"proof_states_2026-03-20.jsonl":108,"proof_states_mathlib4.jsonl":455,"proof_states_tptp.a2ml":16843},"total_proofs":209517,"vocabulary_size":79402,"date":"2026-04-17","balanced_per_prover_counts":{"Why3":161,"Lean":12000,"GLPK":5,"ORTools":6,"Idris2":87,"FStar":75,"Vampire":5615,"Mizar":67,"CVC5":6737,"PVS":231,"QTTTypeChecker":167,"Nuprl":50,"TropicalTypeChecker":474,"Imandra":47,"Alt-Ergo":6732,"Minlog":46,"Metamath":12000,"ChoreographicTypeChecker":111,"SessionTypeChecker":112,"HOL4":1899,"Coq":12000,"EpistemicTypeChecker":12,"RefinementTypeChecker":23,"SCIP":6,"DependentTypeChecker":124,"EchoTypeChecker":11,"EProver":5614,"KatagoriaVerifier":35,"Isabelle":98,"Dafny":48,"SPASS":5614,"ModalTypeChecker":87,"Chuffed":6,"TypeLL":499,"EffectRowTypeChecker":308,"Z3":6735,"HOLLight":7000,"ACL2":278,"MiniZinc":6,"Agda":1,"Twelf":33},"unique_theorems":207975,"balanced_cap_per_prover":12000,"per_source_counts_top50":{"hol4/arithmeticScript.sml":396,"typechecker_ecosystem/typell/spec/type-system/qtt.adoc":47,"hol4/realScript.sml":424,"typechecker_ecosystem/typell/spec/type-system/session.adoc":85,"TPTP":16843,"typechecker_ecosystem/typell/spec/type-system/effects.adoc":118,"typechecker_ecosystem/typell/spec/proof/proof-system.adoc":108,"pvs/abs_lems.pvs":34,"hol4/pred_setScript.sml":613,"hol_light/Multivariate_integration.ml":854,"hol_light/Multivariate_vectors.ml":1097,"typechecker_ecosystem/tropical-resource-typing/docs/FORMAL-PROOFS.adoc":27,"typechecker_ecosystem/typell/crates/typell-core/src/effects.rs":31,"typechecker_ecosystem/tropical-resource-typing/Tropical_Kleene.thy":76,"Metamath":47162,"idris2/Nat.idr":28,"typechecker_ecosystem/tropical-resource-typing/Tropical_Matrices_Full.thy":199,"tropical_resource_typing/isabelle_synthetic":25,"pvs/sq.pvs":35,"typechecker_ecosystem/typell/spec/protocol/TYPELL-PROTOCOL.adoc":184,"typechecker_ecosystem/tropical-resource-typing/TropicalSessionTypes.lean":62,"hol4/stringScript.sml":35,"unknown":319,"typechecker_ecosystem/tropical-resource-typing/Tropical_v2.thy":177,"typechecker_ecosystem/katagoria/verification/proofs/coq/TypeSafety.v":26,"why3/euler001.mlw":27,"typechecker_ecosystem/tropical-resource-typing/Tropical_CNO.thy":95,"typechecker_ecosystem/typell/crates/typell-core/src/types.rs":135,"typechecker_ecosystem/typell/spec/type-system/dependent.adoc":159,"hol_light/Multivariate_measure.ml":712,"typechecker_ecosystem/tropical-resource-typing/Tropical_Determinants.thy":49,"acl2/nth.lisp":23,"typechecker_ecosystem/typell/spec/type-system/modal.adoc":64,"typechecker_ecosystem/typell/spec/type-system/linear.adoc":128,"pvs/gcd.pvs":24,"acl2/logops-lemmas.lisp":133,"hol_light/Multivariate_topology.ml":2373,"mathlib4":99117,"typechecker_ecosystem/katagoria/research/tropical/TropicalKleene.idr":28,"typechecker_ecosystem/katagoria/research/tropical/README.adoc":37,"hol_light/Multivariate_convex.ml":898,"hol4/listScript.sml":378,"hol_light/Examples_pell.ml":66,"SMT-LIB":20202,"hol_light/Multivariate_polytope.ml":352,"hol_light/Multivariate_determinants.ml":307,"typechecker_ecosystem/typell/crates/typell-core/src/session.rs":32,"tropical_resource_typing/tropical_v2":27,"CoqGym":13774,"hol_light/Multivariate_derivatives.ml":200},"provers_with_data":41,"total_backends":60,"per_prover_counts":{"Why3":161,"Lean":99347,"GLPK":5,"ORTools":6,"Idris2":87,"FStar":75,"Vampire":5615,"Mizar":67,"CVC5":6737,"PVS":231,"QTTTypeChecker":167,"Nuprl":50,"TropicalTypeChecker":474,"Imandra":47,"Alt-Ergo":6732,"Minlog":46,"Metamath":47162,"ChoreographicTypeChecker":111,"SessionTypeChecker":112,"HOL4":1899,"Coq":13848,"EpistemicTypeChecker":12,"RefinementTypeChecker":23,"SCIP":6,"DependentTypeChecker":124,"EchoTypeChecker":11,"EProver":5614,"KatagoriaVerifier":35,"Isabelle":98,"Dafny":48,"SPASS":5614,"ModalTypeChecker":87,"Chuffed":6,"TypeLL":499,"EffectRowTypeChecker":308,"Z3":6735,"HOLLight":7000,"ACL2":278,"MiniZinc":6,"Agda":1,"Twelf":33},"balanced_output_file":"proof_states_UNIFIED_BALANCED.jsonl","version":"UNIFIED","coverage_percentage":68.3,"balanced_total_proofs":85160}
1+
{"source_files_used":{"proof_states_fstar.jsonl":76,"proof_states_hol_light.jsonl":7020,"proof_states_coqgym.jsonl":14,"proof_states_why3.jsonl":199,"proof_states_dafny.jsonl":48,"proof_states_minlog.jsonl":46,"proof_states_typechecker_ecosystem.jsonl":1972,"proof_states_twelf.jsonl":33,"proof_states_hol4.jsonl":1899,"proof_states_nuprl.jsonl":50,"proof_states_minizinc.jsonl":29,"proof_states_idris2.jsonl":87,"proof_states_agda.jsonl":5529,"proof_states_coqgym_max.jsonl":15013,"proof_states_metamath.jsonl":47165,"proof_states_mizar.jsonl":66,"proof_states_isabelle.jsonl":97,"proof_states_pvs.jsonl":231,"proof_states_smtlib.jsonl":20527,"proof_states_acl2.jsonl":277,"proof_states_mathlib4_max.jsonl":131770,"proof_states_imandra.jsonl":47,"proof_states_afp.jsonl":20486,"proof_states_2026-03-20.jsonl":108,"proof_states_mathlib4.jsonl":455,"proof_states_tptp.a2ml":16843},"total_proofs":233407,"vocabulary_size":83603,"date":"2026-04-17","balanced_per_prover_counts":{"Why3":161,"Lean":12000,"GLPK":5,"ORTools":6,"Idris2":87,"FStar":75,"Vampire":5615,"Mizar":67,"CVC5":6737,"PVS":231,"QTTTypeChecker":167,"Nuprl":50,"TropicalTypeChecker":474,"Imandra":47,"Alt-Ergo":6732,"Minlog":46,"Metamath":12000,"ChoreographicTypeChecker":111,"SessionTypeChecker":112,"HOL4":1899,"Coq":12000,"EpistemicTypeChecker":12,"RefinementTypeChecker":23,"SCIP":6,"DependentTypeChecker":124,"EchoTypeChecker":11,"EProver":5614,"KatagoriaVerifier":35,"Isabelle":12000,"Dafny":48,"SPASS":5614,"ModalTypeChecker":87,"Chuffed":6,"TypeLL":499,"Agda":3916,"Z3":6735,"HOLLight":7000,"EffectRowTypeChecker":308,"ACL2":278,"MiniZinc":6,"Twelf":33},"unique_theorems":231521,"balanced_cap_per_prover":12000,"per_source_counts_top50":{"hol_light/Multivariate_derivatives.ml":200,"hol4/arithmeticScript.sml":396,"typechecker_ecosystem/typell/spec/type-system/qtt.adoc":47,"hol4/realScript.sml":424,"typechecker_ecosystem/typell/spec/type-system/session.adoc":85,"TPTP":16843,"typechecker_ecosystem/typell/spec/type-system/effects.adoc":118,"typechecker_ecosystem/typell/spec/proof/proof-system.adoc":108,"agda-stdlib/src/Data/List/Properties.agda":97,"hol4/pred_setScript.sml":613,"hol_light/Multivariate_integration.ml":854,"agda-stdlib/src/Reflection/AST/Term.agda":43,"hol_light/Multivariate_vectors.ml":1097,"typechecker_ecosystem/tropical-resource-typing/Tropical_Kleene.thy":76,"agda-stdlib/src/Data/Rational/Properties.agda":126,"Metamath":47162,"typechecker_ecosystem/tropical-resource-typing/Tropical_Matrices_Full.thy":199,"agda-stdlib/src/Data/Fin/Properties.agda":128,"typechecker_ecosystem/typell/spec/protocol/TYPELL-PROTOCOL.adoc":184,"typechecker_ecosystem/tropical-resource-typing/TropicalSessionTypes.lean":62,"unknown":319,"typechecker_ecosystem/tropical-resource-typing/Tropical_v2.thy":177,"agda-stdlib/src/Data/Fin/Subset/Properties.agda":52,"agda-stdlib/src/Function/Related/TypeIsomorphisms.agda":42,"agda-stdlib/src/Data/List/Relation/Unary/All/Properties.agda":54,"typechecker_ecosystem/tropical-resource-typing/Tropical_CNO.thy":95,"typechecker_ecosystem/typell/crates/typell-core/src/types.rs":135,"typechecker_ecosystem/typell/spec/type-system/dependent.adoc":159,"hol_light/Multivariate_measure.ml":712,"typechecker_ecosystem/tropical-resource-typing/Tropical_Determinants.thy":49,"agda-stdlib/src/Data/Nat/DivMod.agda":58,"typechecker_ecosystem/typell/spec/type-system/modal.adoc":64,"typechecker_ecosystem/typell/spec/type-system/linear.adoc":128,"acl2/logops-lemmas.lisp":133,"hol_light/Multivariate_topology.ml":2373,"mathlib4":99117,"typechecker_ecosystem/katagoria/research/tropical/README.adoc":37,"hol_light/Multivariate_convex.ml":898,"hol4/listScript.sml":378,"agda-stdlib/src/Data/Vec/Properties.agda":158,"hol_light/Examples_pell.ml":66,"agda-stdlib/src/Data/Bool/Properties.agda":50,"agda-stdlib/src/Data/Rational/Unnormalised/Properties.agda":108,"SMT-LIB":20202,"hol_light/Multivariate_polytope.ml":352,"hol_light/Multivariate_determinants.ml":307,"agda-stdlib/src/Data/Integer/Properties.agda":149,"agda-stdlib/src/Data/Nat/Binary/Properties.agda":103,"CoqGym":13774,"agda-stdlib/src/Data/Nat/Properties.agda":227},"provers_with_data":41,"total_backends":60,"per_prover_counts":{"Why3":161,"Lean":99347,"GLPK":5,"ORTools":6,"Idris2":87,"FStar":75,"Vampire":5615,"Mizar":67,"CVC5":6737,"PVS":231,"QTTTypeChecker":167,"Nuprl":50,"TropicalTypeChecker":474,"Imandra":47,"Alt-Ergo":6732,"Minlog":46,"Metamath":47162,"ChoreographicTypeChecker":111,"SessionTypeChecker":112,"HOL4":1899,"Coq":13848,"EpistemicTypeChecker":12,"RefinementTypeChecker":23,"SCIP":6,"DependentTypeChecker":124,"EchoTypeChecker":11,"EProver":5614,"KatagoriaVerifier":35,"Isabelle":20073,"Dafny":48,"SPASS":5614,"ModalTypeChecker":87,"Chuffed":6,"TypeLL":499,"Agda":3916,"Z3":6735,"HOLLight":7000,"EffectRowTypeChecker":308,"ACL2":278,"MiniZinc":6,"Twelf":33},"balanced_output_file":"proof_states_UNIFIED_BALANCED.jsonl","version":"UNIFIED","coverage_percentage":68.3,"balanced_total_proofs":100977}

0 commit comments

Comments
 (0)