Recently, the erdosproblems.com site run by Thomas Bloom has enabled a discussion forum for each of the problems on the site.
As a result of some discussions I had with Stijn Cambie and Vjeko Kovac on this forum, we were able to come up with a short elementary solution to a previously open problem on the site: https://www.erdosproblems.com/forum/thread/379 . In fact the proof is sufficiently short and elementary that it was straightforward to formalize in Lean! https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/erdos_379.lean
Terence Tao
npub1gv…2sduy
2025-08-28 22:58:48 UTC
Author Public Key
npub1gvea966levf836g93xsdnkde8mmz58qyznf9c82jg02hq35f46lsn2sduySeen on
wss://relay.momostr.pinkPublished at
2025-08-28 22:58:48 UTCEvent JSON
{
"id": "0e5debed829c4abeaf7320d7af2505b29c59fd273f22a414c420de38c0b39605",
"pubkey": "4333d2eb5fcb1278e90589a0d9d9b93ef62a1c0414d25c1d5243d5704689aebf",
"created_at": 1756421928,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/@tao/115108867524771760",
"web"
],
[
"proxy",
"https://mathstodon.xyz/users/tao/statuses/115108867524771760",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/tao/statuses/115108867524771760",
"pink.momostr"
],
[
"-"
]
],
"content": "Recently, the erdosproblems.com site run by Thomas Bloom has enabled a discussion forum for each of the problems on the site.\n\nAs a result of some discussions I had with Stijn Cambie and Vjeko Kovac on this forum, we were able to come up with a short elementary solution to a previously open problem on the site: https://www.erdosproblems.com/forum/thread/379 . In fact the proof is sufficiently short and elementary that it was straightforward to formalize in Lean! https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/erdos_379.lean",
"sig": "4e3ed6a8ed48339c1e7cbd03c63812adc89b4395b747b68b29a2c22b2eece926d74be32fea0db7d645a4c7a8af5e266dabc5477d0f09e17c5b03d19c7c84c0cb"
}