Getting started
What Plectis is
Plectis publishes Python programs and worked examples for research with AI, together with their source code, saved results and instructions for verifying those results.
What it is
The public toolkit includes programs for finding Lean proof premises, reproducing specified agent failures, comparing forecasts with outcomes, comparing generated files with their source, and recording unfinished work. These programs were taken from the private research system Will Cook built with AI coding agents. He sets the direction; the agents write and maintain code. The public repository contains the selected programs, examples and documentation. It runs independently of the private system. Older package names and the .microcosm/ output directory retain the project's former name.
The separate Lean repository contains mathematics papers, proof source, computations and records of attempted arguments. Its papers state which results have formal proofs and what remains unproved. The paper catalogue links to the mathematics papers and the papers about the software and research process. Published papers can be opened as PDFs.
The Quickstart gives commands for downloading the toolkit and running the project tour. The tour lists files, suggests predefined commands and records a simulated task run in .microcosm/; it does not execute the project's tests. To run an individual component, use the command on its page. A coding agent can read the repository's AGENTS.md, run those commands and explain the resulting files. These local examples do not call a model provider.
Components and their results
There are eighty-eight components in seven areas. A component groups the files and documentation for one task. Its page identifies the source files and any example inputs, commands and saved results. Some examples execute a computation or an external tool; others compare supplied records against rules or check exported files. Some entries provide documentation without a runnable example. A passing result means that the particular input passed the named test. The evidence guide explains these differences and what each kind of result establishes.
Rules for programs and generated documents
The rules require programs to calculate a verdict from the supplied evidence, make the validation procedure runnable, and report missing evidence as a failure. If a computation cannot produce a justified result, it must report the reason. Results must identify their sources, displayed counts must have a way to recompute them, and generated documents must agree with their source files. The Doctrine page lists these rules and the principles behind them.
The seven areas
The areas below group programs by task. The architecture page explains their shared command handlers, registries and project records.
- Entry and orientation provides the project tour and instructions for running a first example.
- Architecture and navigation contains the project data model, component index and command-selection code.
- Import and drift control records copied files in a manifest, calculates their digests and reports differences from the originals.
- Work and continuity records completed work, resumes paused runs and coordinates programs writing to shared files.
- Agent reliability and safety reproduces specified cases of sandbox escape, prompt injection, poisoned memory, sabotage, unauthorised tool use and benchmark manipulation. These prepared examples do not establish the safety of a deployed agent.
- Formal math and proof includes premise lookup, tactic selection and proof-error analysis. Some components, including the Lean example, run Lean on a small supplied proof; others validate stored records.
- Research and science uses synthetic data to demonstrate replication reports, forecast evaluation, circuit-attribution records and financial forecast calculations. These examples do not establish scientific findings or investment performance.
Run an example
Follow the Quickstart to run the project tour. For an individual program, open its component page, read the input description, then run the listed command. Compare the output with the expected result and read the stated limitations. The repository contains the source files used by these examples.