2 citations · 2 across the 8 of their papers we have counts for
3 papers · 1 filter
Formalizing Mathematics at Scale
Ahmad Rammal, Niket Patel, Fabian Gloeckle +5
We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped…
Efficient RL Training for LLMs with Experience Replay
Charles Arnal, Vivien Cabannes, Taco Cohen +2
While Experience Replay - the practice of storing rollouts and reusing them multiple times during training - is a foundational technique in general RL, it remains largely unexplore…
Automatic Textbook Formalization
Fabian Gloeckle, Ahmad Rammal, Charles Arnal +4
We present a case study where an automatic AI system formalizes a textbook with more than 500 pages of graduate-level algebraic combinatorics to Lean. The resulting formalization r…