Mathematicians will soon be out of a job

[John Clark]

An AI from Google solved nine out of 353 open Erdős problems it attempted, including two questions that had gone unanswered for 56 years. The system also proved 44 out of 492 open conjectures from the Online Encyclopedia of Integer Sequences (OEIS), settled a 15-year-old question about Hilbert functions in algebraic geometry, and improved a known bound in convex optimization. Inference costs ran just a few hundred dollars per problem:

Advancing Mathematics Research with AI-Driven Formal Proof Search

===

The following is a quote from: 

Fields Medal proof formalized for the first time

"The proofs were verified by the mathematical community and deemed correct, leading to the Fields Medal recognition. But formal verification, the ability of a proof to be verified by a computer, is another beast altogether. Formal verification of a proof is like a rubber stamp. It’s a kind of bona fide certification that you know your statements of reasoning are correct."

John K Clark    See what's on my list at  Extropolis

3xp