PlectisWorking with a coding agent
Most commands on this site will be run by an agent, not typed by a person. This page is the path for that.
The third reading form
Plectis reads in three forms. The pages here are for people. The AI packet is for a chat assistant: a reading starter with selected paper text, READMEs, video transcripts, website introductions and links to the complete public sources (the reviewer brief is the navigable public source: paper LaTeX, assertion rows, glossary terms, per-problem Lean and Comparator paths, component records, and the site map). The repository itself is for a coding agent: an AI that works inside a folder of files rather than a chat tab, such as Claude Code, Codex, or Cursor. Opened inside the repository, the agent reads the source, runs the components, and checks the result records directly: the same loop this site describes, executed rather than narrated.
The path
No git knowledge is assumed, and nothing here needs typing into a terminal: the agent performs the clone and runs the commands itself.
- Install a coding agent. Claude Code, Codex, and Cursor each install from their own documentation; any agent harness that works in a local folder fits.
- Give it the prompt below.
- Ask in plain language from there.
My task is [describe the question or change]. Start with the relevant project at https://wcook04.github.io/practical-formal-verification/ and follow its code link to the project’s own repository. For the mathematics, use https://github.com/wcook04/plectis-erdos and follow its links to the computer-checked Lean proofs. The older https://github.com/wcook04/practical-formal-verification repository is a separate toolkit, not the source of every project. Clone only the repositories this task needs from current main and preserve existing local work. Read README.md and AGENTS.override.md or AGENTS.md where present. Follow that repository’s setup and checks. Record the checkout commit and local changes. Return the source paths, exact commands and outcomes, and any assumptions or unfinished steps. Say clearly when you could not run a check. A release tag is a frozen edition, not current main.Choose the repository for your task and start from its current main branch. Record the commit and preserve existing changes; release tags describe frozen editions. Follow the software agent quickstart or the mathematics agent quickstart. Each names the compact agent entry, commands and expected result.
After an agent says done
When an agent reports it is done, check the claim against the record it left. Ask what files the agent claims it touched, what validation output exists, whether the repository state changed before a commit claim, what blockers remain, and where the claim stops.
Clone https://github.com/wcook04/practical-formal-verification and open it. Read AGENTS.md and README.md, then inspect the coding-agent residue path: Durable Agent Work Landing Replay, Agent Completion Faithfulness Audit, and Bridge Phase Continuity Runtime. Find the first completion or resume claim that would create false confidence if its evidence were missing.What the agent finds
The repository gives the agent the same material this site projects, in runnable form: the component source under src/, the fixtures each component runs against, validators it can execute, result records accumulating in .microcosm/, and the same scope limits the site prints. The command blocks across this site are written so an agent can execute them verbatim; the quickstart is the usual first request.
Same evidence rules
Ask the agent to compare a statement on this site with its linked source files and recorded test results. Its report should say exactly what those files establish and what remains unresolved. Reading a saved test result does not rerun the test.