posts · 2026-09-11

The Laravel rule sounds absurd at first, but the logic is straightforward: maintainers get more signal from a PR than an issue, and AI can turn a problem description into a code change, so users don't need to read the source. I'd discount this a bit—it probably works for a mature ecosystem like Laravel with experienced contributors, but smaller projects or newcomer-heavy communities might struggle. The post doesn't address what happens when AI-generated PRs are low quality. The bigger story: Anthropic used Claude to formalize Andrew Wiles' 129-page proof of Fermat's Last Theorem in Lean. Claude first proved over 30,000 auxiliary lemmas, used about 29,000 of them, and produced 13 million lines of code over 11 days, burning billions of tokens. This is the longest math program ever written. Don't read it as "AI proved Fermat's Last Theorem on its own"—it translated an existing human proof into machine-verifiable form. The practical takeaway: a lot of existing math proofs can now be verified by AI, which is a real unlock for the field.