All projects
OpenMath: Catch-Up Agent
An agent that turns an AI-generated math paper into an audited briefing with an interactive picture, unattended. Built at the Build an Agent Hackathon in San Francisco, October 2026; working on one paper.
Built solo at the “Build an Agent” Hackathon, Corgi Cafe, San Francisco, on 7 October 2026. Paper in, briefing out, with no human step:
- The claim in plain words.
- Its verification status (Lean-checked, human-reviewed or unreviewed), read from the source repository rather than judged by the agent.
- An interactive picture: the agent picks a simulation from a small vetted library and emits a JSON spec, never pixels or code.
- A self-check: exact arithmetic on the paper’s worked example.
- Open questions.
It works today on one paper (OpenAI’s “Short Egyptian fractions”, Family 025), with 70 tests covering the proof map, the exact check and the card builder.
There is no hosted deployment; the agent runs locally. The briefing it produced for that paper is published as a static page.