NaturalProofs: Mathematical Theorem Proving in Natural Language

Formal theorem-proving research has advanced through HOL Light, Coq, Lean, Mizar, Metamath, premise selection, and benchmarks such as HOList. Neural systems can help choose assumptions for automated provers, but formal languages do not capture how most mathematics is written. ProofWiki-based resources began addressing natural mathematical language, yet generally emphasized one source. NaturalProofs extends this direction with broad, deep, and low-resource domains plus explicit out-of-distribution evaluation.

For theorem x and candidate set R, the system must recover the proof-reference sequence y=(r1,…,r|y|). Retrieval reduces y to a set; generation must recover cardinality, order, and repeated references. The problem is difficult because R contains roughly 46,000 unique candidates, mathematical wording varies widely, proofs omit steps, and test theorems must not have appeared as training references. Relevance is therefore finer than topical similarity.

The corpus unifies ProofWiki’s broad coverage, Stacks’ deep algebraic-geometry coverage, and low-resource textbook material. Every page is represented with title, mixed text/LaTeX contents, proofs, and links in a common schema. A reference graph supports leaf-node splitting and leakage control. The task suite covers both unordered retrieval and ordered generation, while Full@k measures whether a small ranked list contains every result needed for a proof.

• �� Data: extract statements, proofs, mixed text/LaTeX, and explicit links, yielding about 25,000 theorem-proof examples and roughly 46,000 candidate references.
• �� Pairwise retrieval: BERT encodes theorem and reference independently; sθ(x,r) is a dot product, trained with positive references and sampled negatives.
• �� Joint retrieval: compute softmax(Rfθ(x)) over all candidates; R may contain representations learned by an independent reference encoder.
• �� Generation: model pθ(rt|r<t,x), decode with beam search, and terminate with EOS.
• �� Evaluation: train/test within ProofWiki or Stacks, then transfer without training examples to the Real Analysis and Number Theory textbooks.

Baselines are Random, Frequency, and TF-IDF. Neural variants are BERT Pairwise and Joint, trained either per source (P/S) or jointly on ProofWiki plus Stacks (P+S). Retrieval uses mAP, micro-averaged R@10/R@100, and Full@10/Full@100. Generation uses exact match, edit distance, BLEU, set F1, and multiset F1. Oracle conditions—randomized full set, randomized multiset, and correct first half—diagnose whether errors arise from membership, multiplicity, or ordering.

On ProofWiki, source-specific Joint BERT reaches mAP 36.75 versus Pairwise 16.82, R@10 42.45, and Full@100 50.22. On Stacks it reaches mAP 28.32, R@10 39.10, and Full@100 65.59. Joint training remains useful but is usually below source-specific training. In zero-shot evaluation, TF-IDF achieves Real Analysis mAP 15.79 versus 11.24 for ProofWiki-trained Joint BERT; this shows that strong in-domain neural ranking does not yet imply robust mathematical transfer.

A practical system could retrieve prerequisite theorems for students, help researchers navigate large proof libraries, or provide candidate premises to Lean, Mizar, or another prover. It can also support semi-automated textbook indexing and proof explanation. Deployment requires structured references, domain adaptation, and human or formal verification, because high topical relevance is not evidence that a result is logically necessary.

Explicit links are an imperfect proxy for proof reasoning and miss implicit premises. BERT representations remain weak at variable renaming, equivalent equations, symbolic manipulation, and long-range proof structure. Joint scoring over tens of thousands of candidates can be computationally expensive, while autoregressive generation suffers exposure bias and error accumulation. The low zero-shot and exact-generation scores motivate graph-aware, symbol-aware, retrieval-generation models coupled to formal proof checking.