lukeplato

> Our models produced a natural language proof for Yang–Mills existence on September 9th, 2026, and then subsequently produced a proof for QCD on September 18th, 2026. Given the length and complexity of the work, we postponed release until the Lean formalization completed. We finished our formalization of Yang–Mills’ existence on October 16th, 2026, which led us to develop the collaboration described here

absolutely insane

incredible that ideas like this are still being invented

Many comments seem to be misinterpreting this, but all this seems to be suggesting is that the AI companies should not be treating mathematical milestones as benchmark targets but need to release the cumulative findings in a human interpretable and digestible way that enriches and develops the field. See Thurston quote on Tao's banner:

> We are not trying to meet some abstract production quota of definitions, theorems and proofs. The measure of our success is whether what we do enables people to understand and think more clearly and effectively about mathematics.

they're probably referring to CASP13/14