> 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?

▲

permute 5 hours ago | parent | next [-]

Maybe what you mean is that kernels of proof assistants must be small. Here I am referring to a geometry processing kernel (that is formally verified by a proof assistant). The implementation of the algorithm can be very long, the proof that it conforms to the spec can be very long. But lean checks the proof. And so you only have to trust the spec and that the lean proof assistant is correct.

In the 93 lines I assumed a reviewer already trusts that the kernel of the Lean proof assistants is correct. We have to trust somethings.

▲

agentultra 3 hours ago | parent [-]

What I’m wondering about is why we don’t need to understand/verify the generated kernel and only the spec?

Is there an implicit trust we must put in that kernel?

	▲	permute 2 hours ago \| parent [-]
		The implementation of a function is in the CSG/Impl folder. A proof is in the CSG/Proof folder. They are both imported and tied together in the human reviewed file in a theorem that makes a mathematical statement about the function. Lean checks mechanically that the theorems are proven via the supplied proofs. Here you have to trust the Lean checker, but neither the proof nor the implementation. Then you know that the statement in the file you reviewed holds about that function.

▲

UltraSane 3 hours ago | parent | prev [-]

Think of Lean proofs as a kind of inductive proof where if you trust the kernel then you trust every proof the kernel says is true.

▲

agentultra 3 hours ago | parent [-]

Right, I’m thinking of the de Bruijin criterion applied to the generated kernel in this case. That generated kernel sounds large, and being generated, I’m curious as to why or how we don’t have to verify/understand it?

	▲	saithound 2 hours ago \| parent [-]
		You're confused because the word kernel is used in two different senses. The "generated kernel" refers to a "geometric modeling kernel", which has absolutely nothing to do with the proof-checking kernel that the de Bruijn criterion talks about. The proof can be verified by Lean's ordinary proof-checker, or external checkers.