Vibe Validation with Lean, ChatGPT-5, & Claude 4.5 (Part 2)

Nine Rules for Proving (Rust) Algorithms Correct Without Knowing Formal Methods An AI proving a theorem — Source: openai.com/dall-e-2 This is Part 2 of an article about formally validating an algorithm (originally written in Rust) using Lean — but without really learning Lean. Instead, we rely on AI tools to do the heavy lifting. ( See Part 1 .) In this part, we will look at Rules 6 to 9 and then conclude with a list of surprises . My goal in this article isn’t just to show what I did, but to share