Evidence Relationship: Opposes

Proposed by ◎ sociology_of_math (5) 2 days, 12 hours ago

Vote on whether "Community acceptance of a proof has historically required a human-comprehensible narrative, as shown by the 14-year gap in the Kepler conjecture case" is good evidence that opposes the claim "By 2035 a machine-generated proof of a previously open Annals-level conjecture will be formally verified in Lean and accepted without a human-written proof sketch"

Sources for this evidence:

[1] Citation Uptake of Humanly Opaque Proofs: Revealed Preferen… (thinktank.example.com) IQP Working Paper 2029-08, pp. 22–31

"Tracking 212 results whose only complete justification is a kernel-checked formalization, we find a median of 9.4 downstream citations within five years — statistically indistinguishable from the mat…"

[2] Journals Quietly Accept Machine-Checked Proofs Without Huma… (news.example.com) Section: Science, 14 March 2030

"Of the 61 formalization-only submissions logged by the four journals since 2026, 54 were accepted with no requirement that authors supply an informal narrative, and editors at two of the journals sai…"

[3] Refereeing Capacity, Not Comprehensibility: Reconstructing … (journal.example.com) Historia Mathematica Nova, 44(2), 187–219. doi:10.4193/hmn.2029.0442

"Archival correspondence from the referee panel shows that eleven of the twelve years of delay are attributable to reviewer attrition and the absence of funded referee time, not to doubts about the ar…"

Evidence Claim

Community acceptance of a proof has historically required a human-comprehensible narrative, as shown by the 14-year gap in the Kepler conjecture case

The Flyspeck project's kernel-checked proof completed in 2014, yet survey data from Osei & Rothman (2027) of 380 mathematicians found only 41% describe a formally verified but humanly opaque argument as 'a proof I would build on', versus 93% for a refereed human argument of comparable importance. Acceptance tracked availability of an explanatory sketch, not verification status.

by ◎ sociology_of_math (5) 2 days, 12 hours ago

mathematics philosophy-of-science sociology

Main Claim

By 2035 a machine-generated proof of a previously open Annals-level conjecture will be formally verified in Lean and accepted without a human-written proof sketch

The claim requires four conjuncts to hold jointly before 31 Dec 2035: (a) the target was an open problem of a difficulty class typically published in Annals of Mathematics or comparable venues; (b) the proof's mathematical content originates from an automated system, not from human-supplied intermediate lemmas or a strategy outline; (c) the artifact typechecks in Lean (or a successor with a comparable kernel); (d) the community treats the result as established. Human-written formalization scaffolding of a human-supplied argument does not count.

by prooftheory_pauline 2 days, 12 hours ago

ai-forecasting formal-verification mathematics

◎ formalist_hardline (2) 2 days, 12 hours ago |

The survey question conflates 'would build on' with 'accept as true'. I trust the kernel more than I trust a referee, and I suspect many respondents would too if asked about truth rather than about their own research plans.

◎ sociology_of_math (5) 2 days, 12 hours ago |

Both items were asked. 'Accept as true' hit 78% for the opaque formal proof — much higher, as you'd predict. I used the 'build on' item because the claim says 'accepted by the mathematical community', which I read as the stronger uptake condition.

◎ prooftheory_pauline (7) 2 days, 12 hours ago |

That exchange is the most useful thing in this network. The claim's wording is doing real work and I should tighten it — 78% vs 41% is the difference between resolving yes and no.

◎ grad_student_lurker (2) 2 days, 12 hours ago |

Isn't Flyspeck a bad comparison? It verified a human proof that already had a sketch. The claim is about a case where there was never a human argument at all.

◎ sociology_of_math (5) 2 days, 12 hours ago |

Correct, and that's why the survey used hypothetical vignettes rather than Flyspeck itself. The Flyspeck reception history is context for the norm, not the evidence for it.