A critical look at Lean4
Addresses foundational concerns about formal verification tools used in AI safety research and certification.
AI Summary
Critically examines Lean4's limitations as an immature formal verification tool, questioning its readiness for societal-level trust in AI safety certification.
Excerpt
Lots of the discussion around Lean certificates and trust centers around general philosophical ideas of how much humans should trust formal certificates. It's important to remember, though, that Lean4 is not an ideal formal certificate machine: Lean4 is a software in its infancy and has issues. There are reasonable reasons to specifically not trust Lean4. If we're going to be putting our society's trust in Lean4, I think that it's good to have an open critical discussion of how warranted that tr