Emily Riehl

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

Dec 29 at 9:04pmWeb
Show threadPedro AmorimDec 29

@emilyriehl were you able to draw any conclusions from your seminar?

I've been wanting to design something like that before but I've felt somewhat discouraged after reading about how "newbie" students often only brute force their way through Lean goals instead of establishing a mental model of how proofs work.

Show threadEmily RiehlDec 29

@pamorim My actual student audience wasn't quite the optimal audience for this experiment. They were non math majors taking a mandatory pass fail first year seminar. But for the class itself I paired the game levels with pen and paper worksheets. The final project, for instance, asked for a handwritten proof and oral presentation paired with a (partial) formalization. So in short I think the right way to approach this is by mixing modalities (pen and paper, oral communication, game).

In the future, I hope the Lean syntax can be replaced by controlled natural language. Search for "verbose Lean" to see experiments in that direction.

Show threadPedro AmorimDec 29
@emilyriehl thanks for the verbose lean pointer! Looking forward to hearing about your future experiments :)
Show threadpeterbJan 3

@emilyriehl @xenaproject I'm really enjoying the Reintroduction to Proofs game, and have submitted my first PR to it :-D.

Thank you for making it!