While working on the revision of the Equational Theories Project (ETP) report at https://arxiv.org/abs/2512.07087 I came across an observation that we quietly made at the back of that report (see Section 14.1) but has become more relevant today.
The ETP was a successful project, running over several months, to resolve over 22 million implications in universal algebra (and formalize them in Lean) through a variety of methods, both human and automated, although in our case the automation was much more in the ``good old-fashioned'' form of utilizing automated theorem provers (ATP) and simple scripts, rather than modern LLMs. If ETP were run today, it is likely that modern LLMs would very quickly resolve almost all of the implications studied, and the few remaining holdouts would likely then fall in a matter of days with additional LLM compute. (1/3)
Terence Tao
npub1gv…2sduy
2026-09-07 17:40:45 UTC
Author Public Key
npub1gvea966levf836g93xsdnkde8mmz58qyznf9c82jg02hq35f46lsn2sduyPublished at
2026-09-07 17:40:45 UTCEvent JSON
{
"id": "a1ede096b8027f8cea458f8f7f766ef4a73b3926e85e930575bc289bec6ff3ac",
"pubkey": "4333d2eb5fcb1278e90589a0d9d9b93ef62a1c0414d25c1d5243d5704689aebf",
"created_at": 1788802845,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/@tao/117230983266837293",
"web"
],
[
"proxy",
"https://mathstodon.xyz/users/tao/statuses/117230983266837293",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/tao/statuses/117230983266837293",
"pink.momostr"
],
[
"-"
]
],
"content": "While working on the revision of the Equational Theories Project (ETP) report at https://arxiv.org/abs/2512.07087 I came across an observation that we quietly made at the back of that report (see Section 14.1) but has become more relevant today.\n\nThe ETP was a successful project, running over several months, to resolve over 22 million implications in universal algebra (and formalize them in Lean) through a variety of methods, both human and automated, although in our case the automation was much more in the ``good old-fashioned'' form of utilizing automated theorem provers (ATP) and simple scripts, rather than modern LLMs. If ETP were run today, it is likely that modern LLMs would very quickly resolve almost all of the implications studied, and the few remaining holdouts would likely then fall in a matter of days with additional LLM compute. (1/3)",
"sig": "75b214954287032766d3e80e7a511d33279c648aed9d0696c5bd2c36da69f210b18fe49f7048617e81c45cfccc763efa24e63939561c6260d3daf17c9cfe53b6"
}