LEAPing into the Future of Coding

A few months ago in Oxford, Bernard Sufrin, an emeritus fellow, said he's looking to hire a student to implement LEAP (Logic Engine for Argument by Pointing), a way to teach logic by proving basic logic theorems via pointing and clicking. Rahul Santhanam said why not give it to AI. Bernard said AI can't handle this task. I thought why not give it a try.I gave Claude a single prompt that Bernard helped me formulate:Architecture of a system to support proof by pointing in first order logic using LEAPAbout an hour later, without giving additional details, we had a working prototype. Give it a try. I put the code and some more details on GitHub.Watching Claude work was amazing. Claude created an architecture based on the paper Proof by Pointing by Yves Bertot, Gilles Kahn and Laurent Théry.Claude then asked me:Would you like me to proceed with implementing any of these layers?Why not? So I told Claude to go ahead.It started coding and it created 78 test cases and kept debugging itself…