Research
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,742 papers · 148 categories

Trend · papers per month

count% of corpus
0111 · Jun 202319922001200920172026
1 result for “LeanDojo”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscs.LG

LeanDojo removes barriers to theorem proving with open-source tools and data.

problem Difficulty in reproducing and building on existing theorem proving methods.
method Introduces LeanDojo, an open-source Lean playground with toolkits, data, models, and benchmarks.
result ReProver, an LLM-based prover augmented with retrieval, outperforms non-retrieval baselines and GPT-4.
theorem provinglanguage modelsretrievalopen-sourceLeanDojo
2023-06-27abs ↗pdf ↗