Как владелец/поддерживающий сайт проблем Эрдёша, я хотел бы поделиться некоторыми комментариями по этому решению задачи #124: 1) Это хорошее доказательство, которое было предоставлено ИИ на основе формального утверждения без участия человека, а затем формализовано в Lean. Это уже впечатляет!