ORBIT programme overview
One programme. Three directions.
ORBIT is Overdog Research in Behaviour, Inference and Theorems: AI behaviour, statistics and mathematics. Each direction has its own questions and concrete work.
We investigate them together to ask whether better representations can connect proof and behaviour. Statistical tests and formal methods help examine that possibility; they do not establish the connection.
01AI behaviour · the Behaviour direction
How does risk develop across a multi-turn interaction?
Context, memory, tools and changing world state shape an AI system's actions. Can we recognise a developing failure across the interaction early enough for a predefined response to matter?
Current programme: CARF, the Conformal Agentic Risk Framework.
Status: Pre-deployment research. Internally reported synthetic results do not establish prospective early-warning performance.
02Statistics · the Inference direction
What can limited or accumulating evidence justify?
What do observations support, and how uncertain is the conclusion? This direction studies sparse data, exact and sequential inference, calibration and method comparison under stated assumptions.
Current programme: exact and sequential inference.
Public software: ExactCIs, design-aware confidence intervals for 2 × 2 tables. Not every method is exact; this is not CARF validation.
03Mathematics · the Theorems direction
Which representations make difficult problems tractable?
Can a better representation make a difficult problem tractable? Exact objects, computation and proof support reductions and exclusions, with each implication stated explicitly.
Current programme: Erdős Basecamp.
Public result: Paper I gives 17/41 exclusions in its stated shifted-square/Lucas-sequence setting. Erdős 364 remains open.
04Bridge hypothesis
Finding the mathematics between proof and behaviour.
The Rosetta Stone hypothesis asks whether representations, dynamics and constraints can transfer usefully across domains. A useful general translation has not been established.
A candidate mathematical description of state, change, constraint and control that both routes could reach. Whether one exists, and what it would preserve, is the open question.
05Formal methods · shared layer
One shared capability, three different jobs.
Formal methods are not a fourth research direction. Always state the proposition being proved: Lean-checked
is not itself the result.
Machine-check mathematical definitions and implications under stated hypotheses. A theorem fragment does not settle an open conjecture.
Formalise statistical objects and guarantees where useful. Name the construction, assumptions and error or coverage property, not just the proof system.
Specify effect-authorisation and refusal rules; check refinement and conformance. A release-boundary proof does not establish upstream scientific correctness or warning performance.
06Further reading