Development

Thirty thousand agents formalize a graduate textbook

development2026-04-05

Claim

Meta researchers translated an entire graduate mathematics textbook into Lean using 30,000 language model agents, turning formalization into a parallelizable compute job.

Reported metric: 30,000 agents

Reporting date: 2026-04-05 (not necessarily the event date)

Sources

Attribution and reporting linked by this record; links do not imply independent verification.

Welcome to April 5, 2026 (theinnermostloop.substack.com)

Knowledge graphopen in browser →

Reported in

Welcome to April 5, 2026

Actor

Meta

Evidence for

Supersedes

Three more Erdős problems fall to an internal model

Referenced by

Cite or correct this record

Citation formatCitation text

Thirty thousand agents formalize a graduate textbook
Innermost Loop KB — secondary record
Reporting date: 2026-04-05
KB permalink: https://nicholsn.github.io/innermost-loop-kb/developments/2026-04-05-a-textbook-formalized-by-30000-agents
Claim: Meta researchers translated an entire graduate mathematics textbook into Lean using 30,000 language model agents, turning formalization into a parallelizable compute job.
Attributed sources:
- Welcome to April 5, 2026 — https://theinnermostloop.substack.com/p/welcome-to-april-5-2026
This citation does not imply independent verification of linked-source claims.

Suggest a correction — opens a GitHub draft for you to review and submit.