Een artikel dat op 8 oktober 2026 in Science verscheen, meldt dat AlphaProof Nexus negen van 353 open Erdős-problemen oploste, waaronder twee die al 56 jaar openstonden. Het systeem bewees daarnaast 44 van de 492 open vermoedens uit de Online Encyclopedia of Integer Sequences (OEIS).
Welke resultaten meldt Science?
De resultaten betreffen twee afzonderlijke verzamelingen: open problemen van Erdős en open vermoedens uit de OEIS. De negen opgeloste problemen horen bij de eerste verzameling; de 44 bewezen vermoedens bij de tweede.
Hoe werken bewijsgeneratie en Lean-controle samen?
AlphaProof Nexus genereert met een taalmodel formele bewijsstappen en laat Lean die controleren. Lean is een formele bewijsassistent: de compiler controleert of de stappen binnen het formele bewijs kloppen.
Een eenvoudige agent die het genereren en controleren op die manier afwisselde, reproduceerde eveneens de negen Erdős-resultaten.
