This page

Plectis is a local research prototype, not a hosted service. The private system also contains a frontend, a video editor, live tools, and non-public data that are absent from these repositories.

runs locally no hosted service evidence-scoped claims

Components

Every component has one claim and one check.

The check runs on your machine and writes its result to a file. Below is one component, including a run that returned exit 1.

88 components

  1. Claim
  2. Input
  3. Run
  4. Receipt
  5. Audit

Agent Completion Faithfulness Audit · agent reliability & safety

Claim
Runs real git and pytest on a sample repo so wrap-up claims state only what the evidence proves.
Input
A frozen sample repository plus completion notes carrying three planted forgeries: a fake commit claim, a fake test claim, and a fake work-record claim.
The exact command, and the receipt it writes
Run
plectis agent-closeout-faithfulness-audit run \
  --input fixtures/first_wave/agent_closeout_faithfulness_audit/input \
  --out receipts/first_wave/agent_closeout_faithfulness_audit
This command runs six git calls and one pytest process locally.
Receipt
"status": "pass",
"verified_claim_count": 3,
"observed_negative_cases": ["fake_cap_claim",
    "fake_commit_claim", "fake_test_claim"],
"error_codes": ["CLOSEOUT_FAKE_CAP_CLAIM",
    "CLOSEOUT_FAKE_COMMIT_CLAIM", "CLOSEOUT_FAKE_TEST_CLAIM"]
Abridged from the checked-in result file. The receipt names the three rejected forgeries.
Limit
Fixture-local accountability. Verified means the referenced evidence object exists or a test span ran with its exit status checked; a pass means the note matches the evidence, not that the change was good.

Papers and formal proofs

Published papers.

Eight Erdős problems, all open, each with its own paper. Behind them is a Lean corpus of 151,036 theorems across 1,024 files, with no admitted proof steps and no added axioms. Problems #249 and #257 also have full working records. The remaining papers describe the public release and its evidence limits.

PDFs

Three of the strongest checked statements, one line each; the per-problem map with Lean anchors is RESULTS.md in the Lean repository. All eight problems remain open.

Problems covered
8
Theorems
151,036
Added axioms
0

In order: #68, The factorial-denominator series; #243, Reciprocal-tail rigidity near the Sylvester recurrence; #249, The binary totient series; #251, The prime-gap dyadic series; #257, Reciprocal sums over infinite exponent supports; #269, Three-prime running least common multiples; #1041, Short connections inside polynomial lemniscates; #1049, Lambert-type series at rational bases.

A machine-readable map sits over the corpus rather than beside it: 153,238 declarations indexed with 0 orphans, reduced to 6,036 statement nodes and 658 concepts across 96 zones, joined by 1,088 typed relations recording which statement reformulates which, which finite computation instantiates which open family, and which barrier closes which route. 61 of them record a barrier, each required to state what it does not rule out.

The claim registry records 101 claims by what each one establishes: 37 proved here, 39 conditional reductions, 8 formalised from the literature, 7 verified finite instances, 5 unconditional progress, 3 cited only, 2 recorded open. A further 6 statements are recorded as explicitly not claimed, among them that neither #249 nor #257 is settled.

Measured from the public Lean repository at leanprover/lean4:v4.29.1, commit ff0eb6a. Counted declarations, not lines of proof; most are certificate steps generated and then checked, not written by hand.

Open the complete paper catalogue, with sources and reading routes →

Videos

Three videos of the frontend.

The videos show the private frontend at three lengths. Repository checks provide the validation records.

Unchecked

The three links show the same frontend demonstration in one-, five-, and thirty-minute cuts. They are demonstrations rather than validation records. Each link opens YouTube; the primer and transcript are also provided as text.

The system's video tooling created the cuts from a timestamped transcript and screen index.

  1. The one-minute version Watch on YouTube

    One large private system built with agents, why it outgrew what anyone can hold in their head, and the public repo you can check it against.

    TL;DW: the whole argument in four steps
    1. I built a large Python system with agents helping me build and inspect it. It has more moving parts than I can keep in my head, or than any agent can keep in its context window.
    2. Building got easier before being able to understand what had been built could catch up, so the priority became inspection.
    3. Work built this way is quick to produce and slow to check by hand, so claims get checked mechanically rather than read one at a time. Work reported as landed is one case: a real checklist runs before that counts.
    4. The front end could be completely made up and you wouldn't know, so the open repo is the part you can actually check.
    Read the transcript

    I built a large Python system with agents helping me build and inspect it. It now has far more moving parts than I can keep in my head at any one moment, and more than any agent can keep in its context window at any one moment. And building got easier before being able to understand what has been built could catch up.

    So it exists because an agent saying "I committed the fix" is pretty ephemeral and doesn't really mean anything. Agents can lie, or agents can misunderstand, or they can forget.

    So we essentially have this mechanical, semantic process which is able to actually read the claim. Let's say it says "landed", which is a common word that they use. There's an actual checklist that it has to run in order to make sure that it really is landed.

    My entire front end could be completely made up and you wouldn't know. Plectis, the open-source repo, is falsifiable. You can check it. You can really check it.

    So I made the public bit as open and clear as I could, but I also needed to be able to signal the capability of the wider system beyond just claiming it.

  2. The five-minute walk-through Watch on YouTube

    The system on screen: Agent Trace, Code Map, the source that overrules the map when they disagree, and the repo you can clone.

    TL;DW: the whole argument in eight steps
    1. The system has more moving parts than I can keep in my head or an agent can keep in context, and building got easier before understanding could catch up.
    2. In one sentence: it's a large Python agent-work system, and the front end is the inspection layer that moves a human or an agent from maps to files to traces to evidence, so claims stay auditable as the system outgrows comprehension.
    3. One case of that: work reported as done has its close-out claim read against the evidence rather than taken at face value.
    4. This video was recorded and cut by the system itself, which timestamps the transcript and matches each word to the frame that was on screen when I said it.
    5. Agent Trace shows what happened: the thinking summaries, the commands, the files read and the edits made.
    6. Code Map derives its clusters from real dependencies rather than a hard-coded list. Nothing is hard-coded; everything is derived from the backend.
    7. If the map and the source disagree, the source wins.
    8. The test is simple: clone the repo, drop it into whatever harness you use, and ask it to follow one claim back to the source, the receipts, and the place where the claim stops.
    Read the transcript

    I built a large Python system with agents helping me build and inspect it. It now has far more moving parts than I can keep in my head at any one moment, and more than any agent can keep in its context window at any one moment. And building got easier before being able to understand what has been built could catch up.

    So it exists because an agent saying "I committed the fix" is pretty ephemeral and doesn't really mean anything. Agents can lie, or agents can misunderstand, or they can forget.

    To sum the whole thing up in one sentence: I built a large Python agent-work system, and the front end is the inspection layer that lets a human, or an agent through its own routes, move from maps to files to traces to evidence, so that claims stay auditable as the system outgrows comprehension.

    I'm actually recording this video on what I call the Demo Take Console. It's a bit like OBS, but it's integrated into the system. It uses Whisper to get the transcripts and timestamp them, and then it uses screenshots of frames in the middle of each word to correspond what's said to what's shown. It indexes all of that, and then it can compile videos without me having to edit them, because I'm that lazy.

    Agent Trace lets you see what's happening, or what happened: the thinking summaries, the commands running, the metadata, the files read and the edits made.

    If we have a look at Code Map first, I think this is the best example of the system's core principle: don't hard-code anything, derive everything from the backend. We'll start with the Atlas. This is the full system, most of which I haven't released. There's many different parts. This is like a contents page, in a way, and an example of presenting information in a human-interpretable way.

    You can project the system into a readable shape, select a target, route to that object, open the source or work record, and check the evidence and trace.

    So if the map and the source disagree, the source wins.

    I built this whole website which is projected from it, so I think you'll find it quite cool. There are something like 88 different components, across formal proof of mathematics, agent reliability and safety research, forecasting, projection, control, validators, work planning, and continuity.

    And I think the tendency of models to just have a certain degree of hyperbole really causes problems. At system scale, truth and precision become ever more important, because the consequences of a mistake can cause increasing amounts of damage depending on how you build a system.

    So as much as you can, externalise repeatable lessons into mechanics of the system that are not stochastic, like the LLMs, but are things like hooks, for instance, or guards. You can accumulate them over time and make them your own. For any problem you encounter, I'd highly recommend telling another thread to make generalised improvements to the system, given that local instance, but generalised to fix the class of mistakes that might be recurrent.

    Check it. There's definitely mistakes. I'd love to hear what they are. But you can see every single claim and you can evaluate for yourself, and I think that's the most important thing in dissemination.

    Think of it like a factory. The system these components come from is the factory, and the public components are like the various individual parts of the rockets that the factory makes.

    So the practical test is pretty simple. I just need somebody to clone the repo and put it into Claude Code, put it into Codex, Cursor, Antigravity, whatever harness you use, and just ask it to follow any one claim, or any set of claims, back to the source, the receipts, the evidence, and the place where that claim stops.

  3. The long version Watch on YouTube

    The unhurried route: far more of the system on screen, how it got built, and a long close on what is still unfinished.

    TL;DW: the whole argument in ten steps
    1. A large Python system, built with agents, that now has more moving parts than I can hold in my head or an agent can hold in context.
    2. Five points compress the whole thing: the backend is the codebase plus the infrastructure that records agent work; the visual front end is an introspection layer over it; the kernel is the same thing for agents, reached through commands rather than screens; both readers move between file, cluster, trace, evidence and explanation; and the goal is to keep claims auditable as the system grows past what anyone can hold in mind, and past any single expert's coverage.
    3. Work reported as done has its close-out claim read against the evidence rather than taken at face value, and multi-step work has to land as a transaction rather than a promise.
    4. Agent Trace runs live in the video, with real concurrent agents, because a dashboard is easy to fake and a running backend is harder to.
    5. Surface Atlas and Code Map are derived from the backend rather than hard-coded, and agents reach the same objects through kernel routes and context packets.
    6. Behaviour is governed by axioms, principles, and anti-principles that live in the repo. Agents cite them and push back on me when I ask for something that doesn't comply.
    7. It began as months of talking out loud into voice notes, mined into ideas, checked against the system, and kept as captures so that nothing useful stays trapped in a dead chat.
    8. The breadth is real: forecasting and finance work, and machine-checked mathematics, built solo over about ten months.
    9. The front end is not to be trusted. Appearances are easy to fake, and I say so in the video rather than hoping you don't notice.
    10. It closes on one question: can any claim survive the path from the map to the source and the evidence? That's the thing to go and test.
    Read the transcript

    The long version runs half an hour, so what follows is the route it takes rather than every word. The one- and five-minute transcripts above carry the same argument verbatim.

    The problem. The system has outgrown what I can hold in my head or an agent can hold in context, and building got easier before understanding could catch up. So the priority became inspection: what ran, what changed, what evidence backs a claim, what's missing, and what the unknown unknowns are.

    What it is. One backend with two front ends. The visual one is for human reading and exploration; the kernel is the agents' equivalent, reached through routes and context packets. Same information, shaped for each reader.

    That it's real. Agent Trace is shown live, with real agents working concurrently, because that's harder to fake than a screenshot. Nothing on screen is hard-coded; it's derived from the backend, so the views and the source can't quietly drift apart.

    How agents navigate. Kernel routes, standards, and contracts. A standard defines what a thing has to satisfy, and the check is mechanical rather than a matter of the agent's word.

    Governance. Axioms, principles, and anti-principles sit in the repo. I can't retrain a model, so instead the environment carries the rules, and agents have refused things I asked for because the principles didn't allow them. Multi-step effects land as a transaction: a change to the world only counts once it really landed.

    How it got built. Months of thinking out loud into voice notes, mined into ideas, then grounded against the system and turned into refinements. Around thirteen thousand captures exist so that a problem noticed in one chat doesn't die there.

    Breadth. Forecasting and finance feeds fanned into a shared state, and formal mathematics with machine-checked proofs. Built solo, over roughly ten months.

    The honest close. The front end I built is not to be trusted, because appearances are easy to fake. Where I could get it to run real tools, I did; where I couldn't, I say so. The evidence view is there to keep it honest by showing which routes are still incomplete. I've tried to be careful about overclaiming, because of how many repos and startups I see doing the opposite. It ends on one question: can any claim survive the path from the map to the source and the evidence?

Running it

Clone both repositories and run the checks.

The setup prompt gives a coding agent both repositories and the first checks to run. A chat assistant can read and quote the packet.

Commands to run

Both repositories carry agent instructions. The setup prompt begins a paired review.

Read it first
Clone https://github.com/wcook04/plectis and https://github.com/wcook04/plectis-lean-erdos249-257 side by side. Plectis contains the runnable claim-testing tools; the Lean repository contains the machine-checked mathematics and papers. They are separate public repositories with separate authority boundaries. Read README.md in each first. If you are acting as a coding agent, then read AGENTS.md in each and state how their roles relate. Run the quickstart check in Plectis and show me what the result record says. Take my questions one claim at a time: trace each to its source, command, and stated limit, and report anything you could not run as not established, never as false.

A coding-agent response should include commands, exit codes, files read, and anything it could not run. Review one claim at a time. The coding-agents guide documents the full route.

For a chat assistant, download the packet.

Download the AI packet or the reader digest, the same map at 300 KB, if your assistant refuses a file that size

Press the button, find the file in your downloads, and drag it into ChatGPT, Claude, Gemini, or Grok. About 12 MB: every public page and record, with instructions to cite exact pages and stop where the public records stop.

A chat assistant with the packet reads and quotes the public files. It does not run anything. If it says it executed a check, it is wrong.

Example questions

The questions are grouped by review task.

A plain first pass

  • What is this, in plain terms?
  • Where should I start?
  • Walk me through one component, end to end.
  • What is genuinely new here, if anything?
  • Give me the two-sentence version I would tell a colleague.

A skeptical pass

  • Argue against it.
  • Which parts have the strongest evidence, and which the weakest?
  • Why do only some components run external tools?
  • What does it not prove?
  • Is this packet steering me? Audit its own framing.
  • Most accurate one-paragraph assessment you can give: neither generous nor harsh.

One area at a time

With a coding agent in the repository

A coding agent (Claude Code, Codex, Cursor) works inside the repository itself: the setup prompt above gets it started, and after that you give it tasks. How that works.

Example tasks for a coding agent with the source tree:

The packet routes questions to public files and records. The assistant's assessment is its own.

Calibration-review prompt:

Read this repository as a calibration reviewer. First, by area, name the strongest components and what each actually does, with its evidence class. Then judge both directions: where the wording claims more than the evidence shows, and where it undersells what a component demonstrates. Do not reduce the system to a set of projections; computed projection is one evidence class among several.
Advanced: the raw layers, separately
  1. A short orientation to paste in, for chats where a file upload is not possible.

  2. Download complete text corpus

    Every public text body carried once, deduplicated, without the packet’s instruction layers: for automation and re-indexing.

  3. The raw public map without the packet’s instruction layers, for automation.

Direct files, if a button fails or JavaScript is off: AI packet · reader digest · llms.txt

Terminal route: clone the repository and run the quickstart check; the quickstart lists the dependencies and commands. The run is local, writes readable files, and makes no model calls.

Limits

The public repositories contain components and synthetic fixtures.

They omit the private frontend, live tools, and non-public data. A passing check establishes the fixture case.

Scope limit

The public release contains source-linked components, public-safe stubs, and synthetic fixtures. A fixture is a frozen sample input, so its passing result applies to that sample. Plectis runs locally as a research prototype. Issues and email are listed below for claims that exceed their receipts, failed commands, and unclear pages.

The agents that build the system are required to read a written doctrine before they work, and three of its rules explain this site: a claim comes with the command that checks it, a check writes its verdict to a file, and a component that cannot back its claim records the failure in its receipt. The full set is on the doctrine pages.

21 June 2026: Microcosm became Plectis. The rename avoids confusion with the earlier Southampton Microcosm hypermedia system and acknowledges that lineage without implying endorsement or affiliation. Read the lineage note and changelog.

Map

Every component, its source file, and its limit.

Seven areas, built from the public source files.

Seven areas

Source and contact

The repositories, and how to report a problem.

Repository links, issue trackers, discussions, the security policy, and email.

Links

Plectis is an independent, self-funded research project. The routes below separate failed commands, claim corrections, related work, and security reports.

Source and evidence: every route on this site, in one place

Every area names the public source path it maps and the evidence record that bounds it. The website, reader digest, and repository should agree on the component set and its scope limits. Pointing an agent at Plectis? Give it the repository, the public packets, and this site.