AIPS

Stream: Machine Learning for Theorem Proving

[Sid]

https://arxiv.org/abs/2406.14219v1 - inequality prover trained entirely on synthetic data. Gets 10/20 on IMO inequality problems

[llllvvuu]

.pkl is a bit of an insane format for releasing the dataset, so I've re-uploaded to https://huggingface.co/datasets/llllvvuu/AIPS_inequalities and added some documentation. I've contacted the authors and they are OK with this.

[Zheng Yuan]

llllvvuu said:

.pkl is a bit of an insane format for releasing the dataset, so I've re-uploaded to https://huggingface.co/datasets/llllvvuu/AIPS_inequalities and added some documentation. I've also contacted the authors to ask what they want to do (I can take it down, transfer ownership, or change license)

very happy to see a script to translate into lean4

[Andy Jiang]

What's the estimate on the amount of compute they used? I heard the Olympiad geometry one was sort of on the level that can (and has?) be replicated by hobbyists. Do we know if it plateaued at the end of training?