Repository overview

Mathematical research and the system behind it

Plectis collects research on eight problems posed by Paul Erdős: papers, Lean proofs of selected statements, experiments and failed approaches. The aim is to make AI-assisted research easier to understand, check and continue.

Explore the research · Read the system paper · Watch the videos · Open the maths map

Eight Erdős problem programmes: the interactive maths map connects papers, results and their formal evidence

_{The maths map on 9 October 2026. Open the image to explore the current edition.}

Plectis is an independent, AI-assisted prototype built and maintained by Will Cook. A reader’s way in introduces the mathematics without requiring Lean. The glossary explains project terminology.

Papers, tools and explanations

• Mathematics: eight short papers and longer research records.
• Research system: A Repository-Based System for Research and Publication.
• Writing and revision: writing guide, method and changes prompted by readers.
• Connections between problems: cross-problem paper.
• Formal evidence: Lean source and Comparator checks.

The mathematics website connects each problem’s papers, results and sources. The films also show private interfaces. Do not infer results from private or unreleased work.

For a first look: #257

Start with the introductory paper or #257 video: examples followed by a proof for infinite choices of exponents whose reciprocals have a finite sum. Erdős stated this result in 1968.

Problem 257 asks whether the series

$$\sum_{a\in A} \frac{1}{2^a-1}$$

is irrational for every infinite set $A$ of positive integers. The universal question remains open.

The short paper proves sufficient conditions for particular infinite sets, including a Lean-checked prime-weighted criterion that works at every integer base at least two. The proof cancels finitely many terms, then uses averaging to find a small positive remainder that rules out rationality.

Try three changed hypotheses, or follow the Lean declaration.

Results and their limits

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.

ani’s original counterexample is credited in the #1041 case study. Results and limits keeps each programme’s statements beside its assumptions, earlier work and remaining questions.

Watch the videos

• Plectis introduction: why I use AI to explain its research and software.
• The maths map: a tour from checked statements through research records and papers to explanations.
• Erdős #257 explanation: examples and a proof under Erdős’s reciprocal-summability condition; the unrestricted problem remains open.

Why keep the whole research record?

I want other people to work on these questions with me. The records preserve calculations and routes that stopped, which you can question, repair or reuse.

AI agents did most of the research and drafting. I built and directed the infrastructure and reviewed claims when I could; I have not independently verified every claim. I maintain the sources and take responsibility for correcting the public record. Novelty and significance need human judgement. Selected contributions have independent reviews; review does not cover the whole corpus. The system paper explains how the repository records results and corrections and credits contributors.

Problem papers

The short papers present results and arguments; longer records include calculations, failed approaches and unresolved steps. The results guide lists assumptions and sources. The reading edition collects paper openings.

What Lean and Comparator verify

Lean checks whether a proof establishes the exact formal statement written in its source. The source map connects paper passages to those declarations. Claim records list their public status and limits; prior art identifies earlier results and their relationship to this work.

Comparator checks a solution against a separately declared formal statement, with an explicit list of permitted axioms. formalization.yaml lists the selected statements. The verification dossier records selected statements across all eight problems and their replay requirements; it does not cover every argument in the papers.

Researchers judge correspondence with the intended mathematics, novelty and usefulness. A build or platform submission does not establish those judgements. Methodology explains the review required to change a claim.

Contribute

Ideas, corrections, references, counterexamples and clearer explanations are welcome. You need not solve a problem or write Lean.

• Mathematics or exposition: work on a paper or develop a method across problems.
• Software: improve navigation, checks or the contributor experience through the architecture contribution guide.
• A question or correction: use the research-progress form or email me.
• An investigation with your own agent: the frontier relay explains how to return the argument, evidence, limits and next question.

CONTRIBUTING explains returns without a clone. Accepted contributions receive a public evidence and credit record under the credit policy.

Read or verify locally

REPRODUCIBILITY starts with Git and Python 3.11+, then explains how to install Lean and check a proof. Its claim check inspects source links without compiling the proof. For research with an agent, see AGENTS.md and the agent workbench.

Corpus at a glance

The reviewed layer a mathematician should judge: 160 curated claim records in 38 contribution families, reaching Lean source through 478 principal declaration links. docs/SCOPE.md gives its shape and docs/RESULTS.md gives the strongest checked result per problem. The website and the papers are the human reading path.

The rest is engineering inventory. About 87% of the 164,639 declarations (142,668 across 695 modules) are machine-emitted certificate shards: one integer checked prime, one position excluded. The remainder is not all hand-written either.

Generated shards are counted as formal source and never as separate mathematical claims. Claim records cover every status, including cited and open, and are partitioned once. These are navigation counts, not novelty claims. They still need expert validation.

Following a result into Lean

The paper links each headline result to the relevant source. For a particular topic, start with the source map; it gives the module order without asking you to decode Lean declaration names first.

Formal Conjectures contributions

Five mathematical contributions have merged into Formal Conjectures. #6529 covers reciprocal-summable supports for integer bases at least two; arbitrary infinite supports remain open.

#6971 repaired four immutable proof links on 11 October. Bo Cowgill’s checks and Moritz Firsching’s approval concern maintenance, with proofs and statements unchanged and no new mathematics. Trace #1041.

On 12 October, Bo Cowgill approved #6579 using author-hosted verification, without an independent rerun. The request remains open with review required; the unreduced-totient problem remains open.

Nineteen receiving checks pass. Bo approved PR7260, PR6780 and PR7290–7294 using author-hosted checks without independent proof replay. All seven await required reviews.

Other checks: Prove2Me #243/#257 packets and plectis-erdos-lean.

Palomar checks Lean proofs and publishes registered results with their review comments. Our submission record distinguishes verification, editorial review and registration. The Palomar guide explains the local preparation checks; passing those checks alone does not establish acceptance.

The paper catalogue links versioned aiXiv editions; the verification guides explain submission and registry records. An archived edition may differ from the current paper.

Reading routes

Website → papers → research records and open questions

Credit

Some of the biggest changes here came from people telling me what was wrong. One mathematician’s comments on the #243 note led to all sixteen problem papers being rewritten for a first-time reader. The credit ledger lists each piece of advice, what it changed and the lines where you can see the change. Names stay withheld until each person confirms they want to be named.

Citation and licence

Use CITATION.cff and record the commit used. For a tagged release, use that tag’s citation file. For mathematics, cite the relevant problem paper and the original sources it uses. A repository citation does not replace the original author’s credit: prior art and source attributions distinguish earlier results, formalisation and local use.

Code, scripts and documentation are Apache-2.0; manuscript sources and PDFs are CC-BY-4.0. REUSE.toml records exceptions. See also scope, privacy and the code of conduct.