Theorem Proving on set.mm (test)
600Proofs Found (Test)HOLOPHRASM + MetaGen-IL
Evaluation Results
| Method | Links | |
|---|---|---|
| HOLOPHRASM + MetaGen-ILHuman proofs=21786 (100%), Synthetic proofs=10M, Generator=MetaGen-IL, Prover=HOLOPHRASM, remove_trivial_proof_steps=true2020.02 | 600 | |
| HOLOPHRASM + MetaGen-IL (No Trivial Filter)Human proofs=21786 (100%), Synthetic proofs=10M, Generator=MetaGen-IL, Prover=HOLOPHRASM, remove_trivial_proof_steps=false2020.02 | 574 | |
| HOLOPHRASM + MetaGen-RandHuman proofs=21786 (100%), Synthetic proofs=10M, Generator=MetaGen-Rand, Prover=HOLOPHRASM2020.02 | 565 | |
| HOLOPHRASMHuman proofs=21786 (100%), Synthetic proofs=0, Generator=None, Prover=HOLOPHRASM2020.02 | 557 | |
| HOLOPHRASMHuman proofs=4358 (20%), Synthetic proofs=0, Generator=None, Prover=HOLOPHRASM2020.02 | 476 | |
| HOLOPHRASM + MetaGen-ILHuman proofs=2179 (10%), Synthetic proofs=1M, Generator=MetaGen-IL, Prover=HOLOPHRASM2020.02 | 472 | |
| HOLOPHRASM + MetaGen-RandHuman proofs=2179 (10%), Synthetic proofs=1M, Generator=MetaGen-Rand, Prover=HOLOPHRASM2020.02 | 457 | |
| HOLOPHRASMHuman proofs=2179 (10%), Synthetic proofs=0, Generator=None, Prover=HOLOPHRASM2020.02 | 454 | |
| HOLOPHRASM('16)Human proofs=21786 (100%), Synthetic proofs=0, Generator=None, Prover=HOLOPHRASM('16)2020.02 | 388 | |
| HOLOPHRASM + MetaGen-RL-AdvHuman proofs=0, Synthetic proofs=300K, Generator=MetaGen-RL-Adv, Prover=HOLOPHRASM2020.02 | 357 | |
| HOLOPHRASM + MetaGen-RL-LMHuman proofs=0, Synthetic proofs=300K, Generator=MetaGen-RL-LM, Prover=HOLOPHRASM2020.02 | 351 | |
| HOLOPHRASM + MetaGen-RandHuman proofs=0, Synthetic proofs=300K, Generator=MetaGen-Rand, Prover=HOLOPHRASM2020.02 | 346 | |
| TF-IDF & LMHuman proofs=0, Synthetic proofs=0, Generator=None, Prover=TF-IDF & LM2020.02 | 312 | |
| HOLOPHRASMHuman proofs=0, Synthetic proofs=0, Generator=None, Prover=HOLOPHRASM2020.02 | 219 |