Autograder for logic intro with lean

Stream: Lean for teaching

[Thorsten Altenkirch]

We (@Thorsten Altenkirch and @Cas Widdershoven ) are moving our module on Introduction to formal Reasoning (with 400 students !) to Lean4 (using also verso by @David Thrane Christiansen, hurrah). We were using an autograder written by @Jacob Neumann which was coded in lean3. Now we need to implement a new autograder soon (teaching starts end of September) :-(

Any help and advice or examples of existing autograders which fit our purpose would be very much appreciated. We would like to keep it simple.

Thanks a lot!

P.S. For obvious reasons I do not copy the exercises here but I can provide them on request.

[Michael Rothgang]

@Rob Lewis wrote an autograder for Lean. If you search zulip, perhaps you can find it - or a helpful soul can point it out :-)

[Julian Berman]

That's https://github.com/robertylewis/lean4-autograder-main I believe.

[Kevin Buzzard]

Updated to 4.22.0 two days ago :D