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.