Skip to content

Commit d63b4eb

Browse files
hyperpolymathhyperpolymath
committed
chore: resolve accidental conflicts from stash pop
1 parent 0ac1cbe commit d63b4eb

3 files changed

Lines changed: 5135 additions & 2 deletions

File tree

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,3 +193,4 @@ deps/
193193
.cache/
194194
build/
195195
dist/
196+
*.stale-*

‎training_data/stats_UNIFIED.json‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,5 @@
1-
{"source_files_used":{"proof_states_fstar.jsonl":10117,"proof_states_hol_light.jsonl":79300,"proof_states_coqgym.jsonl":111617,"proof_states_why3.jsonl":115600,"proof_states_dafny.jsonl":16680,"proof_states_minlog.jsonl":148,"proof_states_typechecker_ecosystem.jsonl":1972,"proof_states_twelf.jsonl":118,"proof_states_hol4.jsonl":127517,"proof_states_nuprl.jsonl":152,"proof_states_minizinc.jsonl":1590,"proof_states_idris2.jsonl":653,"proof_states_agda.jsonl":50095,"proof_states_coqgym_max.jsonl":15013,"proof_states_metamath.jsonl":70146,"proof_states_mizar.jsonl":77137,"proof_states_isabelle.jsonl":214,"proof_states_pvs.jsonl":2377,"proof_states_smtlib.jsonl":20527,"proof_states_acl2.jsonl":170455,"proof_states_mathlib4_max.jsonl":131770,"proof_states_imandra.jsonl":133,"proof_states_afp.jsonl":105858,"proof_states_2026-03-20.jsonl":108,"proof_states_mathlib4.jsonl":278,"proof_states_tptp.a2ml":0},"total_proofs":702099,"vocabulary_size":141517,"date":"2026-04-20","balanced_per_prover_counts":{"Why3":12000,"Lean":12000,"GLPK":311,"ORTools":310,"Idris2":505,"FStar":6367,"Mizar":12000,"CVC5":6737,"PVS":2189,"QTTTypeChecker":167,"Nuprl":151,"TropicalTypeChecker":474,"Imandra":133,"Alt-Ergo":6732,"Minlog":148,"Metamath":12000,"ChoreographicTypeChecker":111,"SessionTypeChecker":112,"HOL4":12000,"Coq":12000,"EpistemicTypeChecker":12,"SCIP":311,"RefinementTypeChecker":23,"DependentTypeChecker":124,"EchoTypeChecker":11,"KatagoriaVerifier":35,"Isabelle":12000,"Dafny":7551,"Chuffed":311,"ModalTypeChecker":87,"ACL2":12000,"Agda":12000,"Z3":6735,"HOLLight":12000,"TypeLL":499,"MiniZinc":312,"EffectRowTypeChecker":308,"Twelf":118},"unique_theorems":687950,"balanced_cap_per_prover":12000,"per_source_counts_top50":{"CoqGym/coq_projects/bbv/theories/Word.v":518,"CoqGym/coq_projects/math-comp/mathcomp/fingroup/fingroup.v":533,"external_corpora/mathcomp-analysis/reals/constructive_ereal.v":699,"CoqGym/coq_projects/math-comp/mathcomp/character/mxrepresentation.v":518,"hol4/pred_setScript.sml":758,"hol4/integrationScript.sml":602,"acl2/sets.lisp":540,"hol_light/Multivariate_integration.ml":815,"why3/separation_why.why":906,"acl2/MAETT-lemmas2.lisp":633,"hol_light/Multivariate_vectors.ml":1038,"hol4/separationLogicScript.sml":737,"hol_light/Library_ringtheory.ml":1675,"Metamath":53293,"hol4/vars_as_resourceScript.sml":691,"acl2/MAETT-lemmas1.lisp":574,"hol_light/jordan_curve_theorem.ml":1347,"hol_light/Multivariate_paths.ml":977,"hol_light/sets.ml":586,"hol_light/words.ml":737,"CoqGym/coq_projects/math-comp/mathcomp/algebra/ssrnum.v":810,"hol_light/transcendence.ml":966,"hol_light/Multivariate_realanalysis.ml":1291,"acl2/rules3.lisp":1041,"hol4/groupScript.sml":809,"acl2/register-readers-and-writers64.lisp":620,"hol4/wordsScript.sml":626,"hol4/data_to_word_memoryProofScript.sml":571,"hol_light/Multivariate_measure.ml":698,"hol4/rich_listScript.sml":567,"acl2/read-over-write-rules64.lisp":509,"hol_light/Library_grouptheory.ml":1161,"hol_light/Multivariate_topology.ml":2219,"hol4/real_topologyScript.sml":1525,"mathlib4":99164,"hol_light/Multivariate_convex.ml":876,"acl2/basic.lisp":759,"hol4/listScript.sml":534,"hol_light/Multivariate_transcendentals.ml":614,"acl2/read-over-write-rules32.lisp":509,"hol4/holSyntaxExtraScript.sml":601,"hol_light/Multivariate_metric.ml":2336,"SMT-LIB":20202,"why3/sort_why.why":788,"hol4/ringScript.sml":636,"hol_light/tame_list.hl":631,"pvs/prelude.pvs":977,"hol_light/hypermap.hl":540,"CoqGym":13675,"hol4/combinatoricsScript.sml":637},"provers_with_data":38,"total_backends":60,"per_prover_counts":{"Why3":15396,"Lean":99308,"GLPK":311,"ORTools":310,"Idris2":505,"FStar":6367,"Mizar":18858,"CVC5":6737,"PVS":2189,"QTTTypeChecker":167,"Nuprl":151,"TropicalTypeChecker":474,"Imandra":133,"Alt-Ergo":6732,"Minlog":148,"Metamath":53293,"ChoreographicTypeChecker":111,"SessionTypeChecker":112,"HOL4":90170,"Coq":86361,"EpistemicTypeChecker":12,"SCIP":311,"RefinementTypeChecker":23,"DependentTypeChecker":124,"EchoTypeChecker":11,"KatagoriaVerifier":35,"Isabelle":100319,"Dafny":7551,"Chuffed":311,"ModalTypeChecker":87,"ACL2":118123,"Agda":36931,"Z3":6735,"HOLLight":42456,"TypeLL":499,"MiniZinc":312,"EffectRowTypeChecker":308,"Twelf":118},"balanced_output_file":"proof_states_UNIFIED_BALANCED.jsonl","version":"UNIFIED","coverage_percentage":63.3,"balanced_total_proofs":160884}
1+
<<<<<<< Updated upstream
2+
{"source_files_used":{"proof_states_fstar.jsonl":10117,"proof_states_hol_light.jsonl":79300,"proof_states_coqgym.jsonl":111617,"proof_states_why3.jsonl":115600,"proof_states_dafny.jsonl":16680,"proof_states_minlog.jsonl":148,"proof_states_typechecker_ecosystem.jsonl":1972,"proof_states_twelf.jsonl":118,"proof_states_hol4.jsonl":127517,"proof_states_nuprl.jsonl":152,"proof_states_minizinc.jsonl":1590,"proof_states_idris2.jsonl":653,"proof_states_agda.jsonl":50095,"proof_states_coqgym_max.jsonl":15013,"proof_states_metamath.jsonl":70146,"proof_states_mizar.jsonl":77137,"proof_states_isabelle.jsonl":214,"proof_states_pvs.jsonl":2377,"proof_states_smtlib.jsonl":20527,"proof_states_acl2.jsonl":170455,"proof_states_mathlib4_max.jsonl":131770,"proof_states_imandra.jsonl":133,"proof_states_afp.jsonl":105858,"proof_states_2026-03-20.jsonl":108,"proof_states_mathlib4.jsonl":278,"proof_states_tptp.a2ml":0},"total_proofs":702099,"vocabulary_size":141517,"date":"2026-04-20","balanced_per_prover_counts":{"Why3":12000,"Lean":12000,"GLPK":311,"ORTools":310,"Idris2":505,"FStar":6367,"Mizar":12000,"CVC5":6737,"PVS":2189,"QTTTypeChecker":167,"Nuprl":151,"TropicalTypeChecker":474,"Imandra":133,"Alt-Ergo":6732,"Minlog":148,"Metamath":12000,"ChoreographicTypeChecker":111,"SessionTypeChecker":112,"HOL4":12000,"Coq":12000,"EpistemicTypeChecker":12,"SCIP":311,"RefinementTypeChecker":23,"DependentTypeChecker":124,"EchoTypeChecker":11,"KatagoriaVerifier":35,"Isabelle":12000,"Dafny":7551,"Chuffed":311,"ModalTypeChecker":87,"ACL2":12000,"Agda":12000,"Z3":6735,"HOLLight":12000,"TypeLL":499,"MiniZinc":312,"EffectRowTypeChecker":308,"Twelf":118},"unique_theorems":687950,"balanced_cap_per_prover":12000,"per_source_counts_top50":{"CoqGym/coq_projects/bbv/theories/Word.v":518,"CoqGym/coq_projects/math-comp/mathcomp/fingroup/fingroup.v":533,"external_corpora/mathcomp-analysis/reals/constructive_ereal.v":699,"CoqGym/coq_projects/math-comp/mathcomp/character/mxrepresentation.v":518,"hol4/pred_setScript.sml":758,"hol4/integrationScript.sml":602,"acl2/sets.lisp":540,"hol_light/Multivariate_integration.ml":815,"why3/separation_why.why":906,"acl2/MAETT-lemmas2.lisp":633,"hol_light/Multivariate_vectors.ml":1038,"hol4/separationLogicScript.sml":737,"hol_light/Library_ringtheory.ml":1675,"Metamath":53293,"hol4/vars_as_resourceScript.sml":691,"acl2/MAETT-lemmas1.lisp":574,"hol_light/jordan_curve_theorem.ml":1347,"hol_light/Multivariate_paths.ml":977,"hol_light/sets.ml":586,"hol_light/words.ml":737,"CoqGym/coq_projects/math-comp/mathcomp/algebra/ssrnum.v":810,"hol_light/transcendence.ml":966,"hol_light/Multivariate_realanalysis.ml":1291,"acl2/rules3.lisp":1041,"hol4/groupScript.sml":809,"acl2/register-readers-and-writers64.lisp":620,"hol4/wordsScript.sml":626,"hol4/data_to_word_memoryProofScript.sml":571,"hol_light/Multivariate_measure.ml":698,"hol4/rich_listScript.sml":567,"acl2/read-over-write-rules64.lisp":509,"hol_light/Library_grouptheory.ml":1161,"hol_light/Multivariate_topology.ml":2219,"hol4/real_topologyScript.sml":1525,"mathlib4":99164,"hol_light/Multivariate_convex.ml":876,"acl2/basic.lisp":759,"hol4/listScript.sml":534,"hol_light/Multivariate_transcendentals.ml":614,"acl2/read-over-write-rules32.lisp":509,"hol4/holSyntaxExtraScript.sml":601,"hol_light/Multivariate_metric.ml":2336,"SMT-LIB":20202,"why3/sort_why.why":788,"hol4/ringScript.sml":636,"hol_light/tame_list.hl":631,"pvs/prelude.pvs":977,"hol_light/hypermap.hl":540,"CoqGym":13675,"hol4/combinatoricsScript.sml":637},"provers_with_data":38,"total_backends":60,"per_prover_counts":{"Why3":15396,"Lean":99308,"GLPK":311,"ORTools":310,"Idris2":505,"FStar":6367,"Mizar":18858,"CVC5":6737,"PVS":2189,"QTTTypeChecker":167,"Nuprl":151,"TropicalTypeChecker":474,"Imandra":133,"Alt-Ergo":6732,"Minlog":148,"Metamath":53293,"ChoreographicTypeChecker":111,"SessionTypeChecker":112,"HOL4":90170,"Coq":86361,"EpistemicTypeChecker":12,"SCIP":311,"RefinementTypeChecker":23,"DependentTypeChecker":124,"EchoTypeChecker":11,"KatagoriaVerifier":35,"Isabelle":100319,"Dafny":7551,"Chuffed":311,"ModalTypeChecker":87,"ACL2":118123,"Agda":36931,"Z3":6735,"HOLLight":42456,"TypeLL":499,"MiniZinc":312,"EffectRowTypeChecker":308,"Twelf":118},"balanced_output_file":"proof_states_UNIFIED_BALANCED.jsonl","version":"UNIFIED","coverage_percentage":63.3,"balanced_total_proofs":160884}
3+
=======
4+
{"source_files_used":{"proof_states_fstar.jsonl":10025,"proof_states_hol_light.jsonl":79300,"proof_states_coqgym.jsonl":111617,"proof_states_why3.jsonl":115600,"proof_states_dafny.jsonl":100000,"proof_states_minlog.jsonl":2200,"proof_states_typechecker_ecosystem.jsonl":1972,"proof_states_twelf.jsonl":2200,"proof_states_hol4.jsonl":127517,"proof_states_nuprl.jsonl":2200,"proof_states_minizinc.jsonl":1535,"proof_states_idris2.jsonl":574,"proof_states_agda.jsonl":50095,"proof_states_coqgym_max.jsonl":15013,"proof_states_metamath.jsonl":70146,"proof_states_mizar.jsonl":77075,"proof_states_isabelle.jsonl":25,"proof_states_pvs.jsonl":2377,"proof_states_smtlib.jsonl":20527,"proof_states_acl2.jsonl":170455,"proof_states_mathlib4_max.jsonl":131770,"proof_states_imandra.jsonl":2200,"proof_states_afp.jsonl":105858,"proof_states_2026-03-20.jsonl":108,"proof_states_mathlib4.jsonl":278,"proof_states_tptp.a2ml":78531},"total_proofs":871731,"vocabulary_size":143392,"date":"2026-04-20","balanced_per_prover_counts":{"Why3":12000,"Lean":12000,"GLPK":300,"ORTools":300,"Idris2":426,"FStar":6275,"Vampire":12000,"Mizar":12000,"CVC5":6737,"PVS":2189,"QTTTypeChecker":167,"Nuprl":2200,"Imandra":2200,"TropicalTypeChecker":474,"Alt-Ergo":6732,"Minlog":2200,"Metamath":12000,"ChoreographicTypeChecker":111,"SessionTypeChecker":112,"HOL4":12000,"Coq":12000,"EpistemicTypeChecker":12,"SCIP":300,"RefinementTypeChecker":23,"DependentTypeChecker":124,"EchoTypeChecker":11,"EProver":12000,"KatagoriaVerifier":35,"Isabelle":12000,"Dafny":12000,"SPASS":12000,"Chuffed":300,"ModalTypeChecker":87,"ACL2":12000,"Agda":12000,"Z3":6735,"HOLLight":12000,"TypeLL":499,"EffectRowTypeChecker":308,"MiniZinc":300,"Twelf":2200},"unique_theorems":805368,"balanced_cap_per_prover":12000,"per_source_counts_top50":{"dafny_synthetic/predicates":16668,"TPTP":78531,"external_corpora/mathcomp-analysis/reals/constructive_ereal.v":699,"dafny_synthetic/sets":16682,"hol4/pred_setScript.sml":758,"hol4/integrationScript.sml":602,"hol_light/Multivariate_integration.ml":815,"why3/separation_why.why":906,"acl2/MAETT-lemmas2.lisp":633,"hol_light/Multivariate_vectors.ml":1038,"hol4/separationLogicScript.sml":737,"nuprl_synthetic/scaled":2200,"hol_light/Library_ringtheory.ml":1675,"Metamath":53293,"hol4/vars_as_resourceScript.sml":691,"acl2/MAETT-lemmas1.lisp":574,"hol_light/jordan_curve_theorem.ml":1347,"twelf_synthetic/scaled":2200,"hol_light/Multivariate_paths.ml":977,"hol_light/sets.ml":586,"minlog_synthetic/scaled":2200,"hol_light/words.ml":737,"CoqGym/coq_projects/math-comp/mathcomp/algebra/ssrnum.v":810,"hol_light/transcendence.ml":966,"hol_light/Multivariate_realanalysis.ml":1291,"acl2/rules3.lisp":1041,"dafny_synthetic/arith":16672,"hol4/groupScript.sml":809,"acl2/register-readers-and-writers64.lisp":620,"hol4/wordsScript.sml":626,"hol_light/Multivariate_measure.ml":698,"dafny_synthetic/sequences":16682,"imandra_synthetic/scaled":2200,"hol_light/Library_grouptheory.ml":1161,"hol_light/Multivariate_topology.ml":2219,"hol4/real_topologyScript.sml":1525,"mathlib4":99164,"dafny_synthetic/methods":16672,"hol_light/Multivariate_convex.ml":876,"acl2/basic.lisp":759,"hol_light/Multivariate_transcendentals.ml":614,"hol4/holSyntaxExtraScript.sml":601,"hol_light/Multivariate_metric.ml":2336,"SMT-LIB":20202,"why3/sort_why.why":788,"hol4/ringScript.sml":636,"hol_light/tame_list.hl":631,"pvs/prelude.pvs":977,"CoqGym":13675,"hol4/combinatoricsScript.sml":637},"provers_with_data":41,"total_backends":60,"per_prover_counts":{"Why3":15396,"Lean":99308,"GLPK":300,"ORTools":300,"Idris2":426,"FStar":6275,"Vampire":26177,"Mizar":18796,"CVC5":6737,"PVS":2189,"QTTTypeChecker":167,"Nuprl":2200,"Imandra":2200,"TropicalTypeChecker":474,"Alt-Ergo":6732,"Minlog":2200,"Metamath":53293,"ChoreographicTypeChecker":111,"SessionTypeChecker":112,"HOL4":90170,"Coq":86361,"EpistemicTypeChecker":12,"SCIP":300,"RefinementTypeChecker":23,"DependentTypeChecker":124,"EchoTypeChecker":11,"EProver":26177,"KatagoriaVerifier":35,"Isabelle":100138,"Dafny":90871,"SPASS":26177,"Chuffed":300,"ModalTypeChecker":87,"ACL2":118123,"Agda":36931,"Z3":6735,"HOLLight":42456,"TypeLL":499,"EffectRowTypeChecker":308,"MiniZinc":300,"Twelf":2200},"balanced_output_file":"proof_states_UNIFIED_BALANCED.jsonl","version":"UNIFIED","coverage_percentage":68.3,"balanced_total_proofs":209357}
5+
>>>>>>> Stashed changes

0 commit comments

Comments
 (0)