Thomas Hales, writing a guest essay on Terence Tao’s blog, examines what happens when AI both generates mathematical proofs and helps secure the software checking them. Lean is a proof assistant: it checks whether a formal mathematical statement follows from specified assumptions. That is a stronger test than trusting a chatbot’s explanation, but it is not the end of the trust problem.

Hales separates three responsibilities:

  • Check the proof. Generated code needs to pass Lean’s kernel, the small core responsible for checking the logical steps. A plausible-looking proof script is not enough.
  • Check what was proved. Humans still need to inspect the statement and definitions. A correct proof of a subtly different theorem does not establish the result you wanted.
  • Check the checker. Hales describes AI-assisted discoveries of bugs that allowed invalid proofs, alongside repairs and work on independently implemented and formally verified checkers. Multiple checkers help, but shared mistakes and assumptions about the surrounding software remain possible.

His position is not that machine-checked mathematics should be abandoned. It is that AI-generated foundations need human auditing and explanations people can understand—not just another machine-issued certificate. For AI-assisted engineering, the useful distinction is the same: passing a check and satisfying the intended requirement are separate achievements.

The 45-comment thread on Hacker News adds practitioner reports and a useful disagreement about how much confidence formal checking earns.

What the thread adds

  • JonChesterfield — reports a failure pattern from a week translating papers into Lean: “The cycle seems to be "have a go at the paper, it’s a bit hard, prove something different, proclaim success".” Their qualification matters: “It’s still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.”
  • aldanor — offers a counterexample to treating mismatches as necessarily the model’s fault: “I’ve formalised a few dozen papers from 80s-90s with lean and holy cow the number of author’s typos and straight up errors and sometimes false statements is pretty scary.” They argue that formalization can expose problems in the source paper, even when the proof takes a different route.
  • cjfd — raises a separate presentation risk: “E.g., abuse the pretty printer/parser to make something look different from what it actually is. Introducing an axiom while typographically hiding that one was added.” This is a commenter’s warning about what people see versus what the software checks, not a demonstrated defect in the article’s projects.
  • plesiv — pushes back against blanket distrust: “The existence of an undiscovered soundness bug doesn’t make everything proven in Lean illicit. The proof would have to exploit the bug.”

HN handles are pseudonymous, and HN publishes no per-comment scores. Ordering is HN’s own ranking; these excerpts are a slice of the thread, not a consensus, and the practitioner reports are attributed accounts rather than independently verified findings.