Claimed results formalized in Lean