Inspiration

Large language models have become remarkably capable mathematical assistants, yet AI assisted research is still treated as a sequence of independent interactions. And although existing tools can orchestrate models, invoke external software, and automate workflows, the investigation's memory remains short-lived; a conjecture, a failed proof, a symbolic computation, a counterexample, or a verification result are typically just pieces of text scattered across chats, notebooks, and scripts rather than persistent research artifacts.

Modern frameworks such as LangChain, Model Context Protocol (MCP), LeanDojo, SymPy, and Jupyter already make it easier to connect models and tools, and Pico Probe builds on many of these ideas. However, they primarily coordinate execution. They do not provide a unified representation of the evolving research process itself.

This became particularly apparent while I was researching problems involving geometric probability and polylogarithms; models could generate interesting conjectures quickly, but coordinating them was difficult. One model might make a subtle algebraic mistake, another might unknowingly build on it, and by the time I reached a symbolic computation or theorem prover, much of the reasoning history had already been lost. And after using the modern frameworks (LangChain, MCP, etc.) many questions still lingered in my mind:

- What promising research routes did the models consider and then silently discard before showing me a final plan? 
- Why was one proof strategy selected over another? 
- Can I recover an abandoned approach without asking the models to start over? 
- Which model first proposed this conjecture, and which later models modified or challenged it?
- What assumptions does this claim depend on? 
- Which earlier lemma, computation, or source supports this conclusion? 
- Was this result actually verified, or did several models merely agree with one another? 
- Did the symbolic calculation prove the full claim, or only check one algebraic step? And did the models reason independently, or did later models inherit the same mistake from an earlier response? 
- Can I replay the research process for verification in the order it occurred instead of reading a final transcript, even if I used many different AIs and tools? 
- Can another researcher inspect the evidence behind a claim without rerunning the entire project? Can they reuse my pipeline while changing the models, verification tools, or assurance requirements? Do other mathematicians use similar pipelines, and can I inspect their methods rather than only their final results?
- How can I distinguish a proof, a numerical observation, a model consensus, and an unsupported conjecture at a glance?
- If the investigation fails, is that failure preserved as useful mathematical knowledge or simply deleted?
- Can the system state clearly that a problem remains unresolved instead of forcing a polished answer?

And many more questions

These questions were the motivation behind Pico Probe.

Existing tools coordinate execution, but Pico Probe coordinates the evolution of mathematical knowledge and research.

Not only does Pico Probe save time, as multi-agent frameworks do, but the uniqueness lies in the fact that it prioritizes the preservation of scientific reasoning.

Pico Probe is not another multi-agent framework; it is a system that builds an investigation as a graph of mathematical knowledge, complete with provenance, verification, and reusable failed approaches. Instead of treating research as prompt engineering, it treats an investigation as a computational object composed of typed mathematical artifacts, explicit dependencies, execution history, provenance, and verification records. Every conjecture, proof attempt, computation, critique, and failed approach becomes part of a structured Research Graph that can be inspected, replayed, branched, verified, and extended long after the original conversation has ended.

This shifts the focus from connecting tools to capturing scientific reasoning. Rather than producing another AI response, Pico Probe builds a reusable record of how mathematical knowledge was generated, challenged, verified, and refined.

Git transformed software development by making the history of code persistent. Pico Probe applies a similar idea to AI-assisted research by making the evolution of mathematical reasoning persistent.

However, Pico Probe does not aim to just replace today's AI tools like LangChain or MCP; instead, Pico Probe complements today's AI tooling by adding a persistent research layer above models, theorem provers, and symbolic computation systems.

What it does

Pico Probe is research software for AI-assisted mathematics.

Rather than treating an investigation as a sequence of prompts, Pico Probe physically represents it as a persistent graph of nodes connected by explicit dependencies (in the research graph section). Researchers visually design a pipeline consisting of AI models, symbolic mathematics engines, theorem provers, numerical simulations, literature search, and custom plugins. The Research Kernel compiles this pipeline into an executable dependency graph and manages the communication between every component.

Unlike traditional prompt chaining, models do not simply exchange paragraphs of text. Each node communicates using a research protocol containing globally unique identifiers, timestamps, dependency information, provenance, and structured mathematical content.

class PicoPortMessage(BaseModel):
    message_id: str = Field(default_factory=new_message_id)
    schema_version: Literal["1.0"] = "1.0"
    project_id: str
    run_id: str
    branch_id: str | None = None
    pipeline_id: str
    pipeline_version: int
    pipeline_node_id: str
    direction: Literal["input", "output"]
    port: str
    schema_id: str
    object_ids: list[str] = Field(default_factory=list)
    data: dict[str, Any] = Field(default_factory=dict)
    artifacts: list[ArtifactReference] = Field(default_factory=list)
    provenance: ProvenanceRecord
    status: Literal["pending", "completed", "failed", "rejected", "waiting_for_user", "invalidated"] = "completed"

Before a node executes, the Research Kernel automatically compiles an execution envelope describing its role within the investigation.

class NodeExecutionEnvelope(BaseModel):
    schema_version: Literal["1.0"] = "1.0"
    project_id: str
    run_id: str
    branch_id: str | None = None
    pipeline_id: str
    pipeline_version: int
    pipeline_node_id: str
    research_question: str
    project_abstract: str = ""
    project_tags: list[str] = Field(default_factory=list)
    epistemic_contract: dict[str, Any]
    node_assurance_requirements: dict[str, Any]
    node_type: str
    node_role: str
    node_goal: str
    node_instructions: str
    incoming_edges: list[dict[str, Any]] = Field(default_factory=list)
    upstream: list[UpstreamValue] = Field(default_factory=list)
    inputs: list[PicoPortMessage] = Field(default_factory=list)
    downstream: list[DownstreamExpectation] = Field(default_factory=list)
    context: ResearchContextSnapshot = Field(default_factory=ResearchContextSnapshot)
    resolved_inputs: dict[str, Any] = Field(default_factory=dict)
    required_output_schema: dict[str, Any]
    required_output_type: str
    output_port_contracts: dict[str, dict[str, Any]] = Field(default_factory=dict)
    output_port_schema_ids: dict[str, str] = Field(default_factory=dict)
    budget: ExecutionBudget
    execution_mode: Literal["live", "local", "mock", "disabled"]
    provenance_requirements: dict[str, Any]

This means researchers no longer need to repeatedly explain which model generated what, where the output should go next, or what context another model needs. Every node automatically receives its upstream dependencies, downstream consumers, graph state, and execution history.

The visual pipeline is compiled into an executable graph:

Pipeline Editor
       │
       ▼
Graph Compiler
       │
       ▼
Execution DAG
       │
       ▼
Scheduler
       │
       ▼
Execution Envelopes
       │
       ▼
AI Models & Plugins
       │
       ▼
Research Graph

The platform routes work based on capabilities rather than providers. A request for symbolic simplification can be routed to SymPy or Mathematica, formal verification to Lean or Coq, numerical experimentation to Python or Monte Carlo simulation, reasoning tasks to any supported language model, and an option to import plugins. In fact, replacing one provider with another never changes the surrounding research pipeline.

Perhaps the most unique feature is what we call Negative Knowledge. If several models independently explore different proof strategies, Pico Probe does not discard the unsuccessful ones, as modern AIs and automated workflows can often do (under the hood). Every alternative route remains attached to the Research Graph as a failed, plausible, or unexplored branch, preserving its computations, critiques, verification attempts, and provenance. Instead of storing only the final answer, Pico Probe preserves the entire search process.

Every investigation becomes part of a graph that can be replayed chronologically, verified node by node, and extended months later without having to reconstruct previous work.

Accomplishments that we are proud of

The accomplishment we're most proud of is that Pico Probe became much more than a multi model UI, and it evolved into a research infrastructure.

Some of the components we are proud of include:

  • A Research Kernel that compiles visual research pipelines into executable dependency graphs. Structured communication between models using typed research artifacts instead of free form prompt chaining.
  • Automatic execution envelopes that provide upstream, downstream, dependency, and provenance information without manual prompting.
  • Capability based routing that separates research pipelines from specific AI providers.
  • A Research Graph that stores mathematical artifacts, semantic relationships, and execution history among various nodes (such as LLMs, Python code, Lean, SymPy, Ollama, and any plugin the user adds [approved and signed])
  • Complete provenance and replay for reproducible AI-assisted research.
  • Negative Knowledge, allowing discarded reasoning paths to remain available for future investigations.
  • A plugin system supporting AI models, symbolic mathematics systems, theorem provers, numerical computation, and custom research tools (extensibility to theorem provers, symbolic engines, simulations, and virtually any research tool)
  • Independent verification methods for the researcher such as Lean, SymPy, and a Python sandbox
  • A public library to publish all parts of your research, including the assurance contract, pipeline, verification, claim passport, and replay

How we built it

We began by building a multi-model AI pipeline in Python where a researcher would simply enter the number of API keys they had and for which AI models; then each AI would be given an index, eg, chatGPT = 1, Gemini = 2, Ollama = 3, etc., so the researcher could type a sequence of numbers corresponding to the pipeline like 12231 would give chatGPT--> Gemini --> Gemini --> ... --> chatGPT. But as we attempted to gradually build from there, the backend to-do list became far to complex and vast. So, we asked for the crucial assistance of Codex and ChatGPT 5.6 Sol, who helped us complete the project. We implemented a standard communication protocol instead of free-form text to mitigate AI hallucinations and increase rigour, efficiency, and provenance. Then we added a secure method for API key storage: first the key is encrypted with Fernet before storage; then the encrypted value is saved in the SQLite database; then that database is stored in a particular Docker; then the browser stores login tokens in localStorage, but not the raw provider API key.

The next crucial component was the Research Graph, where every mathematical object like questions, definitions, lemmas, conjectures, experiments, simulations, proofs, counterexamples, and verification results became nodes.

On top of that, Codex helped us build the Research Kernel responsible for compiling visual research pipelines into executable dependency graphs, generating execution envelopes, scheduling node execution, tracking provenance, and coordinating communication between systems.

Additionally, the platform was designed around a plugin architecture. So instead of hard coding integrations, every AI model or external tool exposes capabilities that can be discovered and routed automatically. This makes it possible to combine cloud models, local Ollama models, symbolic mathematics systems, theorem provers, numerical simulations, and future research tools within the same execution framework.

Next, we implemented persistent provenance and replay under the Replay tab. Every node stores execution metadata, provider information, timestamps, plugin invocations, generated code, verification objects, and graph dependencies so that an entire investigation can be reconstructed and inspected after execution.

Then, we created a public and private library for researchers to view their and other projects, allowing them to view the assurance contract, pipeline, verification, claim passport, and replay, which gives both inspiration, help, and collaboration for AI assisted math research.

Finally, we built the Research Summary that combines three stored records: the Claim Passport the Research Graph, and the Replay log then reads all claims and separates them by status: supported, accepted, verified, or concluded challenged, rejected, failed, contradicted, or inconclusive; it finds the strongest terminal result: first preference, the latest conclusion node second: the latest accepted node fallback: the final graph node; and it extracts readable text from fields such as results, conclusions, answers, explanations, and reasoning. Then it counts graph nodes, semantic edges, evidence, computation nodes, formal verification records, failed, contradictory, or dead-end routes, replay event sources, independent checks, and human decisions in order to generate three views: Plain language, which explains what question was investigated, whether any claim became supported, the clearest stored conclusion, and a practical next step. A Technical Report graph and execution statistics, such as: 12 typed graph nodes 15 semantic relationships 3 verification artifacts 2 failed routes 24 replay events. And an Evidence & assurance section which focuses on claim count, source count, independent checks, human decisions, and whether an Epistemic Contract exists. This design has two advantages: it works without an API key, and it cannot cause another model to invent a better-sounding conclusion or accidentally present an unverified claim as proven. The summary is therefore an interpretation of the stored research record, and crucially not an AI analysis. It also explicitly warns that the summary explains the stored record. It does not upgrade an unverified claim into a proof.

Finally, I ran this very project description you are currently reading into Codex just before my submission in order to confirm everything I claimed is implemented.

Challenges we ran into

The biggest challenge was deciding how mathematical reasoning should be represented.

Unlike ordinary chat applications, mathematical research is highly structured. A conjecture depends on assumptions, a proof depends on lemmas, symbolic computations verify only specific expressions, and numerical experiments provide evidence without constituting proofs. Capturing these distinctions required designing new data structures rather than simply storing text.

Another challenge was balancing automation with transparency. Fully autonomous systems can hide far too much information and reasoning under the hood, while manual workflows defeat the purpose of orchestration. Pico Probe attempts to automate the mechanical aspects of research like communication, scheduling, routing, provenance, and replay, while leaving scientific decisions under the researcher's control.

Designing a graph that preserved both successful reasoning and discarded approaches also proved surprisingly difficult. And we crucially chose to represent failed reasoning as explicit graph nodes instead of deleting it, allowing future investigations to reuse previous work rather than starting over.

What we learned

Building Pico Probe changed how we think about AI assisted research.

Initially, we believed the difficult problem was orchestrating multiple AI models. Instead, we discovered that the real challenge was preserving research pathways and verification; in fact, there are already many tools to simply orchestrate research, and that is why we went a step further.

Connecting APIs is relatively straightforward, but designing an architecture that preserves math dependencies, provenance, verification history, and reusable research knowledge is much harder.

We also learned that successful AI systems need memory beyond chat history. Scientific progress depends not only on successful ideas but also on failed hypotheses, discarded proof strategies, counterexamples, and unexplored directions. Preserving this negative knowledge makes future investigations more efficient and transparent.

Perhaps most importantly, we realized that language models are only one component of a much larger research framework. Symbolic mathematics systems, theorem provers, numerical simulations, literature search, and human researchers all contribute different forms of evidence. Pico Probe is designed to coordinate these components rather than replace them.

What's next for Pico Probe: A Multi-Model Math Research Pipeline

The current version establishes the foundation of the platform, but many of the most exciting capabilities are still ahead.

Future work includes collaborative research projects, GitHub synchronization, automatic pipeline optimization, distributed execution across cloud and local resources, improved formal verification through Lean and Coq, deeper symbolic mathematics integrations, cost-aware scheduling, and reproducible research package generation.

We also plan to expand beyond mathematics into other scientific disciplines where investigations that require coordination between multiple AI models, external tools, simulations, and formal verification will be aided.

Our long term vision is not to replace researchers, but to give them a new kind of research environment where every idea, computation, proof attempt, counterexample, and verification result becomes part of an inspectable and reproducible scientific record. Instead of ending with a final answer, our mission is to preserve the complete reasoning process, making AI-assisted research transparent, verifiable, and extensible.

Built With

Share this project:

Updates