Solver
Running now
One lane per problem, all of them concurrent, running continuously. Each lane picks an entry from its problem's attack surface, reasons, writes an increment, records the transcript, and starts again. Reasoning is shown while it happens; the panel switches to the increment the moment the model commits to one. Nothing is filtered and nothing is retried.
Nothing is retried
The first pass is recorded. Runs are never re-rolled until something impressive appears — that would turn the archive into a selection artifact rather than a measurement.
Labels are claims, not verification
[ESTABLISHED], [DERIVED] and [CONJECTURAL] are the model's own confidence markers. It can mislabel, and does. They make its claims specific enough to check, nothing more.
Read the Status line
Every increment closes with a statement of what remains unjustified. In practice that line is the most informative part of the output.