PlectisReading and working with the research
The front page introduces the project. This index helps you choose what to read or do next, whether you want to understand a result, check its proof, continue the research, or inspect how the tools work.
Using the degree-seven polynomial constructed by the erdosproblems.com contributor ani, Lean proves that every preconnected strict-lemniscate set containing two distinct roots has one-dimensional Hausdorff measure greater than two. This refutes the exact Formal Conjectures path-image-length statement; the separate total-variation bound is also checked. The other seven targets remain open. Independent human review of correspondence with the 1958 wording has not been recorded. Comparator checks only selected exact statements, axioms and kernel acceptance; it does not assess novelty or historical correspondence. The papers report intermediate results and the approaches that stopped, with enough of the record preserved for somebody else to inspect the argument and continue from it.
Choose a way in
| What you want to do | Start here | Where it takes you |
|---|---|---|
| Understand the project without installing anything | A reader’s way in | The eight questions, what formalisation adds, and how to read the evidence. |
| Read the mathematics | The papers | A short paper for each problem, then a longer record when you need the details. |
| Read the comparison across problems | The cross-problem paper | Capacity and congruences, Lambert subsums, method obstructions and their full research record. |
| Find what has been established and what is missing | Results and limits | The results beside their remaining open questions, with routes to the evidence. |
| See what is open and what would settle it | The argument graph | Every conditional theorem read out of the Lean kernel: what is proved, what reduces to what, which open statements are the same problem in other coordinates, and what a missing input would settle. |
| Check a result yourself | Reproducibility | Inspect one claim without Lean, then install the pinned environment if you want to rebuild proofs. |
| Continue the work or send a correction | Contributing | A plain-language issue or a focused pull request, with evidence and credit. |
| Understand the software and research process | How this repository works | The roles of proofs, claim records, papers, query tools and release checks. |
Read
Choose a statement in a short paper. Read its assumptions and argument, then use the longer record for a compressed step, an earlier attempt, or the surrounding computations. Prior work helps with attribution; related problems follows connections elsewhere in the collection.
The source map locates the supporting Lean declarations and paper passages. Each paper says which results have a Lean proof and which use an ordinary mathematical argument or a cited theorem. The claim record gives the selected public statements, their status and their exact remaining-open propositions. Scope records the release boundary, and methodology explains the rules for changing a claim.
Check
To replay a check, follow reproducibility. For selected statements, external verification also provides Comparator interfaces: separately declared formal statements that can be compared with the development. The verification guides explain those checks and their limits.
Contribute
A contribution can be a correction, clearer explanation, earlier reference, counterexample, or useful failed approach. Contributing explains what to send back. The research commons describes how longer investigations retain their starting point, evidence and credit.
For an AI-assisted session, use the research-shift guide. Give a coding agent AGENTS.md so it can find the relevant workflow. The agent guides explain the tools once you have a question to work on. You can also contribute to navigation, validation or the contributor experience through the architecture contribution path.
Where things live
| Folder | What belongs there |
|---|---|
| Papers | Current PDFs and manuscript sources, grouped by problem. |
| Paper full text | Generated Markdown versions and the detailed paper inventory. |
| Agent guides | Query tools, proof tools and instructions for making changes. |
| Verification guides | Replay instructions, statement comparisons and submission requirements. |
| Technical reference | Research history, correction records and indexing details. |
| Research commons | Contribution, review and attribution records. |
| Semantic index | Technical navigation through formal statements and their recorded relationships. |
| Primary sources | Source provenance and redistribution records. |
| Measurements | Recorded measurements of the tools. |
| Release records | Audits and release identity records. |
The main reading guides stay directly under docs/. The
JSON files beside them supply the query tools and website. For example,
claims.json records public claim status and
methodology.json records review rules; the other indexes
help locate evidence. You can read the papers without opening these
files. Generated technical navigation is a
compact entry for readers who want to use the indexes.
Outside docs/, the repository map distinguishes the
proof libraries, manuscripts and working records. Folder indexes cover
experiments, returned research, tools and formal verification files. The naming
conventions explain why similarly named source and documentation
folders have different roles.
Files at the repository root
README.md introduces the work and
CONTRIBUTING.md explains how to help.
AGENTS.md is the shared entry for coding agents;
CLAUDE.md loads it for Claude Code. The detailed rules live
in the agent guide.
lakefile.toml, lake-manifest.json and
lean-toolchain configure the Lean project and pin its
dependencies. formalization.yaml is the Comparator manifest
for selected statements. CITATION.cff supplies citation
metadata; LICENSE, LICENSES/ and
REUSE.toml record the licences.
The code of conduct, security policy, CI and contribution
forms live under .github/. The privacy
policy stays here with the other guides.
Improving these guides
Give each guide a reader’s question to answer, and make its index link say what the reader will learn or be able to do. Define terms where they first matter, and check examples from the repository root. Keep mathematical hypotheses, evidence and open boundaries exact when changing the prose. For a generated page, change its source and run its owning builder; Contributing explains how to return the improvement.
Work on a paper joins the existing question, paper, source and return routes for every programme.