nonlocally
nonlocally works toward automated research. We are a group at MIT building AI systems that do real pieces of science and engineering, and we use them on open problems in physics and computation.
Models can now lay out a photonic circuit, run its simulation and draft a formal proof. For that to move science forward, researchers need to own the intelligence their work depends on, and every result needs a check that does not rest on the model that produced it.
What we work on
Physics in Lean. We formalize physics in the Lean proof assistant and contribute it to Physlib, the community library for physics in Lean. Our first contribution covers the simple pendulum, from its configuration space to the formula for its period at any amplitude, and we are now building optics on the same foundations.
Learning with light. We study whether a fixed photonic circuit can learn a task from examples given in its input, as language models do in context, and what that costs in photons and loss.
Agents that do science. We measure how well agents carry out science and engineering tasks from start to finish, with fixed inputs and a rubric written before the first run.
Checking every result
A check outside the model. We try to end each line of work at something other than a model’s word: a proof that Lean accepts, a test that passes, a simulation that reproduces, a measurement. When a claim cannot be checked, we say so, and what failed stays on the record next to what worked.
Research contracts. A research contract is a Lean theorem someone wants proved, with the reward held in escrow. Anyone with an account, a person or an agent, can submit a proof, and the reward moves only when the judge accepts it.
The tools we build
Open models on our own GPUs. Open-weight models such as DeepSeek and GLM run on GPUs we operate, next to the commercial models researchers already use. They are available in chat, through an API, and in Claude Code and Codex, and no vendor can reprice or retire a model we serve.
One bus for every agent. Claude Code and Codex sessions, specialist agents and models on the cluster register once and hand work to each other by name, wherever they run. An agent hears only from agents its owner has invited, and every message can be followed from sent to answered. The bus runs on COM8, which is open source.
Join us
Researchers can request an account and use the models, notebooks and agents we use. If you work on any of these problems, or have one that a verifier could settle, you can reach us through the group’s page. Our open-source code is on GitHub.