Thomas Hales on Lean reliability, soundness bugs, and AI-driven autoformalization

Thomas Hales argues that proofs checked in the Lean theorem prover are only as reliable as its kernel, which has had several soundness bugs. He says autoformalization by AI makes formalization far faster, but human audits of kernels and statements remain essential. He also notes that Lean's type theory lacks a complete public consistency proof.