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.
This Lean 4 version is not yet well tested since it has not been used a lot for teaching yet. It is currently used in Strasbourg. 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.
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.
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.