Thomas Hales는 테렌스 타오 블로그 기고에서 AI 형식 증명에 대한 신뢰를 커널 구현, 수학적 기반, 명제 충실성으로 나눠 설명했다. 2026년 여름 발견된 Lean 건전성 버그는 수정됐고 mathlib도 재검증됐지만 독립 커널 교차 검사가 모든 오류를 없애지는 않는다고 지적했다. 별도로 확인한 Con-Leche 저장소는 집합론 가정 아래 거짓 명제를 받아들이지 않는 외부 검사기를 제시한다. 이는 공식 커널의 무결함 보장이 아니며 실행 환경과 사람이 의도한 명제의 감사는 여전히 남는다.