On-device research index

arXiv research

A locally-built, LLM-digested index of recent arXiv papers in quant finance, geometry/topology, and statistical ML — keyword search served straight from SQLite on this machine.

168,657 papers · 148 categories

Trend · papers per month

count % of corpus

2 results for “Metamath”

Generative Language Modeling for Automated Theorem Provingcs.LG

GPT-f uses language models to find new proofs in formal math.

problem Generating original mathematical terms for automated theorem proving.

method Transformer-based language model for automated theorem proving and proof assistant.

result GPT-f contributed new proofs to the Metamath library.

automated theorem proving language models deep learning formal mathematics Metamath

2020-09-07abs ↗pdf ↗

Learning to Prove Theorems by Learning to Generate Theoremscs.LO

We consider the task of automated theorem proving, a key AI task. Deep learning has shown promise for training theorem provers, but there are limited human-written theorems and proofs available for supervised learning. To address this limitation, we propose to learn a neural generator that automatically synthesizes the…

2020-02-17abs ↗pdf ↗