Announcing a project: lean-mine

Stream: Machine Learning for Theorem Proving

[Srivatsa Srinivas]

Hi all,

I would like to announce a new github organization, lean-mine, the purpose of which will be to collect the formalized proofs of textbook problems along with their natural language explanations. This meant to serve two purposes, help newcomers to Lean (like myself) get better at formalizing proofs, while also creating a data set for machine learning.

I started working on the sub project titled the "baby-rudin-project" link about two days ago and will dedicate about 300-600 hours of my time to it over the course of the next year.

If you have ideas for other textbooks we can work on, or just vague problem dumps (such as formalizing stack exchange elementary number theory) please don't hesitate to let me know!

Best,
Vatsa

[Siddhartha Gadgil]

I parsed the names accidental double meaning and was reminded of Sydney Brenners definition of "data mining"

Data Mining: Your data is mine. My data is also mine.