Current papers

What the papers establish

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 partial results, failed or equivalent routes, finite evidence, and the exact obligations that survive. If the problem numbers or formalisation are unfamiliar, read a reader’s way in first. For the design of the tools and the research process, go to the project papers.

Problem papers

#68 · #243 · #249 · #251 · #257 · #269 · #1041 · #1049

Reading the eight together

One cross-problem paper develops the mathematics that arises from reading the programmes together. For $c>0$ and integers $d\ge 1$, it considers entire functions $f(z)=\sum _{n\ge 1}{e}_n{z}^n/n!$ with nonnegative integer $e_n$ eventually bounded by $n^c$ and, for each fixed positive integer $q$, eventually divisible by $q$. The set of derivative-value vectors at $1$ has Hausdorff dimension $min(c,d)$ and contains an open set exactly when $c>d$. This result has an ordinary proof with the formal ingredients identified separately. The paper also contains the capacity and congruence criterion, Lambert-subsum results, exact computations and method limits.

Reading Eight Erdős Problems Together (source).

Follow the argument into its evidence

Read the assumptions of the result you want to use, then the proof. The longer record gives the surrounding working context, including routes that failed, finite experiments and open obligations. If you cannot reconstruct a step or find its source, that is useful feedback through Contributing.

Some results are checked in Lean; others are ordinary mathematical arguments or applications of cited external theorems. Each paper states the boundary for its own claims. Results and limits gives the result beside what remains open, and the source map connects the paper to supporting declarations. Lean files are proof authority only for the exact declarations they check; docs/claims.json records the selected public claim interfaces.

The full-text index provides generated Markdown versions for browsing. The PDFs and .tex files above are the authored manuscripts. The older joint #249/#257 paper is retained for provenance; it is not the entry point for either problem.

Project papers

Start with A Repository-Based System for Research and Publication (source). This is the main systems paper: it follows a result from its mathematical argument through formal support, written explanation, review and contribution.

The accompanying writing guides describe the exposition process: Writing a Good Mathematical Paper is the compact guide; Writing Mathematics from the Literature and Reviewed Revisions records the method and its sources. Their LaTeX sources are in exposition/.

For current use, follow the reading guide, agent instructions or Contributing.

For the repository layout, sources of truth, build path, and release infrastructure, see docs/ARCHITECTURE.md.

Sources and earlier manuscripts

The manuscript layer (the .tex sources and rendered PDFs) is licensed CC-BY-4.0; see REUSE.toml at the repository root.