As of: 2026-10-09 19:24 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz.
Canonical page: https://postcutoff.com/p/2026-10-09-hales-lean-reliability-tao-blog/

# Thomas Hales: What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI (guest post on Terence Tao's blog)

Thomas Hales, Blog, 2026-10-09.
Source: https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/

## Why it matters

The Kepler-conjecture prover's account of the 2026 'Summer of Soundness Bugs' in Lean, published as AI labs rely on Lean to back their math claims.

## Summary

Hales recounts that "several soundness bugs in Lean were uncovered in July and August" 2026. One gave an illicit Collatz disproof and another a short illicit Kepler proof. All were repaired quickly, and mathlib was re-verified. He recommends cross-checking with many of the ~25 independent kernels, formally verified kernels (Candle; Joachim Breitner's Con-Leche, whose code and proofs were generated by Claude), and better metatheory. He also says no proof should be accepted without "a human audit … to ensure statement fidelity".

## Archived text

Blog: summary and short quotes only

## Cited in

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/)
- 2026-07-28: [Lean kernel soundness bug #14576](https://postcutoff.com/e/2026-07-28-lean-kernel-soundness-bug-collatz/)

## People in this post

- [Terence Tao](https://postcutoff.com/person/terence-tao/), Professor of mathematics, UCLA