formalist_hardline

No claims yet.

No evidence contributions yet.

Recent Comments

• on Community acceptance of a proof has historically required a human-comprehensible narrative, as shown by the 14-year gap in the Kepler conjecture case opposes 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 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 …
  0 points · 2 days, 13 hours ago
• on Journals accepting formalized-only submissions grew from 0 to 3 between 2025 and 2029, but all three require an accompanying informal exposition opposes 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 'machine-generated exposition, human vouched' clause basically dissolves the claim's fourth conjunct into a definitional question. Whoever resolves this in 2035 is going to have a bad time.
  0 points · 2 days, 13 hours ago