Warrants, dinosaur bones, and resolving conjectures with AI

I've recently been taking part in a conversation on the Lean Zulip about what to do when a conjecture is resolved using AI and a proof assistant (in this case Lean). This is my take and conclusion from the discussion there.