Anatomy of a Formal Proof
ams.org
ams.org
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.
Claude also understands, say, computational group theory or strategies for combinatorial enumeration, remarkably well. So it can assist in math research.
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.
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.
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.
The process is acutely painful. It can't stick to directions, and keeps trying to add proof features that it can't get to work, despite my instructions that we're using Lean 4 as a general purpose programming language.
To my surprise, the code ran faster than either Haskell or Rust on a small case. There could be so many artifacts involved in such a conclusion, but larger cases blew the stack. That's just inexperienced code.
Yup, that's mostly a factor of using declarative proofs rather than lists of proof "tactics" based on an entirely opaque proof state (that can only be reconstructed and understood by replaying them in the proof system). You'd find these proofs in systems like Mizar or Isar (a declarative framework that's part of Isabelle). Systems like Lean and Coq/Rocq do support structured proofs that can act as a minimal step towards declarativity but are not nearly as readable as actual declarative proofs.
I don't recall how it is built already.