The work treated mathematical discourse as a retrieval problem rather than only an answer-generation problem. Its dataset captures links among conjectures, definitions and supporting propositions in ProofWiki, while accompanying baselines and later graph-based experiments measured how effectively…
Deborah Ferreira and André Freitas introduced the natural-language premise-selection task, in which a system receives a mathematical conjecture expressed through prose and formulae and must retrieve definitions or propositions likely to support a proof, together with a ProofWiki-derived dataset and reproducible extraction pipeline.
The work treated mathematical discourse as a retrieval problem rather than only an answer-generation problem. Its dataset captures links among conjectures, definitions and supporting propositions in ProofWiki, while accompanying baselines and later graph-based experiments measured how effectively models could recover proof-relevant references.
Reference selection is a core bottleneck in both informal and formal mathematical reasoning. By defining a benchmark directly on human-facing mathematical text, this work provided a bridge from earlier formal premise-selection research toward later NaturalProofs-style retrieval and reference-grounded proof generation.
Significance rationale: Natural Language Premise Selection made retrieval of supporting definitions and propositions from ordinary mathematical text an explicit machine-learning task and released a ProofWiki-derived dataset for evaluating it. This supplied an early benchmark for reasoning over mixed prose and formulae before later natural-language theorem-proving datasets and grounded proof-generation systems.
—
—
The arXiv and LREC research records establish the natural-language premise-selection task and the released ProofWiki-derived dataset.
The public nl-ps repository exposes the dataset, extraction pipeline and baseline tooling. E3 records artifact-level inspectability rather than independent validation of every reported retrieval result.
No corrections recorded.
