Reactive Proof Search: Orchestration via XState v5

As autonomous mathematical research systems scale, procedural orchestration becomes increasingly difficult to maintain and verify. Relying on complex await chains and nested loops introduces non-deterministic behavior that can compromise the integrity of the research pipeline.

To address these challenges, we have transitioned Perqed's orchestration layer to a reactive state machine using XState v5. This architectural shift provides a formal framework for managing the research lifecycle—from literature-based ideation to empirical validation and formal verification.

State Machine Topology

The orchestration logic is represented as a Directed Acyclic Graph (DAG) of state transitions. This approach ensures that the entire research process is deterministic and auditable. We have mapped the core research flow into a 10-state topology that explicitly handles successful transitions, falsification forks, and execution plateaus.

Actor-Model Implementation

Each component of the system—including the Librarian, Explorer, and Formalist—is encapsulated as an isolated actor using XState's fromPromise API. These actors are stateless, receiving structured input and returning typed output, while the central Hub manages the transition logic.

This decoupling facilitates robust error recovery. For instance, if the Validation actor identifies an invalid syntax tree, the Hub captures the event, increments a retry counter, and re-routes execution to the Ideation node. Similarly, if the Explorer identifies a search plateau, the system can automatically transition to an SMT-based resolution node to evaluate the subspace using Z3.

Formal Verification of Orchestration

The transition to a formal state machine significantly improves the verifiability of the orchestration logic. By utilizing XState's .provide() API, we can inject mocked actors into the state machine, enabling exhaustive testing of the topology without external dependencies. Our validation suite verifies all 10 states and their associated transitions—including edge cases and terminal failure states—within a controlled environment, ensuring that Hub-and-Spoke coordination remains consistent across diverse research tasks.

By implementing a mathematically sound orchestration layer, we have established a robust foundation for autonomous mathematical discovery.