Intelligence should be scalable. Compute alone isn’t the path.
We investigate the structures and mechanisms that could make intelligent systems more capable, adaptive, and efficient. Our work is experimental; our conclusions must be earned.
THE CENTRAL QUESTION
Our prototype explores this question through structured theorem proving. A trusted host compiles an inspectable architecture into a proof searcher; candidate changes alter reasoning components while verification, evaluation, and resource accounting remain independent.
The next question goes beyond tactic ordering: can a system construct useful intermediate abstractions, verify them, and use them in future reasoning? Sustained recursive self-improvement remains an open research objective.
We investigate systems that modify their own reasoning mechanisms and the process used to discover those modifications. Architecture is mutable; evaluation and resource accounting must remain independent.
A solver improvement is not, by itself, recursive self-improvement. We ask whether a retained mechanism can causally improve subsequent research on new tasks.
Our experimental prototype uses Lean 4 as a proof verifier. Structured proof search makes it possible to inspect reasoning paths, test tactic composition, and distinguish an accepted proof from a plausible answer.
We investigate scoped proof state, typed dependencies, and intermediate constructions. A verified answer establishes correctness; separate experiments must establish transfer and efficiency.
We study changes to representation, search, retrieval, memory, and composition. The goal is to expand what a system can construct, beyond improving the ordering of a fixed action menu.
Current questions include typed obligation graphs, abstraction invention, and compiling verified constructions into reusable capabilities. These are research directions, not established general capabilities.
We evaluate capability alongside its full cost: discovery, verification, compilation, retrieval, and execution. Reuse matters when it helps on genuinely new tasks, rather than replaying a known answer.
Fixed budgets, parent–descendant comparisons, regression checks, and held-out problem families help distinguish useful mechanisms from improvements to the measurement itself.
OUR METHODOLOGY
Progress starts with a falsifiable hypothesis, not an assumed conclusion. We test changes against explicit criteria and let evidence determine what survives.
State a specific claim and define what would disprove it.
Build an inspectable, versioned change. Keep the evaluator outside the mutable architecture.
Compare with the parent under matched budgets. Check held-out transfer, regressions, and full costs.
Retain changes supported by independent evidence. Preserve failed experiments and negative results.
Rigorous empirical testing. Reproducible experiments. Falsifiable hypotheses. These are commitments to how we work, not evidence of results we have yet to establish.
Can typed dependency graphs and scoped intermediate obligations unlock reasoning that flat tactic search cannot express within the same budget?
When does a verified construction become a reusable abstraction? We must test new compositions, negative contexts, and the full cost of discovery and reuse.
Can an improved solver help diagnose failures, design experiments, and synthesize better research mechanisms on prospectively held-out campaigns?
AN OPEN CONVERSATION