Project: Reintroduction to Proofs

Stream: ItaLean 2025

[Lorenzo Luccioli]

This thread is dedicated to the Reintroduction to Proofs project:

• Repository: https://github.com/emilyriehl/ReintroductionToProofs
• Informal & Formal Manager: @Emily Riehl

[Emily Riehl]

If you want to play the game online, you can find it here.

[Emily Riehl]

Note this has been updated and re-organized from the version that appeared on the web yesterday. I'm currently in the process of reorganizing the early levels so that the constructions involving elements of types come before the corresponding constructions involving proofs of propositions. As a result the comments in the left hand columns that accompany each level need some editing. The first two worlds are fairly polished and the third (Implication World) is in decent (but not perfect) shape. I'll polish these up as quickly as I can and push updates frequently.

[Emily Riehl]

In the meanwhile comments or PRs are very welcome.