Verifying Move Borrow Checker in Lean:An Experiment in AI-Assisted PL Metatheory