Erdos problem #728 was solved more or less autonomously by AI
Barreto and ChatGPT-5.2 have proved that, for any
<...>
This appears to answer the question in the spirit it was intended.
В комментариях задают какие-то разумные вопросы:
How do you verify that the AI translation to Lean is a correct formalization of the problem? In other fields, generative AI is very good at making up plausible sounding lies, so I'm wondering how likely that is for this usage.
Но в целом, все более очевидно, что ИИ придёт за учеными очень быстро.
Непонятно, зачем тратить десять лет на попытки дойти до границы человеческого знания, и потом тратить жизнь на проверку гипотезы, которая не факт, что пройдёт, а публикация -то нужна, поэтому придётся или подменять данные, или топтаться на месте, или ещё что-то, если вместо этого можно делать разные приколюхи с ИИ, а потом разными методами верифицировать ответы.
Конечно, не предлагается просто генерить рандомные тексты и тратить время спецов на проверку просто случайного набора слов, но это уже не то.
Можно сказать, что именно таким и будет учёный — человеком, который сам что-то понимает, чтобы читать такие исследования, но передаю привет всем тем, кто пытается не использовать ИИ вообще, надеется, что он не справится, или что он сам сделает что-то лучше, потому что ИИ может рисовать картинки и болтать ерунду, но нормально думать не сможет. Уже даже общедоступный ChatGPT 5.2 очень и очень умён.