ИИ-математики снова взбудоражили ленту, и на этот раз всё выглядит почти как прорыв
ИИ-математики снова взбудоражили ленту, и на этот раз всё выглядит почти как прорыв. Почти. Стартап Harmonic выкатил новость: их система Aristotle якобы решила одну из задач из списка Эрдёша — №124. Это не какая-то скучная теоремка, а проблема, которая с конца 90-х висела нерешённой — впервые сформулированная в Acta Arithmetica. Человеческая математика — 30 лет. Aristotle — 6 часов. Без участия людей. Красиво. Что вообще делает Aristotle? Это не «пишу вам текст про математику, как ChatGPT». Он работает в среде Lean — формальной системе доказательств...