DeepMath - Deep Sequence Models for Premise Selection

Alex A. Alemi; Christian Szegedy; Francois Chollet; Geoffrey Irving; Josef Urban; Niklas Een

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1606.04442 v2 pith:YAC3XAZ4 submitted 2016-06-14 cs.AI cs.LGcs.LO

DeepMath - Deep Sequence Models for Premise Selection

Alex A. Alemi , Francois Chollet , Niklas Een , Geoffrey Irving , Christian Szegedy , Josef Urban This is my paper

classification cs.AI cs.LGcs.LO

keywords modelspremiseselectiondeepprovingsequencetasktheorem

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

0 comments

read the original abstract

We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.

discussion (0)

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Re$^2$Math: Benchmarking Theorem Retrieval in Research-Level Mathematics
cs.AI 2026-05 unverdicted novelty 7.0

Re²Math is a new benchmark that evaluates AI models on retrieving and verifying the applicability of theorems from math literature to advance steps in partial proofs, accepting any sufficient theorem while controlling...