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
Wenn Ihnen der Artikel gefallen hat, vergessen Sie nicht, ihn mit Ihren Freunden zu teilen. Folgen Sie uns auch in Google News, klicken Sie auf den Stern und wählen Sie uns aus Ihren Favoriten aus.
Wenn Sie weitere Nachrichten lesen möchten, können Sie unsere Wissenschaft kategorie besuchen.
