Autoform Bot: Multi-agent system for translating LaTeX mathematics into verified Lean 4 proofs

I'm Matt Wood, and this is For Your Information. A live list of riffs and links for you and your agent, drawn from what I'm reading, noticing, questioning, concluding, and revising.

Architecture: - Multi-agent pipeline with orchestrator, workers, and reviewers operating in a DAG workflow - MCP tool servers: filesystem, git, bash, Lean REPL/LSP, mathlib - Supports multi-node execution via SLURM - Configurable LLM backends (Claude Opus 4.6, GPT, Gemini)

github.com →

Connections

Supports

ATLAS: Autoformalized Textbook Library At Scale Autoform Bot's multi-agent LaTeX-to-Lean 4 translation pipeline provides exactly the kind of automated tooling needed to scale up large autoformalized libraries like ATLAS.

Supported by

Proof Editor - Collaborative Document Editor for Agents and Humans Proof Editor's live presence, comments, and provenance tracking for agent-human collaboration directly address the review and orchestration needs of Autoform Bot's DAG-based reviewer workflow.
What Sort of Maths Are LLMs Good At? Autoform Bot translating LaTeX mathematics into Lean 4 proofs is a specific instantiation of LLM mathematical capability that the new item's analysis would apply to
Leiden Declaration on Artificial Intelligence and Mathematics The Leiden Declaration on AI and Mathematics provides institutional/policy backing for exactly the kind of work Autoform Bot does — translating LaTeX mathematics into verified Lean 4 proofs, a core intersection of AI and formal mathematics.

Kimi Vendor Verifier Both rely on dedicated verifier/reviewer agents to check correctness of generated artifacts, whether vendor code or formal Lean proofs.
ARchitect: Automated Reasoning Policy Formalization for Bedrock Guardrails Both systems automate translation of natural-language or policy specifications into verifiable formal logic, one for AWS guardrails and the other for Lean 4 proofs.

Type:	link
First published:	Friday, 29 May 2026 at 12:00 UTC
Location:	https://github.com/facebookresearch/autoform-bot
URL:	https://mattwood.fyi/i/5023b165