---
title: "Discussion on \"Uncharted Waters: Thirteen Rules for Not Trusting an AI's Proofs\" | Hashnode"
description: "Discussion on \"Uncharted Waters: Thirteen Rules for Not Trusting an AI's Proofs\". Seven theorems in fifteen days, one refutation, ~104 cycles of Lean — and the ship's log of why nothing sank"
url: "https://hashnode.com/posts/uncharted-waters-thirteen-rules-for-not-trusting-an-ai-s-proofs/6a81d4b8ffe9b2105b711255"
---

[Feed](https://hashnode.com/feed) /

Discussion

# [Uncharted Waters: Thirteen Rules for Not Trusting an AI's Proofs](https://blog.iroha1203.dev/uncharted-waters-thirteen-rules-for-not-trusting-an-ai-s-proofs?utm_source=hashnode&utm_medium=feed)

Seven theorems in fifteen days, one refutation, ~104 cycles of Lean — and the ship's log of why nothing sank

Aug 16 · 18 min read · blog.iroha1203.dev  
Read the article

-   [#ai](https://hashnode.com/tag/ai)
-   [#loop-engineering](https://hashnode.com/tag/loop-engineering)
-   [#lean](https://hashnode.com/tag/lean)
-   [#software-engineering](https://hashnode.com/tag/software-engineering)
-   [#math](https://hashnode.com/tag/math)

## Written by

[Hiroyuki Nakahata](https://hashnode.com/@iroha1203)

@iroha1203 · Tokyo, Japan

  
[View profile](https://hashnode.com/@iroha1203)

Algebraic Architecture Theory

I’m a software engineer in Japan. Outside of work, I enjoy horse racing. ORCID:0009-0008-5928-0234

## Responses 1

Markdown supported · ⌘↵ to post

[Duko tools](https://hashnode.com/@talha24ramzan)

[Aug 18](https://hashnode.com/posts/uncharted-waters-thirteen-rules-for-not-trusting-an-ai-s-proofs/6a81d4b8ffe9b2105b711255/comment/6a8460c91d3089e1d3eccdb4)

Rule 10 is the one I'd want to see more of elsewhere, naming specific cheat shapes (vacuous success, playing to the grader, one-direction equivalence claims) turns "be suspicious" into something you can actually audit mechanically instead of relying on a reviewer remembering to be paranoid that day. Most AI-verification setups stop at "have a human check it," which doesn't scale past cycle 10, let alone 104.

The G-105 refutation being reframed as the first machine-checked evidence for a real claim is the best illustration of Rule 3 actually paying off, that only works because the failure-policy format was fixed before the refutation happened, not improvised afterward when the null result showed up.

Rule 12 pairing with Rule 13 is the quieter but more important design choice though, banning full-project verification inside the loop only works because a human explicitly decided where the cost tradeoff sits, rather than the loop discovering on its own that thorough checking is expensive and cutting corners.