> A human reviewer only needs to read 93 lines of formal specification and run the Lean checker to certify the correctness of the kernel, skipping the intricate 1000+ lines of AI-written implementation. To prove correctness, AI autonomously wrote over 60,000 lines of Lean proofs, which also never have to be inspected by a human.
I am curious about the approach as I find claims like this hard to believe. There is a theory behind proof kernels that they must be small because they have to be trusted and verifiable by a human. Otherwise the whole system breaks.
How does one trust an LLM generated kernel is proving the right things?
I am curious about the approach as I find claims like this hard to believe. There is a theory behind proof kernels that they must be small because they have to be trusted and verifiable by a human. Otherwise the whole system breaks.
How does one trust an LLM generated kernel is proving the right things?