15 citations · 23 across the 4 of their papers we have counts for
Showing 2023Show all
2 papers · 1 filter
cs.AI2023★ 1 cited
Machine-Learned Premise Selection for Lean
Bartosz Piotrowski, Ramon Fernández Mir, Edward Ayers
We introduce a machine-learning-based tool for the Lean proof assistant that suggests relevant premises for theorems being proved by a user. The design principles for the tool are…
cs.CL2023★ 15 cited
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf +3
We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of…