You guys are missing the forest for the trees.

They used an AI agent sending ideas to a fuzzer and discovered a heap buffer overflow in Lean. This is big.

Indeed this is a nice discovery and I think it is useful in its own right.