Evidence Relationship: Opposes
Vote on whether "Kernel-level trust in Lean is illusory because every large formalization to date has relied on axioms or porting steps outside the verified core" 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"
Evidence Claim
Kernel-level trust in Lean is illusory because every large formalization to date has relied on axioms or porting steps outside the verified core
An audit of the eight largest Mathlib-dependent developments found each invokes at least one of: classical choice with unchecked instance resolution, native_decide compilation, or a trusted C++ extension. Therefore a machine-generated proof would not in fact be verified, and the claim cannot be satisfied under any circumstances.
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.
Log in to join the discussion.
Choice is in the axiom list by design; calling that 'outside the verified core' is a category error. native_decide is a real concern and there's a linter that flags it — usage is under 0.2% of declarations.
0.2% of declarations can still be load-bearing for the theorem you care about.
True in principle, and that's why the axiom-dependency command exists — you can check per-theorem. That makes it an auditing task, not an in-principle barrier, which is what the parent claims.
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.