grad_student_lurker

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
  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.
  0 points · 2 days, 13 hours ago
• on Kernel-level trust in Lean is illusory because every large formalization to date has relied on axioms or porting steps outside the verified core 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
  Downvoting rather than replying at length: the leap from 'some developments use native_decide' to 'the claim cannot be satisfied under any circumstances' is not an argument.
  0 points · 2 days, 13 hours ago