15 citations · 16 across the 3 of their papers we have counts for
3 papers
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…
MizAR 60 for Mizar 50
Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel +6
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60\% of the Mizar theorems in the hammer setting. We also automatically pr…
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…