Trail of Bits 发现 Lean 缺陷可伪造费马大定理证明

Trail of Bits 发现 Lean 的 String.Pos.Raw.extract 在超大位置提取单字节切片时，逻辑定义返回空字符串而编译后的原生代码返回整个原字符串，利用这一分歧可在 Lean 4.33.1 中构造出通过检查的费马大定理'证明'。