Title says formalizing, article amounts to "we asked claude to check one result with lean, got bad results, then we told it to make no mistakes".