Here the train set was only 1000 proofs (with an average of 90 steps per proof) ... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		nestorD on Sept 9, 2020 \| parent \| context \| favorite \| on: Generative Language Modeling for Automated Theorem... Here the train set was only 1000 proofs (with an average of 90 steps per proof) so it is decidely a small dataset (but highly structured and noiseless).

spolu on Sept 9, 2020 [–]

(30k proofs to be precise, valid and test are each 1k)

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact