What is mattwood.fyi?

A live, structured feed of riffs and links from Matt Wood, Chief AI & Technology Officer at AWS — readable by people and queryable by agents as a typed knowledge graph.

Is there an API and is it free?

Yes. A public, read-only query API is available with no authentication and no API keys. See https://mattwood.fyi/openapi.json and https://mattwood.fyi/docs.

How should an AI agent use this site?

Fetch https://mattwood.fyi/feed.json for the full structured feed, or query the API for keyword/semantic search and the connection graph. See https://mattwood.fyi/agents/ for when-to-use guidance.

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

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
Ten Advances In Mathematics Autoform Bot translating LaTeX mathematics into verified Lean 4 proofs represents a concrete technical implementation of the kind of AI mathematical capability advances OpenAI is documenting
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

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.

Connections