ИИ-агент Google DeepMind решил 9 задач Эрдёша с помощью нескольких моделей и Lean

Google DeepMind показала систему AlphaProof Nexus, которая ищет формальные доказательства математических утверждений и проверяет их в языке Lean. В тестах на открытых задачах агент решил 9 из 353 задач, связанных с Эрдёшем, а также 44 из 492 гипотез OEIS.

Система работает через строгую машинную проверку: если в доказательстве есть ошибка, поиск продолжается. При этом успехи пока заметны в областях с уже развитой библиотекой формализованных результатов.

@forgeeks | @forgeeksflash