* But neither of the human authors had much experience in Lean, so they decided to "vibe code" a proof via ChatGPT. In contrast to most vibe coding use cases, this actually worked after several days of effort, giving a ~3000 line Lean proof that has been fully verified, using the formal statement of the theorem that was already present in the Formal Conjectures Repository at https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/707.lean
* But in doing so, they located a typo in that formalization (a condition that a certain modulus had to be nonzero was omitted).
Due to these latter developments, both ChatGPT and Lean are also listed as co-authors on the paper. (2/3)
Terence Tao
npub1gv…2sduy
2025-10-22 05:40:02 UTC
in reply to nevent1q…h52m
Author Public Key
npub1gvea966levf836g93xsdnkde8mmz58qyznf9c82jg02hq35f46lsn2sduySeen on
wss://relay.momostr.pinkPublished at
2025-10-22 05:40:02 UTCEvent JSON
{
"id": "cceaeccb2b8c4370cee03c0342b465ae8089798ec693b6dd33432f617281005b",
"pubkey": "4333d2eb5fcb1278e90589a0d9d9b93ef62a1c0414d25c1d5243d5704689aebf",
"created_at": 1761111602,
"kind": 1,
"tags": [
[
"e",
"16b353aed174b6efe42f3a3f7fef5004ecc63507fd2425abafb5645da0205667",
"",
"root",
"4333d2eb5fcb1278e90589a0d9d9b93ef62a1c0414d25c1d5243d5704689aebf"
],
[
"proxy",
"https://mathstodon.xyz/@tao/115416210007455376",
"web"
],
[
"p",
"4333d2eb5fcb1278e90589a0d9d9b93ef62a1c0414d25c1d5243d5704689aebf"
],
[
"proxy",
"https://mathstodon.xyz/users/tao/statuses/115416210007455376",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/tao/statuses/115416210007455376",
"pink.momostr"
],
[
"-"
]
],
"content": "* But neither of the human authors had much experience in Lean, so they decided to \"vibe code\" a proof via ChatGPT. In contrast to most vibe coding use cases, this actually worked after several days of effort, giving a ~3000 line Lean proof that has been fully verified, using the formal statement of the theorem that was already present in the Formal Conjectures Repository at https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/707.lean\n\n* But in doing so, they located a typo in that formalization (a condition that a certain modulus had to be nonzero was omitted).\n\nDue to these latter developments, both ChatGPT and Lean are also listed as co-authors on the paper. (2/3)",
"sig": "15233c74d392325e3b29e076ebe3d3e026c4d9efaf3ba6696101b42372475e913beea47fc64c3345fcf917e1de423c1d2e4fead3774e22f11af0991cbb37a19b"
}