Prompts

Reusable prompts and skills for automating research in theoretical cryptography. Each one is a single Markdown file: download the raw source and paste it as a system or instruction prompt, alongside whatever .tex or proof you want it run against.

Research

Multi-agent harness for attacking an open conjecture — an architecture of role-separated agents (Scout, Strategist, isolated Provers, Refuter, blind Verifiers, Triage, Reviser, Formalizer, Weakener, Lifter, plus a persistent Ledger) built so errors decorrelate and no agent can see the reasoning trace behind the result it’s checking. Motivated by the finding that in the largest published sweep of agent-claimed proofs of open problems, only 6.5% were meaningfully correct (Feng et al., Towards Autonomous Mathematics Research, arXiv:2602.10177, Section 4.2: of 200 gradeable responses, 137 were fundamentally flawed and a further 50 were technically valid but vacuous, leaving 13) – most failures were a valid proof of a weaker or different statement. Includes the problem-contract template, the retreat/weakening protocol for descending to a provable special case, and file-based persistence so state survives across sessions rather than living only in a conversation.
Harvesting conjectures from a paper — a three-call prompt for reading one paper and coming back with the open problems it poses, built around the fact that asking a model for open problems succeeds every time and that this is the difficulty rather than the feature. A model reading forty pages will hand back a strengthening of a theorem the paper proves, or a question the authors settle in Section 6, or a synthesis of two remarks nobody has posed, and all three read exactly like the real thing. So the prompt is not asked to be careful, it is asked to be checkable: every candidate carries verbatim quotes with page numbers, one for the statement and one for the fact that it is open, and scripts/harvest_conjectures.py then matches those quotes against the PDF’s own text layer — undoing ligatures, hyphens broken across lines and curly quotes first — and drops any candidate whose evidence is not in the paper before a line is written to disk. That check is mechanical and cannot be talked round; it is calibrated to pass a verbatim span whose mathematics the extractor mangled and to fail a paraphrase, which is the distinction the whole thing turns on. A second call then refutes the first, deliberately without seeing its reasoning, against eight named checks (existence, openness, strength, quantifiers, attribution, definitions, fabrication, self-containment), with the burden on the draft: for openness, “I could not confirm it” is a failure and not an uncertainty. A third renders the survivor as statement.tex and is forbidden to change any mathematics at all. Includes the selection criteria for what makes a conjecture worth a page (a problem rather than a programme, an obstruction the paper names, stateable in a page) and the rejection list for what is not (engineering left as future work, security assumptions dressed as conjectures, extending to \(k\) parties where the paper gives no reason it is blocked).
Filling one UC functionality stub — a prompt for taking a single page of this site’s UC functionality encyclopedia from a title and a bare reference list to a finished entry, in six stages of which the middle two are the point: work out which of the papers the page already cites actually prints a definition of this functionality, decide which of those definitions is the current one, capture it as printed so the transcription can be checked against the original rather than trusted, then rewrite it as code in the interface-box conventions of UC for Gamers. The mechanical half — fetching each cited paper, taking the newest ePrint revision, finding the pages that carry a box named after the functionality, rendering them to PNG in the entry’s own folder — is delegated to scripts/uc_source.py, so the prompt spends its attention on the choice. That choice is made in a fixed order (is it even the same object; then revision, formulation and framework currency, which are three different things; then a tie-break ladder ending at the encyclopedia’s own consistency) against the hard constraint that newest is not the same as current. Built around the fact that most UC functionalities have been defined several mutually incompatible ways: it must name the variants, pick one explicitly, and record every place the source does not fit the house conventions in a mismatch register — leakage interfaces the source never had, delayed output that is not the same as a responsive call, “and halt” that hides a one-shot assumption, “ignore subsequent calls” that hides a re-entrance question. Hard constraints forbid inventing an operation, inventing a citation, citing a revision you did not read, or blending two papers’ variants into one box. Output is the .tex fragment scripts/gen_interface.py consumes plus the page’s prose, never hand-written HTML.

Proof checking

Prompts for auditing a finished proof adversarially: the model’s job is to find where an argument breaks, or to certify that it tried and could not, never to summarize or praise.

Idealized-model proof audit — a system prompt for auditing proofs in the random-oracle, ideal-cipher, and generic-group models, tuned for probability-heavy arguments: presampling and auxiliary input, concentration inequalities, martingales, communication-complexity reductions, and randomness extraction. Runs a staged protocol (pin down the exact model variant, build the lemma dependency graph, check independence/conditioning, attempt an explicit attack, classify every issue as FATAL/GAP/FIXABLE/COSMETIC) against a long subtlety checklist, and outputs a findings table plus inline \aicomment/\aifix/\aiwcfix LaTeX annotations. Ships with a list of verified reference anchors for the techniques it checks against.
UC security-proof audit — a composite protocol for auditing universally composable security proofs (UC/GUC/UCGS/JUC/iUC/GNUC/IITM/SUC), merging a read-only, non-inventive extraction pass with staged, adversarial auditing and an independent-baseline verifier. Fixes a five-way verdict vocabulary (ERROR/GAP/CONVENTION/UNVERIFIABLE/QUESTION), forbids silently repairing a step to make it work, and includes the full staging, scoring rubric, adjudication procedure, and a LaTeX sidecar variant for running it directly against a manuscript.

Writing

Prompts for turning a working LaTeX draft into a submittable one, split by concern: typesetting hygiene versus prose quality, so a single pass never has to judge both mathematics and grammar at once.

LaTeX stylistic and typesetting audit — a copy-editor/compositor prompt that produces a defect report, not a rewrite: orthography, punctuation, spacing, cross-reference and bibliography consistency, and TeX source hygiene for IACR/AMS/ACM/LNCS-style manuscripts. It explicitly does not judge correctness, novelty, or persuasiveness — every finding must carry a file, a line number, and a verbatim excerpt, or it’s suppressed. Configure via a filled-in header (project root, document class, target venue, US/UK spelling, house style overrides, scope) before pasting.
Restrained typographic pass over a LaTeX document — a compositor’s prompt rather than a copy-editor’s: where the audit above only reports, this one changes the typesetting. Configured through a header (engine, document class, whether the class is yours to alter, target venue, whether font changes are allowed) and fenced in by hard constraints — not one word of prose or symbol of mathematics changes, the page grid is frozen under a publisher’s class, no coloured headings or boxed theorems or drop caps, and the document must still compile with no new warnings. Work proceeds in tiers, smallest first, each judged against a recorded baseline of page count and overfull/underfull counts: page level (measure, leading, widow and orphan penalties), then safe defaults (microtype, csquotes, booktabs, a mathematics font matched to the text font), then local repairs — tables of symptom-to-fix one-liners covering en dashes, false sentence spaces after e.g., eqnarray, \left(...\right) in inline math, vertical rules in tables, [h!] float placement. The closing self-check is the test the whole thing is built around: would a reader notice anything other than that the pages read more easily? If so, that change is too loud, and it gets reverted.
Revise a LaTeX manuscript for quality of writing — the current, fuller version of the prose-revision prompt: every edit is tagged with a rule ID traceable to a published style authority (not the reviser’s taste), under hard invariants that forbid changing mathematical content, repairing a suspected error instead of logging it, renaming a \label, or introducing an em dash. Adds a mandatory proof overview, numeric length targets, a mechanical-sweep section for the checks a linter would normally catch, and a conflict register for where two cited authorities disagree.
Revise LaTeX prose (earlier version) — the original, shorter version of the same prose-revision prompt, before the length targets, mechanical sweep, and conflict register were added. Kept for comparison; use the manuscript version above for new work.

Publishing

Prompts for turning a finished artifact into something the site can host, where the risk is not that the job fails but that it succeeds visibly and fails invisibly.

Convert UC for Gamers to HTML — a staged conversion prompt for a heavily customised LaTeX book, built around the observation that a converter will emit a readable page while flattening a numbered interface box, restarting its line numbering, or turning a resolved cross-reference into [?], none of which a reader notices without the PDF beside them. Forces the target to be chosen before any toolchain is installed (a faithful mirror of the whole book, or excerpts, which the repository’s own gen_interface.py largely already solves), then a two-converter bake-off on a single representative box scored on five checkable questions, then a hybrid that splices the existing generator’s output over the converter’s for the constructs it handles better. Acceptance is measured against the compiled PDF: heading order, resolved-reference count, printed line numbers, and an explicit accounting for every diagram. Ships with the document’s actual measurements, including a correction to an earlier note that overstated its \hypertarget use.

Contributing

Open a pull request that adds a Markdown file to prompts/ and a bullet to the matching section above.