Share this page!

Enter URL or ID to Unroll

You can paste full URL like: https://x.com/threadreaderapp/status/1644127596119195649
or just the ID like: 1644127596119195649

How to get URL link on X (Twitter) App

  1. On the Twitter thread, click on or icon on the bottom
  2. Click again on or Share Via icon
  3. Click on Copy Link to Tweet
  4. Paste it above and click "Unroll Thread"!
  5. More info at Twitter Help
Fabian Gloeckle Profile picture
Fabian Gloeckle
@FabianGloeckle
PhD student at @AIatMeta and @EcoledesPonts with @syhw and @Amaury_Hayat, co-supervised by @wtgowers. Machine learning for mathematics and programming.
Apr 3 • 7 tweets • 2 min read
A new milestone in automatic formalization:
We translated an entire graduate math textbook into Lean using 30K LLM agents.
Open-source, large-scale multi-agent inference that actually works
> Blueprint+Lean: faabian.github.io/algebraic-comb…
> Codebase+preprint: github.com/facebookresear…
1/7 Image The target: Introduction to Algebraic Combinatorics by Darij Grinberg ().
Formalizes directly on top of Lean’s Mathlib while remaining largely disjoint from it, providing a realistic benchmark for the actual complexity of extending Mathlib book by book. 2/7arxiv.org/abs/2506.00738