Auf dem ArXiv ist am 4. April ein Preprint mit einem Gegenbeispiel zu der Anderson-Vermutung aus der Theorie lokaler Ringe erschienen: https://arxiv.org/html/2604.03789v1
Screenshot
Bemerkenswert an diesem Gegenbeispiel ist, dass es nicht von einem Menschen gefunden wurde, sondern von einer Maschine.
Our framework consists of two components: an informal reasoning agent, Rethlas, and a formal verification agent, Archon. Rethlas mimics the workflow of human mathematicians by combining reasoning primitives with our mathematical theorem search engine, Matlas, to explore solution strategies and construct candidate proofs. Archon, equipped with our formal theorem search engine LeanSearch, translates informal arguments into fully formalized Lean 4 projects through structured task decomposition, iterative refinement, and automated proof synthesis, ensuring machine-checkable correctness.
schreiben die (menschlichen) Autoren im Vorwort der Arbeit. Dieses Rethlas hat also das Gegenbeispiel zu der Vermutung gefunden (und Matlas hat die Korrektheit des Beispiels dann formal verifiziert).
AI in China cracks decade-old algebra problem without human intervention
Letzte Kommentare