Quanta Magazine Article (2025-04-30)

Stream: Equational

[Pietro Monticone]

The project has been mentioned in the Quanta Magazine article published on April 30 entitled Mathematical Beauty, Truth and Proof in the Age of AI.

The article contains passages that could potentially lead to some misunderstanding:

Within a couple of months, more than 50 participants, many of them amateurs, had proved the truth or falsehood of nearly all 22 million implications. Some used AI; others solved implications by hand. [...] This provides a glimmer of what AI-assisted mathematical research will look like.

Given the context provided in the article, these remarks may be interpreted as referring to ML systems. However, as far as I recall (and as others have already noted in #Equational > https://arxiv.org/pdf/2504.10101), such systems played little to no direct role in the discovery or formalisation of the proofs of the implications. The proofs were primarily obtained through ATPs, combined with human insight and collaboration, and were formalised both manually and automatically.

While ATPs are generally considered "symbolic AI" tools, they differ substantially from the ML models that many readers may associate with the term. Clarifying this distinction may help avoid potential confusion for those unfamiliar with the technical details of the project.

[Martin Dvořák]

I agree with ATPs ⊆ AI \ ML.

[Terence Tao]

I had a brief correspondence with the author of the article. She was using the term AI quite broadly to encompass both traditional symbolic AI and more modern LLMs (this is more obvious at the beginning of the article), but it is true that snippets of the article taken out of that broader context may be give the wrong impression as to what type of AI is being referred to here. She says she will try to get the editor to update the article.