Verbose Lean 4
This project provides tactics and commands for Lean in a very controlled natural language. The original version of those tactics were written in French for teaching purposes at Université Paris-Saclay in Orsay using Lean 3. The goal is not to make Lean code easier to write, the goal is to make Lean code easier to transfer to a traditional paper proof.
The best way to have a quick look is to read the examples file in English or French, although GitHub obviously misses proper syntax highlighting here.
There is also a point-and-click interface for courses with a low time budget. One can see it in the following animated gif.
You can read a paper written about this library for ITP2024.
If you want to try it or start writing your exercises using it then you should read getting-started.md. Then you can tweak the behavior of tactics using the basic configuration guide. For information about translating those tactics to your language, see the translation guide.
You can find a very simple example of a library importing Verbose at verbose-lean-demo. You can find a full set of exercises in the proofs with Lean repository. If you are a teacher then you can ask me for the solutions to those exercises. The French version is in the MDD154 repository.
If you simply want to play a bit with the example shown in the picture above
then you can
and use the file explorer to open the file Verbose/English/Examples.lean.
If you use those tactics for teaching, I'd be very interested to hear about it, and would gladly add your name and the name of your university in this file.