I love Lean 4 as a general purpose programming language, but I can't use it because no current AI coding assistant can reliably work with me in Lean. I can be trying six languages at once like a chess master playing an exhibition simultaneous match, and they'll all flow in Cursor using Claude 3.5 Sonnet, or even Windsurf. Then add Lean 4 and everyone chokes.<p>On the other hand, Claude 3.5 Sonnet understands my iPad math drawings better than my colleagues. I am admittedly weird, but AI as an association engine of incomprehensible scope likes trippy. Trippy helps its reach. Philosophy never really worked until now when you can run it on a computer. AI really rewards recursive meta; it picks up speed like ice sailing. We're would-be shamans sitting around the fire a million years ago, imagining we can control the dance of the flames. With AI, we can.<p>Claude also understands, say, computational group theory or strategies for combinatorial enumeration, remarkably well. So it can assist in math research.<p>Formal proofs in Lean 4 may be hard to read, but the elephant in the room is how hard conventional math papers are to read. We're terrible at expressing ourselves, so reading a paper is the equivalent of reverse-engineering bad computer code to reconstruct thoughts the author failed to express. And it's embarrassing in 2025 that conventional papers can't be automatically checked.<p>A new genre will emerge in between: In the "Centaur" model Gary Kasparov popularized after he recovered from his chess defeat by IBM's Big Blue, we want papers to actually be very careful, battle-tested prompts for AI. They will pass as conventional papers for mathematicians still trapped in amber, but they're really just prompts for both us and AI.<p>The documentation for Lean 4 is aimed at humans. If it were designed to be a hybrid "Centaur" prompt doc, perhaps my tools would be better able to help me code in Lean 4.
I’m no expert in formal methods, but of all the tools I’ve used, Athena [0] has been one of my favorites to work with. The proofs read much more like what you’re used to seeing in math literature.<p>0. <a href="https://athena-lang.org/" rel="nofollow">https://athena-lang.org/</a>
The title is quite misleading. This is a tutorial on reading a Lean verification script so the title should be like "Anatomy of a Lean verification script". As it is it suggests that all formal proofs look like this which they typically don't.