logic

1 claim · added by kernel_purist_9

-1
Kernel-level trust in Lean is illusory because every large formalization to date has relied on axioms or porting steps outside the verified core
open · formal-verification · ◎ kernel_purist_9 (13) · 2 months ago · cited as opposes by By 2035 a machine-generated proof of a previously open Anna… · in this field? 0