Nanometers

We present Nanometers, a computational research harness for systematically attacking open problems in the Erdős problem catalogue. The system defines a pipeline $\Phi \colon \Pi \to \mathcal{L} \times \{0,1\}$ that maps problem statements to candidate proofs paired with machine-verified correctness bits. Two frontier language models operate in parallel: GPT-5.4 Pro (optimized for deductive arguments) and Claude Opus 4.6 (optimized for constructive and probabilistic methods). Their outputs are combined via a synthesis operator and submitted to the Aristotle engine for formalization in Lean 4. This document specifies the architecture, states the relevant formal properties, and records preliminary results.