We're running Kairos with a small number of systems-neuroscience labs preparing Nature Methods submissions. Share your email and we'll be in touch within two business days.
The two-timescale actor‑critic convergence theorem that reinforcement-learning textbooks retell as the algorithmic ground of temporal‑difference credit assignment is false as commonly stated. The missing hypothesis is bounded feature maps, which biological feature spaces are not known to satisfy. Kairos derived the counterexample from the theorem statement itself and machine-checked the corrected theorem in Lean 4, with zero sorry and only the three standard logic axioms. An independent theorem prover (Aristotle, Harmonic.AI) arrived at the same conclusion through a different mathematical witness.
Kairos then re-analysed the public datasets of four recent Nature papers on dopaminergic learning (Tang 2024[1], Markowitz 2023[2], Greenstreet 2025[3], Sousa 2025[4]) and surfaced findings those papers did not report from their own data: the slow‑versus‑fast learner binary is a continuous population, not two clusters; per‑action credit windows vary by 48% across action types; value‑free action‑prediction error holds in 21 of 21 animals including under lesion, which rules out a single‑locus temporal‑difference account.
What this means. A textbook convergence argument that every dopamine-learning review cites has been under-specified for 25 years. The corrected theorem states the precise hypothesis biological feature maps must satisfy for that argument to apply, so papers that built on the original statement can re-ground their claims without rewriting their experiments. Labs proposing a new learning rule can now run Kairos as a pre-publication check: formal consistency, paradigm-replay calibration against the paradigm’s own data, and a distinguishability witness against competing rules, end-to-end on a laptop and without any new animal cohorts.
Scientific claims about neural computation proliferate faster than the field can distinguish them. Competing learning‑rule accounts each fit their own paradigm, but no pre‑publication apparatus checks a proposed rule simultaneously for biological faithfulness, algebraic consistency, and robustness under implementation mutations. Kairos closes that gap with a machine‑checked verification stack that refutes candidate rules against their paradigm’s own public data and leaves a reviewer‑reproducible bundle of Lean proofs and paradigm‑replay traces. Refutations are certain; support is provisional; the bundle is the evidence.
You give Kairos a scientific hypothesis. Kairos returns a verdict with bounds, a machine‑checked proof, and the candidate rules the hypothesis rules out.
A natural‑language claim, its formal statement, and a paradigm (paper, dataset, or instrumented simulator) it must hold against.
A verdict per verification layer, a sandwich bound on the key parameter, and a Lean proof that either closes the theorem or localises the counterexample.
theorem credit_window_is_one_over_e_decay (γ λ Δt : ℝ) (hgl_pos : 0 < γ * λ) (hgl_lt : γ * λ < 1) (hΔt : 0 < Δt) : Real.rpow (γ * λ) (creditWindowTau γ λ Δt / Δt) = Real.exp (−1)
In plain English: if the decay rate γλ lies strictly between 0 and 1, then exactly τc seconds after a reward, the eligibility signal has dropped to 1/e of its peak. No free parameters; the credit window is forced by γ, λ, and the simulator step Δt alone. The Tang 2024[1] data lives inside that bound, so the hypothesis survives this paper. Candidate rules that predict a wider or narrower window are rejected.
One concrete hypothesis, unpacked. The sliders are the paper's knobs, the formula is the relationship between them, the conditions below are the rules the hypothesis must obey, and the four candidates are the alternative theories Kairos compares against.
A real dopaminergic-learning paradigm is a multi-month, multi-mouse instrumented-wet-lab operation: Tang et al.\ 2024[1] trained 25 mice over three days; Greenstreet et al.[3] ran approximately 80. A single-shot frontier-model agent writes code but cannot close a Lean proof. A team of agents without a formal-verification layer still cannot calibrate against the paradigm’s own public data. A pure theorem prover takes a prose claim but cannot replay the paradigm. Kairos is the only apparatus that satisfies every capability the task requires and completes in minutes.
| Capability | Humans (wet‑lab) |
Claude Opus 4.6 | 3×Opus 4.6 (orch.) |
Aristotle (Harmonic) |
Kairos |
|---|---|---|---|---|---|
| Accepts natural-language hypothesis | ✓ | ✓ | ✓ | ✓ | ✓ |
Shared State type across paradigm encodings | ✗ | ✗ | ✗ | ✗ | ✓ |
| Simulates the Tang paradigm (Layer 3) | ✓ | ✗ | ✓ | ✗ | ✓ |
| Property tests at sampled parameters (Layer 2) | ✗ | ✗ | ✗ | ✗ | ✓ |
| Machine-checked Lean 4 proof (Layer 1) | ✗ | ✗ | ✓ | ✓ | ✓ |
| AST mutation catalog (Python + Lean) | ✗ | ✗ | ✗ | ✗ | ✓ |
| Calibrates against Tang and Sousa public data | ✓ | ✗ | ✗ | ✗ | ✓ |
| Spans four paradigm families in one framework | ✗ | ✗ | ✗ | ✗ | ✓ |
| Completes pre-publication | ✗ | ✓ | ✓ | ✓ | ✓ |
| Wall-clock | 3 months 10–80 mice | 4 min | 19 min | 30 min – 2 h | 16 min |
How to read. Each row is one capability the Tang 2024[1] credit-assignment paradigm actually demands. A ✓ means the alternative satisfies it; ✗ means it does not. Aristotle is Kairos’s independent cross-check arm on the hardest theorems. Kairos does not depend on it and completes every main-text claim without it.
Each row is one way Kairos can check a candidate rule. The five run in parallel; a rule has to pass every applicable row to survive.
For each candidate rule, Kairos ships a typed artifact per modality. Pick a tab to see the Lean theorem, property-test outputs, simulation trace, or mutation coverage for that rule.
-- off-state updates are identically zero theorem td0_cannot_produce_temporal_window (α γ : ℝ) (V : ValueFn) (s s' : State) (r : Reward) : ∀ x : State, x ≠ s → tdUpdate α γ V s r s' x = V x := by intro x hx exact td0_one_step_support α γ V s s' r x hx
Two bounds on the key parameter, plotted together. The left line is the lower bound derived from experimental data; the right line is the upper bound derived from the analytic formula. A rule is consistent with the data only if the real value lives inside that band. Kairos reports the gap between the two bounds.
The per-layer outcome, collapsed to one line. Refuted means at least one verification layer caught a contradiction. Supported means every applicable layer passed and the sandwich bound held, which is the strongest statement Kairos can make without claiming absolute certainty.