Mathematicians Assess the Novelty of Astra's Proofs Separately from Formal Verification

Mathematicians Assess the Novelty of Astra's Proofs Separately from Formal Verification

On August 6, Scientific American reported mathematicians' responses to the ten Astra results that OpenAI presented on August 1. They noted that the two most prominent papers drew on ideas from recent literature. OpenAI later revised its claim that these problems had seen no progress for decades.

The analysis of the manuscripts and Lean code for Astra's ten results focused on the proofs themselves. OpenAI published the manuscripts and formalizations in Lean, a language that allows software to check every recorded logical step. The code therefore makes it possible to verify independently whether each theorem follows from its stated proof.

Assessing novelty requires a different kind of review. A mathematician must trace the earlier results on which the current construction depends and determine what the construction adds to them.

The distinction is visible in the proof that a nonsofic group exists. A nonsofic group is a mathematical object that cannot be approximated with increasing accuracy by permutations of a finite number of elements. Astra constructed such an object. Andreas Thom, a coauthor of one of the preceding papers, explained how the new construction combines a 2016 theorem by Gábor Kun with a 2019 paper by Kun and Thom. Thom described it as a “creative and at the same time elementary construction.”

Formal verification establishes that the recorded chain of reasoning works. Comparing the papers and their references reveals where its central steps came from and which part of the work is genuinely new.