Trail of Bits proves Miden core library arithmetic correct with AI-generated Lean proofs