Another interesting example of modern computer assistance in mathematics, again involving the https://www.erdosproblems.com/ site: Problem #707 (https://www.erdosproblems.com/707), previously marked as "open", is now "disproved" - with the disproof formalized in Lean : https://borisalexeev.com/papers/erdos707.html . But the path towards that disproof was quite unusual, not fitting neatly into any of the standard narratives about AI in mathematics:
* The authors' initial proof used some numerical computer experiments, but did not get much help from LLMs initially, with even the code generated by hand.
* The authors then found a disproof by conventional human arguments (and also obtained some stronger results of a similar nature), and did not turn up any prior solution to this problem in their literature searches. Even the modern AI deep research tools did not locate any hits.
* Nevertheless, as part of the process of writing the paper, they found a solution to the problem (slightly different from theirs) had been obtained by Hall, thirty years before Erdos even posed the problem!
* Perturbed by this, the authors then decided to formalize both their result and Hall's result in Lean. (1/3)
Terence Tao
npub1gv…2sduy
2025-10-22 05:39:47 UTC
Author Public Key
npub1gvea966levf836g93xsdnkde8mmz58qyznf9c82jg02hq35f46lsn2sduySeen on
wss://relay.momostr.pinkPublished at
2025-10-22 05:39:47 UTCEvent JSON
{
"id": "16b353aed174b6efe42f3a3f7fef5004ecc63507fd2425abafb5645da0205667",
"pubkey": "4333d2eb5fcb1278e90589a0d9d9b93ef62a1c0414d25c1d5243d5704689aebf",
"created_at": 1761111587,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/@tao/115416208975810074",
"web"
],
[
"proxy",
"https://mathstodon.xyz/users/tao/statuses/115416208975810074",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/tao/statuses/115416208975810074",
"pink.momostr"
],
[
"-"
]
],
"content": "Another interesting example of modern computer assistance in mathematics, again involving the https://www.erdosproblems.com/ site: Problem #707 (https://www.erdosproblems.com/707), previously marked as \"open\", is now \"disproved\" - with the disproof formalized in Lean : https://borisalexeev.com/papers/erdos707.html . But the path towards that disproof was quite unusual, not fitting neatly into any of the standard narratives about AI in mathematics:\n\n* The authors' initial proof used some numerical computer experiments, but did not get much help from LLMs initially, with even the code generated by hand.\n\n* The authors then found a disproof by conventional human arguments (and also obtained some stronger results of a similar nature), and did not turn up any prior solution to this problem in their literature searches. Even the modern AI deep research tools did not locate any hits.\n\n* Nevertheless, as part of the process of writing the paper, they found a solution to the problem (slightly different from theirs) had been obtained by Hall, thirty years before Erdos even posed the problem!\n\n* Perturbed by this, the authors then decided to formalize both their result and Hall's result in Lean. (1/3)",
"sig": "6dbf5f792e3abf9ebb7350dd5ee203b283403b5c80c2d99d2deb89219b9900b8af958afa911a6d1a056243c7955cd6870f4e64a8544e573a3d9c304b288e5957"
}