RE: https://mamot.fr/@pluralistic/115819402267996681

A crazy long thread, but well worth the time it takes to read it. It’s a detailed justification of why the world should repeal the ‘anti-circumvention’ laws that US big tech has forced on us.

In a talk called "A reintroduction to proofs"

https://emilyriehl.github.io/files/reintroduction-to-proofs-hardy.pdf

I've speculated about teaching an undergraduate level introduction to proofs course but using dependent type theory as the implicit formal system in place of set theory and first order logic.

This past fall, I taught a first year seminar course at Johns Hopkins along these lines. As part of the course, I developed the Reintroduction to Proofs Game:

https://adam.math.hhu.de/#/g/emilyriehl/reintroductiontoproofs

which is now featured on the Lean Game Server:

https://adam.math.hhu.de/

The game uses Lean tactics to animate the analogy between function types and implications, product types and conjunctions and so on. Following a suggestion made by @xenaproject this past summer, there is a world studying constructions involving the empty type before introducing negations, which allows us to separate out constructive proofs (eg double negation introduction) from classical ones (such as double negation elimination).

The prefix "re" the title imagines more experienced players who might like to learn more about dependent type theory, the Curry Howard correspondence, or constructive mathematics.

This game was made possible by the good folks who built the Lean Game Skeleton repository and answered questions on the Lean for teaching thread on the Lean zulipchat, such as Alex Kontorovich, Aaron Liu, and Dan Velleman . In particular, Jon Eugster saved me several times, when I needed help (or back end fixes) in a rush before my text class.

After the semester ended, I reordered several of the worlds and made various edits and additions. Further contributions are very welcome, especially in the form of PRs to:

https://github.com/emilyriehl/ReintroductionToProofs