1.Introduction

Paul Erdős posed hundreds of problems in combinatorics, number theory, and graph theory over the course of his career. Many remain open. The Erdős Problems catalogue, maintained by Thomas Bloom, documents over 800 such problems, ranging from elementary conjectures to deep structural questions at the frontier of modern mathematics.

The emergence of frontier language models with strong mathematical reasoning capabilities raises a natural question: can structured AI-assisted reasoning yield progress on these classical open problems?

1.1 Motivation

Traditional approaches to Erdős problems rely on individual insight: a researcher recognizes a connection to Ramsey theory, or discovers that a probabilistic argument yields an unexpected bound. These moments of insight are difficult to systematize. However, they can be decomposed. A proof of a combinatorial bound typically involves (i) selection of a proof strategy from a known family, (ii) instantiation of the strategy with problem-specific parameters, and (iii) verification that all steps are logically valid.

Nanometers exploits this decomposition. Rather than replacing mathematical intuition, the system creates a structured environment where multiple AI reasoning strategies are applied in parallel, compared for correctness, and synthesized. The key observation is that different models exhibit complementary strengths: one may excel at rigorous ε-δ\varepsilon\text{-}\delta arguments while another discovers creative constructions via the Lovász Local Lemma or the probabilistic method.

1.2 Scope

This project restricts attention to Erdős problems in three areas:

  • Additive combinatorics: sum-free sets, arithmetic progressions, sumset bounds
  • Extremal graph theory: Turán-type problems, chromatic numbers, forbidden subgraph densities
  • Ramsey theory: partition regularity, Hales-Jewett extensions, hypergraph Ramsey numbers

Problems involving deep analytic number theory or algebraic geometry are out of scope, though the harness architecture is extensible. Each problem is processed through a pipeline that produces a candidate proof, a partial result improving known bounds, or a novel construction illuminating the problem structure. All outputs are submitted for formal verification in Lean 4.

1.3 Notation

Definition1.1(Standard Notation).

Throughout this document:
  • [n]={1,2,…,n}[n] = \{1, 2, \ldots, n\} for n∈Nn \in \mathbb{N}
  • (Sk)\binom{S}{k}: the set of kk-element subsets of SS
  • O(⋅),Ω(⋅),Θ(⋅)O(\cdot), \Omega(\cdot), \Theta(\cdot): standard asymptotic notation
  • L\mathcal{L}: the space of natural-language mathematical arguments
  • Π\Pi: the space of well-formed Erdős problem statements
  • Λ\Lambda: the space of well-typed Lean 4 terms

1.4 Related Work

AI-assisted theorem proving has seen significant progress in recent years, from neural theorem provers operating within formal systems (AlphaProof, LEGO-Prover) to natural-language reasoning systems. Nanometers occupies a distinct position in this landscape: it uses frontier language models for conjecture attack in natural language, then delegates verification to a type-theoretic system. This two-phase architecture separates the creative and verificational aspects of proof discovery, allowing each to be optimized independently.