Announcing a project: lean-mine

Stream: general

[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

[Yaël Dillies]

Not directly relevant, but similar: Kalle Kytölä, Kin Yau James Wong and I were busy formalising Gibbs Measures and Phase Transitions by Hans-Otto Georgii

[Srivatsa Srinivas]

Interesting! James Wong and I were friends at UCSD

[Yaël Dillies]

Small world :smile: