Our research programme runs long automated jobs. Language models propose mathematical statements, other models try to prove them, and a formal proof checker, the Lean kernel, accepts or rejects every proof. A run lasts days. Before these screens existed, the only way to know what a run had done was to read its logs.
The cockpit is a live view of those runs. It streams the state of the run as it changes: how many results the checker has certified, how many statements are still open, how productive each model is for what it costs, and a genealogy graph that traces every certified result back to the model branch that produced it. Clicking a node opens its record. No number on the screen is typed by hand: each one is read from the ledger the checker writes.
The screen answers the questions a person asks first: what was certified, what is still open, which model is worth what it costs. The detail of each result stays one click away instead of crowding the first screen.
The software itself
A screen from the running tool. Theorem and model names are blurred.
Why it holds
The screens only show what an independent checker has already accepted. The cockpit does not decide whether a proof is correct: the kernel does, and the cockpit counts its verdicts. That separation is what lets someone who cannot read the proofs still trust a number on the screen.
The cockpit is plain Python and JavaScript, with no framework and no third-party package, so it starts in about a second on any machine that has Python. The same approach carries over to an operations dashboard on a business process: read the source of truth, never retype it.
SCOPE AND LIMITS
This is an internal tool, not a product. It is not sold, and it appears here for its interface rather than as a deliverable. It reads files on the machine that runs the jobs; serving it to a team would add sign-in and access control, which it does not have.