Lean

Claude впервые формализовал Великую теорему Ферма в Lean. Почему это не «решил», а «записал»

Claude впервые формализовал Великую теорему Ферма в Lean. Почему это не «решил», а «записал» Привет, друзья. У меня немного странные ощущения от этой новости. С одной стороны — да, впервые в истории программа самостоятельно