Neuf problèmes d'Erdos d'un coup... Toujours avec la méthode de Deepmind de faire générer des formalisations en lean.
Je n'ai pas lu toutes les preuves mais je m'étonne de la simplicité de certaines : est-ce le signe que ces problèmes ont été peu regardés ou un biais ?
arxiv.org/pdf/2605.22763
