diff --git a/images/minif2f.jpg b/images/minif2f.jpg new file mode 100644 index 0000000..a140d59 Binary files /dev/null and b/images/minif2f.jpg differ diff --git a/images/proofnet.jpg b/images/proofnet.jpg new file mode 100644 index 0000000..b7a9f77 Binary files /dev/null and b/images/proofnet.jpg differ diff --git a/images/proofnet_retrieval.jpg b/images/proofnet_retrieval.jpg new file mode 100644 index 0000000..b50c0b4 Binary files /dev/null and b/images/proofnet_retrieval.jpg differ diff --git a/index.html b/index.html index 65c02cf..035311d 100644 --- a/index.html +++ b/index.html @@ -392,6 +392,18 @@

Experiments

Discovering New Proofs and Uncovering Formalization Bugs

We evaluate ReProver on theorems in miniF2F and ProofNet. It discovers 33 proofs in miniF2F and 39 proofs in ProofNet of theorems that did not have Lean proofs. Our proofs have helped ProofNet uncover multiple bugs in the formalization of theorem statements.

+ + +
+ Example new proofs discovered on miniF2F. + + +
+ Example new proofs discovered on ProofNet. + + +
+ Three new proofs discovered on ProofNet that cannot be found without premise retrieval.